## Part II : Language cascades
Chain together language models to guide formal proof search with informal proofs.


#### Notebooks:
| Topic | Notebook | 
|:-----------------------|-------:|
| 1. Language model cascades | [notebook](./notebooks/II_dsp__part1_intro.ipynb) |
| 2. Draft, Sketch, Prove | [notebook](./notebooks/II_dsp__part2_dsp.ipynb) |

All notebooks are in ([`partII_dsp/notebooks`](./notebooks)).

#### Setup
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](./isabelle_setup.md)