mlsanityData to 14 Oct 2026

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

arXiv 2606.17581 ↗First posted 16 Jun 2026cs.PL cs.AIcited by 0

Not on the map. Why?

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/

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

25 of 52 references.

References · 25

  1. 2017Attention Is All You Needcited by 60,361
  2. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  3. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  4. 2022Survey of Hallucination in Natural Language Generationcited by 2,075
  5. 2023A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questionscited by 1,601
  6. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
  7. 2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 867
  8. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  9. 2023Llemma: An Open Language Model For Mathematicscited by 388
  10. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  11. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  12. 2022Autoformalization with Large Language Modelscited by 263
13 more
  1. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  2. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  4. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  5. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 101
  6. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
  7. 2025Mathematical exploration and discovery at scalecited by 77
  8. 2025ThetaEvolve: Test-time Learning on Open Problemscited by 64
  9. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 21
  10. 2024GFLean: An Autoformalisation Framework for Lean via GFcited by 9
  11. 2024A Natural Formalized Proof Languagecited by 2
  12. 2026Towards Solving the Gilbert-Pollak Conjecture via Large Language Modelscited by 2
  13. 2026LLM2SMT: Building an SMT Solver with Zero Human-Written Codecited by 2

Built on by

Not cited yet.