Pith. sign in

REVIEW 4 major objections 4 minor 119 references

Autoformalization must stop translating isolated statements and start building complete, interconnected formal libraries of theories.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-02 05:35 UTC pith:7JIJES6X

load-bearing objection A well-organized position paper that usefully names the theory-level shift and nails the equivalence-checking problem, but overstates the urgency when the hard part—automated blueprint generation—is still unshown. the 4 major comments →

arxiv 2607.13292 v1 pith:7JIJES6X submitted 2026-07-14 cs.AI cs.CLcs.LGcs.PL

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

Marcus J. Min , Mike He , Zhaoyu Li , Zixuan Yi , Sharad Malik , Aarti Gupta , Xujie Si , Osbert Bastani This is my paper
classification cs.AI cs.CLcs.LGcs.PL
keywords autoformalizationtheory-levelformal knowledge basetheorem provingformal verificationabstraction learningdomain-specific languagesmultimodal input
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This position paper argues that the field of autoformalization—translating natural-language mathematics and engineering text into machine-checkable form—has set its sights too low. Real formalization projects, from the verification of major theorems to compilers and hardware, succeed only after a whole web of axioms, definitions, lemmas, and notations is in place; current systems treat that context as given. The paper claims that the next step is theory-level autoformalization: automatically constructing entire formal theories, with all dependencies, as coherent libraries. It argues this is necessary for scaling verification, for synthesizing training data for theorem-proving AI, and ultimately for discovering new mathematical abstractions. It then identifies the missing pieces—sound equivalence checking, hierarchical decomposition, abstraction learning, low-resource domain languages, and multimodal input—and proposes benchmarks, general-purpose models, and a common intermediate representation as a way forward.

Core claim

On the paper's own terms, the central discovery is a reframing: autoformalization is not a statement-translation task but a theory-construction task. The authors define Theory-Level Autoformalization as formalizing the full theoretical context—axioms, definitions, notations, examples, lemmas, theorems, proofs, tactics, and their inter-dependencies—as a single coherent formal library. Their key evidence is structural: even a single theorem like the Pythagorean theorem requires lower layers of primitives, derived definitions, and proof tooling before it can even be stated. They argue that statement-level success so far has been an artifact of leaning on mature human-built libraries, and that g

What carries the argument

The argument is carried by the 'Theory-Level Autoformalization Tower,' a four-layer model of how any formal theory is built: axiomatic primitives at the base, derived definitions above them, proof infrastructure (notations, lemmas, tactics) in the middle, and target theorems at the top. It makes visible why statement-level translation implicitly assumes all lower layers already exist. The paper's proposed forward machinery is a common intermediate representation that can express multiple domain-specific languages, be type-checked and verified, and embed target languages for verified translation—turning the problem of supporting many niche domain-specific languages from combinatorial into lin

Load-bearing premise

The cost-reduction argument assumes that language models can generate the hierarchical blueprint—the decomposition of a whole theory into lemmas and dependencies—with little expert effort, a capability demonstrated so far only for single statements or with human-authored blueprints.

What would settle it

