Definition
Plain language
A method where a model first writes an informal proof, turns it into a skeleton with the hard steps blanked out, and then fills in the blanks formally.
As stated in the literature
A formal-theorem-proving pipeline that drafts an informal natural-language proof, translates it into a formal skeleton with sorry-style gaps, and dispatches a prover to close each gap; the conceptual ancestor of blueprint-seeding in Goedel-Architect.
Why it matters: It breaks the hard problem of formal proof into stages a machine can handle, using informal reasoning to guide the rigorous part.
For example, the model might first write a casual paragraph explaining why a statement is true, then turn it into a step-by-step outline with the tricky steps left blank, and finally fill each blank with a formally checkable argument.
Heard on the show
“… This natural-language seeding goes back to an older idea called Draft-Sketch-Prove — have a model draft an informal proof, turn it into a formal skeleton with the gaps left blank, …”Episode 117 — How an Open AI System Verified 672 Hard Math Proofs for Under $300