Today I announce that PyPantograph is stable enough for usage. Pantograph is a Lean 4 interaction library specifically tailored to the need for training and evaluating machine theorem proving agents. It provides a few features not available in other Lean interaction systems:
- Executing tactics and writing expressions, with support of
have,let,calc,conv. - Conducting tree search on proofs
- Manual and automatic (default) handling of metavariable coupling
- Reading and adding symbols to the Lean environment
- Extraction of tactic training data
- Drafting (like Draft-Sketch-Prove)
The paper can be found here. The API documentation is in the repository.
More features will be added in Pantograph. Anyone who wishes to collaborate on experiments using Pantograph can send me an email.