Within a couple of days we will release Pantograph v0.3. This tool incorporates a few critical features for training machine learning agents for Lean, including:
- Proper handling of metavariable coupling
- The ability to scrape proof data from Mathlib
- Drafting and environmental modification
- Inspecting proof terms generated by tactics
These feature enhance Lean 4 so it becomes more suitable for AIML.
More stabilization and feature releases will come after v0.3. The primary purpose of these features is to facilitate training of non-autoregressive models such as Graph Neural Networks (GNN) and hybrid theorem proving algorithms. The details of which will be released at an undetermined time in the future.
In the mean time, bring your best models out and train them!