Run an end-to-end case study formalizing a previously unformalized graduate-level theory chapter with and without a human-written blueprint under identical expert time budgets. If removing the blueprint does not reduce total expert effort relative to traditional formalization, the theory-level scaling claim fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Benchmarks and leaderboards would shift from accuracy on isolated statements to coherence and verifiability of whole libraries, with sound equivalence checking reported alongside precision and recall.
  • Theorem-proving AI would train on structured, dependency-linked corpora rather than flat statement-proof pairs, potentially improving generalization to new domains.
  • Verification of software, hardware, protocols, and access-control policies could be accelerated because the bottleneck—formalizing the surrounding specification context—would be automated rather than expert labor.
  • A common intermediate representation could make progress in mathematical autoformalization directly reusable for low-resource domain-specific languages, including declarative policy languages.
  • The eventual pay-off is a formalized knowledge base large enough to refactor, exposing common structure across domains and enabling proofs of results that cannot currently even be stated.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If theory-level autoformalization reaches maturity, the binding constraint on formal proof shifts from proof search to abstraction design; systems that can propose new definitions and reorganize libraries may matter more than systems that prove given statements.
  • The paper's subjectivity argument about equivalence suggests that evaluation will need interactive or human-in-the-loop equivalence checking for hard cases, not only fully automated judges—a design choice the paper leaves open.
  • A concrete testable extension: build a benchmark where the same theory is formalized twice with deliberately different but equivalent definitions; a sound theory-level checker should still recognize the two libraries as equivalent. No current checker would pass this.
  • The common-intermediate-representation proposal implies a transfer test: success on formalizing one well-supported mathematical domain should transfer to formalizing a legal or security-policy text, since both reduce to building a coherent dependency graph of concepts.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. This position paper argues that autoformalization research should move from translating isolated informal statements into formal ones to constructing complete, interdependent formal theory libraries. It defines theory-level autoformalization, motivates the shift through real-world formalization projects, the dependence of statement-level tasks on existing libraries, and the role of new abstractions in mathematical discovery. It then considers and rebuts three alternative views, identifies four open challenges (equivalence checking, hierarchical decomposition and abstraction learning, low-resource DSLs, and multimodal inputs), and makes three proposals (theory-level benchmarks, general-purpose LLMs, and a common intermediate representation). The paper is a synthesis and position statement rather than an experimental study.

Significance. If accepted, the thesis would redirect evaluation and system design from statement-level benchmarks to library-scale formalization, with implications for neural theorem-prover training data, verification speed, and the formulation of new mathematical abstractions. The paper's strengths are its clear articulation of an important problem, the critical analysis of equivalence checking in §4.1, the useful taxonomy of low-resource DSLs in §4.3, and the survey repository. However, the force of the central claim depends on the unexamined assumption that automated blueprint generation can scale; the paper's own survey indicates this is not yet established. With revision to temper the urgency claim and to sharpen the research agenda, the paper could serve as a useful agenda-setting contribution.

major comments (4)
  1. [§2.2c, §3.3, §4.2a] The central thesis ('necessary and imminent', §2.2) rests on the premise that automated theory-level formalization can replace human blueprints. The paper itself supplies evidence against this premise: §3.3 concedes that human blueprints 'still require substantial time and effort from human experts,' and §4.2a states that current decomposition methods (DNA, DRIFT, Aria) 'handle only high school mathematics with shallow dependency graphs' and 'remain insufficient for theory-level blueprint generation.' No experiment or mechanism is offered for closing this gap. If blueprint generation remains expert-intensive, the contribution is a repackaging of semi-automated formalization rather than a new capability. I recommend either softening the 'necessary and imminent' conclusion or adding a concrete test—e.g., the expert-effort measurement in §5.1—and making the scalability of blueprint generati
  2. [§4.1c, §5.1] Proposal 1 asks for benchmarks with 'sound equivalence checking' (criterion ii), but §4.1 convincingly shows that no checker combining soundness with practical coverage exists and that formal-formal equivalence is inherently subjective (§4.1c). As stated, the benchmark criterion is unsatisfiable. It should be restated as equivalence relative to a restricted admissible fragment—as BEq+ does in §4.1b—with precision and recall against expert judgments reported, not blanket soundness. This is not a cosmetic change: it determines what can be measured and therefore what the benchmark actually rewards.
  3. [§2.2b] The argument that statement autoformalization implies theory-level autoformalization relies on a conflation. For domains outside existing libraries, the main work is constructing the missing formal context, but that can be done incrementally, on demand for the target statements. The paper defines theory-level as formalizing 'the entire theoretical context ... as a coherent formal library' and speaks of 'holistic formal knowledge bases' (Abstract, §6). The step from 'dependencies are needed' to 'whole theories must be formalized as unified artifacts' is not automatic and is not supported by the survey. The paper should either define theory-level to include incremental dependency construction or justify the added holism requirement.
  4. [§2.2c] The claim that formalizing entire theories will enable discovery of new abstractions ('refactoring this codebase allows us to identify common structures ... eventually use these new abstractions to prove new results') is speculative. Historical examples show humans inventing abstractions; they do not show that a formal corpus is either necessary or sufficient for such invention. Library learning in program synthesis (Ellis et al., 2021) and theorem proving (Zhou et al., 2022) operates on much smaller scales and does not generate new mathematical abstractions. This is acceptable as a long-term motivation, but it should be separated from the 'necessary' claim so that the argument's load-bearing assumptions are explicit.
