majiayu000 HOL4 Proof Pipeline Skills
Three-phase proof development methodology:
/hol4-plan
Interactive proof planning. Creates mathematical argument with validated assumptions. See plan.md
/hol4-sketch
Translate plan to HOL4 sketch. Creates SML with cheats + task files for subagents. See sketch.md
/hol4-prove
Fill in cheats and complete proofs. Interactive or autonomous mode. See prove.md
Autonomous Execution
python hol_planner.py --goal "prove theorem X"
python hol_sketch.py --plan plan.md --workdir /path
python hol_proof_agent.py --task TASK_foo.md
python hol_pipeline.py --theorem X --workdir /path # end-to-end
Methodology Prompts
Full prompts in prompts/hol4/:
planner.md- Planning methodologysketch_impl.md- Sketching methodologyproof_agent.template.md- Proving methodology