We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Coq. Its core design choices include a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file.
Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark.
Lean output excerpts can be found on GitHub.
Blogger's Review: This project opens new avenues for the automation of mathematical proofs by combining LLM's natural language processing capabilities with formal verification. Its design significantly reduces the learning curve for users, making it a noteworthy development in the field.