Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
It addresses the challenge of making formal theorem proving accessible to LLMs by mimicking natural mathematical language, but results are preliminary and incremental over existing provers.
Visored is a dependent-type-based prover designed for LLM-generated mathematics, featuring a natural-language-like surface and rule-driven automation. Early experiments show LLMs can use it effectively on miniF2F without prover-specific training data.
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 Rocq. Its core design choices are 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: https://github.com/xiyuzhai-husky-lang/visored/