# Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics

arXiv: https://arxiv.org/abs/2606.17581 · HTML: https://mlsanity.com/paper/2606.17581/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 25 of its 52 references that are in the map.
- First posted on arXiv 16 Jun 2026.

## Builds on (most cited first, 25 of 25)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions](https://mlsanity.com/paper/2311.05232/) (2023)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Mathematical exploration and discovery at scale](https://mlsanity.com/paper/2511.02864/) (2025)
- [ThetaEvolve: Test-time Learning on Open Problems](https://mlsanity.com/paper/2511.23473/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [GFLean: An Autoformalisation Framework for Lean via GF](https://mlsanity.com/paper/2404.01234/) (2024)
- [A Natural Formalized Proof Language](https://mlsanity.com/paper/2405.07973/) (2024)
- [Towards Solving the Gilbert-Pollak Conjecture via Large Language Models](https://mlsanity.com/paper/2601.22365/) (2026)
- [LLM2SMT: Building an SMT Solver with Zero Human-Written Code](https://mlsanity.com/paper/2603.06931/) (2026)

## Abstract (arXiv)

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/