minor comments (4)
  1. [§2.2] The claim that 'the best current method achieves 71.4% on statements in Layer 3' (Min et al., 2026) needs the task and metric specified: is this statement autoformalization accuracy, proof autoformalization, or something else? Which dataset? Without this, the number is hard to interpret.
  2. [§4.3, Figure 7] Figure 7 is central to Proposal 3 but not described in enough detail. A concrete example showing how a multimodal input (e.g., a timing diagram plus text) would be represented in the common IR would make the proposal more actionable.
  3. [Appendix A] The distinction between declarative and imperative synthesis is helpful, but 'contains strictly more information' is intuitive rather than formal. Consider connecting this to the equivalence discussion in §4.1: a semantics-preserving translation is one for which the equivalence check passes under an appropriately restricted fragment.
  4. [Throughout] There are several typos and formatting issues: 'Goedel' should be 'Gödel', 'V oronkov' has a stray space, and the Abstract's survey URL is line-broken. A careful proofreading pass is needed.

Circularity Check

0 steps flagged

No significant circularity: the position argument is independent of its self-citations, and the paper explicitly concedes the scalability gaps that a circular argument would need to hide.

full rationale

This is a position paper, not a fitted derivation; there is no equation in which an output is defined in terms of an input, no fitted parameter is relabeled as a prediction, and no uniqueness theorem or ansatz is imported from the authors' prior work. The central claim—that autoformalization should move from isolated statements to theory-level knowledge bases—is supported by external formalization projects (Hales et al. 2015; Gonthier et al. 2013; Leroy 2009; Commelin et al. 2022) and by an independent argument that statements implicitly depend on surrounding theory. The self-citations (Min et al. 2026; Lin et al. 2025b) are used as illustrative empirical performance numbers, not as premises that entail the conclusion by construction. The paper also explicitly concedes the weak points: Section 3.3 says human blueprints 'still require substantial time and effort from human experts,' and Section 4.2a says current decomposition methods 'remain insufficient for theory-level blueprint generation' and handle only 'high school mathematics with shallow dependency graphs.' These admissions are the opposite of circularity—they acknowledge the gap between current methods and the proposed theory-level goal rather than defining it away. The scalability risk identified by a skeptical reader is a correctness/evidence concern, not a circular-reasoning defect. Therefore no circular step is present, and the score is 0.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 0 invented entities

This is an argumentative position paper, so the ledger records load-bearing assumptions rather than fitted parameters. No numbers are fit to data; the open-challenges sections are qualitative. The four assumptions above are the load-bearing premises of the agenda, not derived in the paper.

axioms (4)
  • domain assumption Formal, machine-checkable representation is the appropriate ground truth for reliable reasoning.
    Adopted throughout §2.1; if informal reasoning with LLM judgment is sufficient, the whole theory-level agenda loses its motivation.
  • domain assumption Informal reasoning scales only via learning and may plateau; formal reasoning scales via learning and search.
    Invoked in §3.1, View 1 counterargument; not proven, yet central to why formalization is necessary.
  • domain assumption Significant theoretical discoveries require new abstractions that compress knowledge, and these can be discovered by refactoring a formalized corpus.
    Used in §2.2c and §4.2b to argue theory-level autoformalization enables discovery; supported by historical examples but not by an operational mechanism.
  • domain assumption Current statement-level methods are blocked by missing theory context rather than by theorem-proving difficulty.
    Underlies §2.2b and §3.3; if formal context could be reconstructed cheaply per statement, the theory-level framing would be unnecessary.

pith-pipeline@v1.3.0-alltime-deepseek · 19896 in / 10618 out tokens · 103953 ms · 2026-08-02T05:35:25.941281+00:00 · methodology

0 comments
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.13292 by Aarti Gupta, Marcus J. Min, Mike He, Osbert Bastani, Sharad Malik, Xujie Si, Zhaoyu Li, Zixuan Yi.

