mlsanityData to 14 Oct 2026

Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases

arXiv 2607.13292 ↗First posted 14 Jul 2026cs.AI cs.CL cs.LGcited by 3

Not on the map. Why?

Abstract (arXiv)

Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are inherently theory-level: they require an entire web of axioms, definitions, and lemmas before target theorems can even be stated. In this position paper, we argue for theory-level autoformalization: formalizing complete theories, including all their inter-dependencies, as structured libraries. We examine the significance of this shift, address alternative views, identify open challenges, and propose three promising paths forward. Our survey of autoformalization is available at https://github.com/marcusm117/Awesome-Autoformalization.

Key facts. Cited by 3 papers in the map (data through 14 Oct 2026). Builds on 37 of its 89 references that are in the map. First posted on arXiv 14 Jul 2026.

Builds on

37 of 89 references.

References · 37

  1. 2022Survey of Hallucination in Natural Language Generationcited by 2,075
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  3. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  4. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  5. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  6. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  7. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  8. 2024Tool Learning with Large Language Models: A Surveycited by 223
  9. 2023VeriGen: A Large Language Model for Verilog Code Generationcited by 200
  10. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  11. 2023CRAFT: Customizing LLMs by Creating and Retrieving from Specialized Toolsetscited by 129
  12. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
25 more
  1. 2024TroVE: Inducing Verifiable and Efficient Toolboxes for Solving Programmatic Taskscited by 75
  2. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
  3. 2024Herald: A Natural Language Annotated Lean 4 Datasetcited by 59
  4. 2022Generating Natural Language Proofs with Verifier-Guided Searchcited by 52
  5. 2015A formal proof of the Kepler conjecturecited by 42
  6. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  7. 2024Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)cited by 34
  8. 2024Text2Cypher: Bridging Natural Language and Graph Databasescited by 30
  9. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 28
  10. 2025Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitionscited by 22
  11. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 21
  12. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 21
  13. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 21
  14. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 18
  15. 2023A New Approach Towards Autoformalizationcited by 10
  16. 2022Formalizing Chemical Physics using the Lean Theorem Provercited by 9
  17. 2024REFACTOR: Learning to Extract Theorems from Proofscited by 9
  18. 2025FormaRL: Enhancing Autoformalization with no Labeled Datacited by 9
  19. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  20. 2025Reasoning Curriculum: Bootstrapping Broad LLM Reasoning from Mathcited by 8
  21. 2025Towards a Common Framework for Autoformalizationcited by 7
  22. 2025QLCoder: A Query Synthesizer For Static Analysis of Security Vulnerabilitiescited by 7
  23. 2025StepProof: Step-by-step verification of natural language mathematical proofscited by 6
  24. 2025FLAG: Formal and LLM-assisted SVA Generation for Formal Specifications of On-Chip Communication Protocolscited by 3
  25. 2025Translating Informal Proofs into Formal Proofs Using a Chain of Statescited by 3

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 3.

3 papers.

  1. 2026VALG: An Agentic System for ML Theory Researchcited by 2
  2. 2026Aligning Faithfulness for Theory-Scale Autoformalizationcited by 0
  3. 2026Definition Grounding in Theory-Level Auto-formalizationcited by 0