Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
-
Updated
Jul 17, 2024 - OCaml
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
Mostly Automated Proof Repair for Verified Libraries
Artifact for "Proof Repair across Quotient Type Equivalences" paper (OOPSLA 2025 paper)
Self-hostable paraconsistent HoTT LLM-to-Lean acceptance gateway. Runs proof attempts through security preflight, Lean checks, theorem-fingerprint locks, and ShadowHoTT bilattice routing for accept/repair/reject/human-review decisions.
Verifier-backed math reasoning lab for proof flaw localization, minimal repair, and RL-style evaluation.
Reproducible, cheat-checked evaluation of AI proof-filling in Lean 4: mine missing proofs, run a pluggable model, replay and score under explicit anti-cheat guards (statement-unchanged, axiom-whitelist, reverse-dependency).
Add a description, image, and links to the proof-repair topic page so that developers can more easily learn about it.
To associate your repository with the proof-repair topic, visit your repo's landing page and select "manage topics."