Figure 1
Figure 1. Figure 1: Overview of this position paper. We argue for theory￾level autoformalization by examining its significance (Section 2), addressing alternative views (Section 3), identifying open chal￾lenges (Section 4), and proposing paths forward (Section 5). mains not yet supported by such libraries, the main work is precisely to construct those missing theoretical contexts. The need for this shift is evident from real-… view at source ↗
Figure 2
Figure 2. Figure 2: The “Theory-Level Autoformalization Tower” illus￾trated with the formal SystemE (Avigad et al., 2009) of Euclidean geometry implemented by Murphy et al. (2024) in Lean. 2 [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 4
Figure 4. Figure 4: shows an informal-to-formal translation of the Chang-Roberts leader election protocol (Chang & Roberts, 1979). In this example, the ring topology and initial states are encoded logically with axioms, and the formal model references atomic predicates introduced in this encoding. Theory-level datasets are needed to train LLMs on encoding such domain knowledge. c. Hardware Verification Languages. Hardware sec… view at source ↗
Figure 6
Figure 6. Figure 6: Informal-to-formal translation example of Cedar policy that implements clauses in HIPAA regulations. HIPAA regulations (U.S. Department of Health and Human Services, 2024) span hundreds of pages of legal prose with nested conditions, exceptions, and cross-references. For example, [PITH_FULL_IMAGE:figures/full_fig_p008_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Our 3 proposals for theory-level autoformalization: a common intermediate representation, general-purpose LLM agents, and benchmarks with sound equivalence checking. 5. Call to Action: Proposals for Advancing Theory-Level Autoformalization 5.1. Proposal 1: Theory-Level Benchmarks with Sound Equivalence Checking Existing benchmarks only evaluate definitions, statements, and proofs in isolation. We need benc… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

119 extracted references · 3 canonical work pages

  1. [1]

    Z3: an efficient

    De Moura, Leonardo and Bj. Z3: an efficient. Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages =. 2008 , isbn =

    2008

  2. [2]

    Barbosa, Haniel and Barrett, Clark and Brain, Martin and Kremer, Gereon and Lachnitt, Hanna and Mann, Makai and Mohamed, Abdalrhman and Mohamed, Mudathir and Niemetz, Aina and N\". Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Pract...

    doi:10.1007/978-3-030-99524-9_24 2022

  3. [3]

    The L ean 4 Theorem Prover and Programming Language

    Moura, Leonardo de and Ullrich, Sebastian. The L ean 4 Theorem Prover and Programming Language. Automated Deduction -- CADE 28. 2021

    2021

  4. [4]

    , title =

    Nipkow, Tobias and Wenzel, Markus and Paulson, Lawrence C. , title =. 2002 , isbn =

    2002

  5. [5]

    1997 , MONTH = May, KEYWORDS =

    Barras, Bruno and Boutin, Samuel and Cornes, Cristina and Courant, Judica. 1997 , MONTH = May, KEYWORDS =

    1997

  6. [6]

    2405.14333 , archivePrefix=

    Huajian Xin and Daya Guo and Zhihong Shao and Zhizhou Ren and Qihao Zhu and Bo Liu and Chong Ruan and Wenda Li and Xiaodan Liang , year=. 2405.14333 , archivePrefix=

    Pith/arXiv arXiv

  7. [7]

    2022 , eprint=

    Generating Natural Language Proofs with Verifier-Guided Search , author=. 2022 , eprint=

    2022

  8. [8]

    A machine-checked proof of the odd order theorem , year =

    Gonthier, Georges and Asperti, Andrea and Avigad, Jeremy and Bertot, Yves and Cohen, Cyril and Garillot, Fran. A machine-checked proof of the odd order theorem , year =. Proceedings of the 4th International Conference on Interactive Theorem Proving , pages =. doi:10.1007/978-3-642-39634-2_14 , abstract =

    doi:10.1007/978-3-642-39634-2_14

  9. [9]

    A formal proof of the

    Thomas Hales and Mark Adams and Gertrud Bauer and Dat Tat Dang and John Harrison and Truong Le Hoang and Cezary Kaliszyk and Victor Magron and Sean McLaughlin and Thang Tat Nguyen and Truong Quang Nguyen and Tobias Nipkow and Steven Obua and Joseph Pleso and Jason Rute and Alexey Solovyev and An Hoai Thi Ta and Trung Nam Tran and Diep Thi Trieu and Josef ...

    Pith/arXiv arXiv

  10. [10]

    Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20) , pages =

    The. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '20) , pages =. 2020 , publisher =

    2020

  11. [11]

    and Zdancewic, Steve , title =

    Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic, Steve , title =. Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , pages =. 2012 , isbn =. doi:10.1145/2103656.2103709 , abstract =

    arXiv 2012

  12. [12]

    CAV 2016, Part II, Lecture Notes in Computer Science , location =

    Alastair Reid and Rick Chen and Anastasios Deligiannis and David Gilday and David Hoyes and Will Keen and Ashan Pathirane and Erin Shepherd and Peter Vrabel and Ali Zaidi , acceptance =. CAV 2016, Part II, Lecture Notes in Computer Science , location =

    2016

  13. [13]

    2025 , eprint=

    Towards a Common Framework for Autoformalization , author=. 2025 , eprint=

    2025

  14. [14]

    Exploration of neural machine translation in autoformalization of mathematics in Mizar , url=

    Wang, Qingxiang and Brown, Chad and Kaliszyk, Cezary and Urban, Josef , year=. Exploration of neural machine translation in autoformalization of mathematics in Mizar , url=. doi:10.1145/3372885.3373827 , booktitle=

    arXiv

  15. [15]

    2023 , eprint=

    LeanDojo: Theorem Proving with Retrieval-Augmented Language Models , author=. 2023 , eprint=

    2023

  16. [16]

    Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings , pages =

    Szegedy, Christian , title =. Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings , pages =. 2020 , isbn =. doi:10.1007/978-3-030-53518-6_1 , abstract =

    work page doi:10.1007/978-3-030-53518-6_1 2020

  17. [17]

    2026 , url=

    Benchmark scores are well correlated, even across domains , author=. 2026 , url=

    2026

  18. [18]

    The Fourteenth International Conference on Learning Representations , year=

    Divide and Abstract: Autoformalization via Decomposition and Abstraction Learning , author=. The Fourteenth International Conference on Learning Representations , year=

  19. [19]

    2025 , eprint=

    DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems , author=. 2025 , eprint=

    2025

  20. [20]

    2025 , eprint=

    Mathesis: Towards Formal Theorem Proving from Natural Languages , author=. 2025 , eprint=

    2025

  21. [21]

    2023 , eprint=

    Multilingual Mathematical Autoformalization , author=. 2023 , eprint=

    2023

  22. [22]

    2025 , eprint=

    ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data , author=. 2025 , eprint=

    2025

  23. [23]

    2025 , eprint=

    Lean Workbook: A large-scale Lean problem set formalized from natural language math problems , author=. 2025 , eprint=

    2025

  24. [24]

    2025 , eprint=

    Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning , author=. 2025 , eprint=

    2025

  25. [25]

    2025 , eprint=

    FormaRL: Enhancing Autoformalization with no Labeled Data , author=. 2025 , eprint=

    2025

  26. [26]

    The Thirteenth International Conference on Learning Representations , year=

    Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach , author=. The Thirteenth International Conference on Learning Representations , year=

  27. [27]

    2025 , eprint=

    Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph , author=. 2025 , eprint=

    2025

  28. [28]

    2024 , eprint=

    Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency , author=. 2024 , eprint=

    2024

  29. [29]

    2025 , eprint=

    Reliable Evaluation and Benchmarks for Statement Autoformalization , author=. 2025 , eprint=

    2025

  30. [30]

    2021 , isbn =

    Ellis, Kevin and Wong, Catherine and Nye, Maxwell and Sabl\'. 2021 , isbn =. doi:10.1145/3453483.3454080 , booktitle =

    arXiv 2021

  31. [31]

    2024 , url=

    Lifan Yuan and Yangyi Chen and Xingyao Wang and Yi Fung and Hao Peng and Heng Ji , booktitle=. 2024 , url=

    2024

  32. [32]

    Proceedings of the 41st International Conference on Machine Learning , articleno =

    Wang, Zora Zhiruo and Neubig, Graham and Fried, Daniel , title =. Proceedings of the 41st International Conference on Machine Learning , articleno =. 2024 , publisher =

    2024

  33. [33]

    Jin Peng Zhou and Yuhuai Wu and Qiyang Li and Roger Baker Grosse , year=

  34. [34]

    2310.00656 , archivePrefix=

    Haiming Wang and Huajian Xin and Chuanyang Zheng and Lin Li and Zhengying Liu and Qingxing Cao and Yinya Huang and Jing Xiong and Han Shi and Enze Xie and Jian Yin and Zhenguo Li and Heng Liao and Xiaodan Liang , year=. 2310.00656 , archivePrefix=

    Pith/arXiv arXiv

  35. [35]

    Tool learning with large language models: a survey , volume =. Front. Comput. Sci. , author =. doi:10.1007/s11704-024-40678-2 , language =

    doi:10.1007/s11704-024-40678-2

  36. [36]

    2024 , eprint=

    FormalAlign: Automated Alignment Evaluation for Autoformalization , author=. 2024 , eprint=

    2024

  37. [37]

    Herald: A Natural Language Annotated

    Guoxiong Gao and Yutong Wang and Jiedong Jiang and Qi Gao and Zihan Qin and Tianyi Xu and Bin Dong , booktitle=. Herald: A Natural Language Annotated. 2025 , url=

    2025

  38. [38]

    2025 , eprint=

    ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization , author=. 2025 , eprint=

    2025

  39. [39]

    2025 , eprint=

    StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion , author=. 2025 , eprint=

    2025

  40. [40]

    2025 , eprint=

    Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions , author=. 2025 , eprint=

    2025

  41. [41]

    2024 , eprint=

    A New Approach Towards Autoformalization , author=. 2024 , eprint=

    2024

  42. [42]

    2025 , eprint=

    TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition , author=. 2025 , eprint=

    2025

  43. [43]

    2025 , eprint=

    ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization , author=. 2025 , eprint=

    2025

  44. [44]

    2025 , eprint=

    ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings , author=. 2025 , eprint=

    2025

  45. [45]

    2025 , eprint=

    Translating Informal Proofs into Formal Proofs Using a Chain of States , author=. 2025 , eprint=

    2025

  46. [46]

    Tyukin , year=

    Xiaolin Hu and Qinghua Zhou and Bogdan Grechuk and Ivan Y. Tyukin , year=. Step. 2506.10558 , archivePrefix=

    Pith/arXiv arXiv

  47. [47]

    AI for Math Workshop @ ICML 2024 , year=

    More Details, Please: Improving Autoformalization with More Detailed Proofs , author=. AI for Math Workshop @ ICML 2024 , year=

    2024

  48. [48]

    2023 , eprint=

    Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs , author=. 2023 , eprint=

    2023

  49. [49]

    The 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025 , year=

    Babel-formal: Translation of Proofs between Lean and Rocq , author=. The 5th Workshop on Mathematical Reasoning and AI at NeurIPS 2025 , year=

    2025

  50. [50]

    The strong Prime Number Theorem , year =

  51. [51]

    The Riemann Hypothesis for curves, autoformalized , year =

  52. [52]

    Certifying the FRI protocol , year =

  53. [53]

    2026 , eprint=

    130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? , author=. 2026 , eprint=

    2026

  54. [54]

    2024 , eprint=

    Autoformalizing Euclidean Geometry , author=. 2024 , eprint=

    2024

  55. [55]

    2010 , url =

    Zhong Shao and Bryan Ford , title =. 2010 , url =

    2010

  56. [56]

    2023 , eprint=

    Formalizing Chemical Physics using the Lean Theorem Prover , author=. 2023 , eprint=

    2023

  57. [57]

    2006 , eprint=

    A formally verified proof of the prime number theorem , author=. 2006 , eprint=

    2006

  58. [58]

    Computer Mathematics: 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007

    Gonthier, Georges , title =. Computer Mathematics: 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers , pages =. 2007 , isbn =. doi:10.1007/978-3-540-87827-8_28 , abstract =

    doi:10.1007/978-3-540-87827-8_28 2007

  59. [59]

    core-v-verif , year =

  60. [60]

    Formalization of Partial Differential Equations using HOL Theorem Proving , note =

    Deniz, Elif , url =. Formalization of Partial Differential Equations using HOL Theorem Proving , note =. 2024 , month =

    2024

  61. [61]

    QWIRE Practice: Formal Verification of Quantum Circuits in Coq , volume=

    Rand, Robert and Paykin, Jennifer and Zdancewic, Steve , year=. QWIRE Practice: Formal Verification of Quantum Circuits in Coq , volume=. doi:10.4204/eptcs.266.8 , journal=

    work page doi:10.4204/eptcs.266.8

  62. [62]

    Survey of Hallucination in Natural Language Generation , volume=

    Ji, Ziwei and Lee, Nayeon and Frieske, Rita and Yu, Tiezheng and Su, Dan and Xu, Yan and Ishii, Etsuko and Bang, Ye Jin and Madotto, Andrea and Fung, Pascale , year=. Survey of Hallucination in Natural Language Generation , volume=. ACM Computing Surveys , publisher=. doi:10.1145/3571730 , number=

    doi:10.1145/3571730

  63. [63]

    Textbook Proofs Meet Formal Logic -- The Problem of Underspecification and Granularity

    Autexier, Serge and Fiedler, Armin. Textbook Proofs Meet Formal Logic -- The Problem of Underspecification and Granularity. Mathematical Knowledge Management. 2006

    2006

  64. [64]

    Shulman, Michael , title =. Bull. Amer. Math. Soc. (N.S.) , volume =. 2024 , doi =

    2024

  65. [65]

    2025 , eprint=

    Reasoning Curriculum: Bootstrapping Broad LLM Reasoning from Math , author=. 2025 , eprint=

    2025

  66. [66]

    2024 , eprint=

    Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization , author=. 2024 , eprint=

    2024

  67. [67]

    LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers , url=

    Olausson, Theo and Gu, Alex and Lipkin, Ben and Zhang, Cedegao and Solar-Lezama, Armando and Tenenbaum, Joshua and Levy, Roger , year=. LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers , url=. doi:10.18653/v1/2023.emnlp-main.313 , booktitle=

    doi:10.18653/v1/2023.emnlp-main.313 2023

  68. [68]

    Missing undergraduate mathematics in mathlib , year =

  69. [69]

    Johan Commelin and Adam Topaz and Kevin Buzzard and Filippo A. E. Nuccio and Riccardo Brasca and others , title =. 2022 , howpublished =

    2022

  70. [70]

    2025 , howpublished =

    Thang Luong and Edward Lockhart , title =. 2025 , howpublished =

    2025

  71. [71]

    2025 , howpublished =

    Alexander Wei , title =. 2025 , howpublished =

    2025

  72. [72]

    2019 , howpublished =

    Rich Sutton , title =. 2019 , howpublished =

    2019

  73. [73]

    2020 , eprint=

    Generative Language Modeling for Automated Theorem Proving , author=. 2020 , eprint=

    2020

  74. [74]

    2020 , howpublished =

    2020

  75. [75]

    2025 , note =

    Harrison, John , title =. 2025 , note =

    2025

  76. [76]

    arXiv preprint arXiv:2109.05093 , year=

    PICARD: Parsing incrementally for constrained auto-regressive decoding from language models , author=. arXiv preprint arXiv:2109.05093 , year=

    Pith/arXiv arXiv

  77. [77]

    Advances in Neural Information Processing Systems , volume=

    Din-sql: Decomposed in-context learning of text-to-sql with self-correction , author=. Advances in Neural Information Processing Systems , volume=

  78. [78]

    Overview of semantic views , year =

  79. [79]

    About MetricFlow , year =

  80. [80]

    LookML terms and concepts , year =

Showing first 80 references.