Chain together language models to guide formal proof search with informal proofs.
| Topic | Notebook |
|---|---|
| 1. Language model cascades | notebook |
| 2. Draft, Sketch, Prove | notebook |
All notebooks are in (partII_dsp/notebooks).
The Draft, Sketch, Prove notebook requires setting up an Isabelle proof checker for the "sketch" stage.
Please follow this guide to set up the Isabelle Proof Checker: Isabelle Proof Checker Setup