Pith. sign in

REVIEW 4 major objections 5 minor 5 cited by

Autoformalization in the Era of Large Language Models: A Survey

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Autoformalization turns LLM guesses into machine-checkable proofs

desk verdict A useful survey of autoformalization with a handy workflow framing and dataset tables, but rough prose, uncited numbers, and an overstrong verifiability claim mean it needs major revision. read the letter →

arxiv 2505.23486 v2 pith:RIMHTXRE submitted 2025-05-29 cs.AI

Ke Weng , Lun Du , Sirui Li , Wangyue Lu , Haozhe Sun , Hengyu Liu , Tiancheng Zhang This is my paper
classification cs.AI MSC 03B3568V20
keywords autoformalizationlargelanguagemodelsformalverificationtheoremprovingproofassistantsmathematicalreasoningsemanticequivalencehallucination
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Autoformalization is the process of translating informal mathematical statements into formal, machine-checkable logic, and this survey argues that it is becoming a foundational enabler for trustworthy LLM systems, not just a tool for theorem proving. The paper organizes the field along three dimensions—mathematical problem domain, difficulty level, and the end-to-end workflow from data preprocessing to evaluation—and shows how each stage now has concrete model and dataset support. It also connects autoformalization to formal verification of LLM outputs in code validation, medicine, and self-improvement, arguing that translating LLM claims into formal logic lets those claims be checked instead of trusted. A sympathetic reader would take the paper's central assertion to be that the path to reliable, verifiable AI reasoning runs through autoformalization, with current proof-assistant results providing early evidence.

What carries the argument

The load-bearing object is the autoformalization workflow: a pipeline that moves from an informal or semi-formal statement through data preprocessing, a translation model (rule-based or LLM-based), postprocessing corrections, and evaluation, ending in a formal statement that a proof assistant can type-check. The survey treats this pipeline as the bridge between natural-language ambiguity and machine-verifiable logic, and its breakdown into stages is what lets the paper compare systems and identify where semantic drift, data scarcity, and proof-strategy errors enter. The accompanying three-dimensional taxonomy—problem domain, difficulty level, and abstraction level—does the work of explaining why the same pipeline behaves very differently on competition problems, undergraduate textbook theorems, and graduate research mathematics.

What would settle it

Take a set of natural-language mathematical arguments with deliberately wrong conclusions, run them through an autoformalizer and proof assistant with the survey's recommended postprocessing, and count how many wrong arguments pass; if a substantial fraction pass because the formal statements no longer reflect the original claims, the verifiability benefit fails. A complementary round-trip check is to back-translate accepted formal statements to informal language and have human judges detect meaning shifts.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is that 'autoformalization is not merely a tool for mathematical proof: it is a foundational enabler for building LLM systems that can reason, code, and verify in an integrated and principled way.' The survey assembles the evidence for this claim by reviewing how modern LLM-based autoformalizers convert natural-language mathematics into proof-assistant code, how data pipelines and postprocessing filters improve the fidelity of that conversion, and how evaluation has moved beyond compile-time type checking toward semantic equivalence. It further documents the emerging applications of autoformalization as a verification layer for LLM-generated artifacts, where formal logic, specification languages, and sanitized structured references are used to catch unsound outputs. The picture the paper paints is a positive feedback loop: machine learning makes formalization easier, and formal systems make machine learning outputs checkable.

Load-bearing premise

The load-bearing premise is that the formal statement produced by autoformalization preserves the meaning of the original informal statement; if it drifts, checking the formal version only checks a different, possibly vacuous proposition.

Editorial extensions

If this is right

  • If the central claim is right, formal verification becomes a practical quality gate for LLM-produced code, specifications, and mathematical reasoning, not an idealized add-on.
  • Proof-assistant checking alone will not be enough: the survey's own evaluation section implies that semantic-equivalence metrics must accompany type checking, making semantic fidelity a core engineering requirement.
  • Progress on autoformalization will be uneven: competition and undergraduate mathematics should yield first, while research-level 'unlinked' theorems will require compositional generalization and missing-context handling.
  • Data scarcity is the binding constraint, so synthetic data, back-translation from formal to informal, and multi-linguistic formal corpora are the levers that move the field.
  • LLM self-improvement loops can be made safer by filtering or reweighting outputs that fail formal checks, connecting autoformalization to data curation and reinforcement learning.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A step the paper leaves implicit is that the entire verifiability benefit rests on semantic fidelity: if the formalized statement does not mean what the informal statement meant, a successful proof-assistant check verifies a different proposition, so semantic equivalence metrics are not a bonus but the crux.
  • A testable extension would be a round-trip benchmark: autoformalize a statement, informally back-translate it, and compare the two informal versions for meaning; a high divergence rate would signal that current autoformalizers are not yet ready to serve as verification bridges.
  • The pipeline view suggests autoformalization could generalize beyond mathematics into any high-assurance domain with a formal target language, such as program contracts or security properties, whenever a faithful translation layer exists.
  • A further consequence is that hallucination detection could be recast as a formalization check: rather than asking whether an LLM answer is true, ask whether its formalized version proves itself in a proof assistant, which would turn verification into a training signal.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 5 minor

Summary. This manuscript surveys autoformalization, the translation of informal mathematical statements into machine-checkable formal representations, with an emphasis on LLM-based methods. It proposes a three-dimensional taxonomy organized by mathematical domain, difficulty level, and workflow; inventories open-source models and datasets; reviews data preprocessing, modeling, post-processing, and evaluation; surveys recent theorem-proving systems; and argues that autoformalization can serve as a bridge from LLM outputs to formal verification. The paper is a survey with no new derivations or experiments; its contributions are organizational and descriptive.

Significance. If the survey's claims are taken at face value, it provides a useful entry point to a rapidly growing field: the resource tables, the workflow taxonomy, and the discussion of evaluation metrics such as BEqL and alignment scoring are valuable, and the paper explicitly acknowledges that type checking alone does not establish semantic correctness. The central vision—autoformalization as an enabler of verifiable LLM reasoning—is timely and plausible, but it currently rests on an unvalidated semantic-fidelity assumption and on a few unsourced quantitative statements. With targeted corrections and a clearer separation between established results and open assumptions, the survey could be a useful reference.

major comments (4)
  1. [Section 1 and Section 5.1] The claim that 'GPT-o3 reportedly solved 25.2% of problems in the Frontier Mathematics benchmark, significantly outperforming earlier models that achieved only around 2%' is given without any citation or specification of the evaluation protocol. The same unsourced figure reappears in Section 5.1. Because this number is used to motivate the need for formal verification, please cite the primary benchmark report and state the exact protocol (e.g., sampling budget, pass@k), or remove the quantitative comparison.
  2. [Section 4.2, LLM-based Autoformalization] The paragraph beginning 'Recent research has shown that LLMs can translate...' asserts that 'under the same model, the informal math competition level problem achieves 70% accuracy, while the formal math competition level problem only achieves 30% accuracy' without a citation. This quantitative comparison is load-bearing for the later back-translation discussion and needs a source. In the same subsection, the sentence 'In order to further expand the data, [Liu et al., 2025c]...' appears twice verbatim; please remove the duplication.
  3. [Section 6 (esp. 6.3) vs. Section 4.2 Evaluatation] The central claim that autoformalization can verify LLM outputs presupposes that the formalization preserves the meaning of the informal statement. Section 4.2 itself concedes that type checking does not guarantee semantic equivalence and that existing metrics (BEqL, BEq+, alignment scoring, LeanScorer) are heuristic and, in the case of BEqL, have a high false-negative rate. The survey reports no end-to-end measurement of semantic-drift rates ('proven but semantically wrong' outputs) for the verification pipelines it highlights. Please either present such evidence, or explicitly reframe Section 6 as a research vision with semantic fidelity as an open condition.
  4. [Table 2, Formal Math row] The Formal Math row states that the dataset is '22.8× larger than the widely used MiniF2F benchmark', but MiniF2F is listed immediately above as 488 statements; 5,560/488 is approximately 11.4, not 22.8. Please correct the multiplier or clarify which baseline and dataset size are being used.
minor comments (5)
  1. [Section 4.3 heading] The heading 'Therom Proof' should read 'Theorem Proof'; the text also contains multiple misspellings such as 'assistans' in Section 3.
  2. [Section 5.2, Graduate Level] The sentence about 'unlinked formalization' is garbled and repeats the same phrase several times; please rewrite to state what 'unlinked formalization' means and what Patel et al. actually propose.
  3. [References] Reference [Peano, 1889] is incomplete (it gives only 'Giuseppe Peano. 1889.'), and reference [Antropic, 2024] misspells 'Anthropic'.
  4. [Table 3, GSM8K row] The GSM8K row has no entries; if the dataset is included only as a natural-language reasoning benchmark rather than an autoformalization resource, this should be stated in the caption.
  5. [Sections 6.1, 6.2, and 8] Please replace 'LLMS' with 'LLMs' in Sections 6.1 and 6.2, and rephrase the Section 8 title 'Different with Other Survey' to standard English such as 'Comparison with Existing Surveys'.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the survey synthesizes external results and makes no derivation that reduces to its own inputs.

full rationale

This paper is a survey: it organizes, summarizes, and compares existing autoformalization work rather than deriving new predictions from fitted parameters or from its own definitions. The central claim in Section 1 that autoformalization is a foundational enabler for verifiable LLM systems is a synthesis of external cited results (AlphaProof, DeepSeek-Prover, FormalAlign, LLEMMA, etc.) and does not reduce to the authors' own prior work. The few self-citations (e.g., Shi et al. 2023 and Zheng et al. 2025, which include co-author Lun Du) are used only to illustrate broad application areas such as code generation and system specification; they are not load-bearing for any specific technical conclusion. Section 8 explicitly credits Yang et al. 2024 for the rule-based vs. LLM-based taxonomy it builds on, which is honest external attribution rather than circular self-justification. The skeptic's concern about semantic fidelity is a genuine limitation, and the paper itself acknowledges it in Section 4.3: type checking does not guarantee semantic equivalence. But acknowledging a limitation is not circular reasoning. There is no equation, fitted parameter, or definitional chain in which a stated prediction is equivalent to its input. The paper is self-contained as a survey against external benchmarks, so the appropriate circularity score is 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

This is a survey, so there are no fitted parameters or invented entities. The listed axioms are the unproven premises the survey's central argument depends on.

assumptions (3)
  • domain assumption Informalization is easier than formalization.
    Used in Sections 4.1 and 4.2 to justify data augmentation via back-translation; the survey relies on this asymmetric difficulty to claim that synthetic data will improve autoformalization performance.
  • domain assumption The surveyed datasets and results are accurately reported.
    The survey's conclusions rest on the correctness of numbers and claims from cited papers; numerous typos and missing details prevent independent verification of these reports.
  • ad hoc to paper Autoformalization outputs preserve meaning.
    The claim that autoformalization can verify LLM outputs assumes that the formalized statement is semantically equivalent to the informal one; if not, verification is vacuous. This is a central unstated assumption in Section 6.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Autoformalization in the Era of Large Language Models: A Survey." pith.science (2026). https://pith.science/paper/RIMHTXRE

@misc{pith2026250523486,
  author       = {Pith},
  title        = {Pith review of: Autoformalization in the Era of Large Language Models: A Survey},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RIMHTXRE}},
  note         = {Machine review of arXiv:2505.23486}
}
read the original abstract

Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both theoretical and applied domains. Driven by the rapid progress in artificial intelligence, particularly large language models (LLMs), this field has witnessed substantial growth, bringing both new opportunities and unique challenges. In this survey, we provide a comprehensive overview of recent advances in autoformalization from both mathematical and LLM-centric perspectives. We examine how autoformalization is applied across various mathematical domains and levels of difficulty, and analyze the end-to-end workflow from data preprocessing to model design and evaluation. We further explore the emerging role of autoformalization in enhancing the verifiability of LLM-generated outputs, highlighting its potential to improve both the trustworthiness and reasoning capabilities of LLMs. Finally, we summarize key open-source models and datasets supporting current research, and discuss open challenges and promising future directions for the field.

Figures

Figures reproduced from arXiv: 2505.23486 by the authors.

Figure 1
Figure 1. The framework of workflow for Autoformalization [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Multi-dimensional partitioning Autoformalization in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 5 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generation

    cs.SE 2026-07 conditional novelty 7.0 of 10

    An exact model-checker oracle for NL-to-TLA+ still yields an elevenfold “correctness envelope” (18.7%–1.7%) once interface supply and vacuity screens are made explicit.

  2. Verified LLM-Driven Synthesis for Concept Design

    cs.SE 2026-07 conditional novelty 7.0 of 10

    A formal reaction semantics plus an LLM+Alloy CEGIS loop synthesizes and bounded-verifies coordination rules for Concept Design, with scenarios beating natural-language prompts for intent recovery.

  3. FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

    cs.CL 2026-07 conditional novelty 7.0 of 10

    FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.

  4. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

    cs.CL 2026-07 accept novelty 6.0 of 10

    LLM formal provers must shift from competition solvers to research agents that handle open-ended, under-specified frontier mathematics under machine-checked rigor.

  5. Integrating Rules and Semantics for LLM-Based C-to-Rust Translation

    cs.SE 2025-08 unverdicted novelty 5.0 of 10

    IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.

Reference graph

Works this paper leans on

59 extracted references · 49 canonical work pages · cited by 5 Pith papers

  1. [1]

    Alphaverus: Bootstrapping formally ver- ified code generation through self-improving translation and treefinement

    [Aggarwal et al., 2024] Pranjal Aggarwal, Bryan Parno, and Sean Welleck. Alphaverus: Bootstrapping formally ver- ified code generation through self-improving translation and treefinement. arXiv preprint arXiv:2412.06176,

    arXiv 2024

  2. [4]

    Claude 3 haiku: Our fastest model yet

    [Antropic, 2024] Antropic. Claude 3 haiku: Our fastest model yet

    work page 2024

  3. [5]

    Ayers, Dragomir Radev, and Jeremy Avigad

    [Azerbayev et al., 2023] Zhangir Azerbayev, Bartosz Pi- otrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics,

    work page 2023

  4. [7]

    On learning verifiers for chain-of-thought reasoning,

    [Balcan et al., 2025] Maria-Florina Balcan, Avrim Blum, Zhiyuan Li, and Dravyansh Sharma. On learning verifiers for chain-of-thought reasoning,

    work page 2025

  5. [9]

    Lean-ing on quality: How high- quality data beats diverse multilingual data in autoformal- ization,

    [Chan et al., 2025] Willy Chan, Michael Souliman, Jakob Nordhagen, Brando Miranda, Elyas Obbad, and Kai Fronsdal Sanmi Koyejo. Lean-ing on quality: How high- quality data beats diverse multilingual data in autoformal- ization,

    work page 2025

  6. [10]

    Bunescu, and David Juedes

    [Cunningham et al., 2023] Garett Cunningham, Razvan C. Bunescu, and David Juedes. Towards autoformalization of mathematics and code correctness: Experiments with elementary proofs. CoRR, abs/2301.02195,

    arXiv 2023

  7. [11]

    The lean theorem prover (system description)

    [de Moura et al., 2015] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378–388, Cham,

    work page 2015

  8. [13]

    How numina- math won the 1st aimo progress prize

    [Fleureau et al., 2024] Yann Fleureau, Edward Beeching Jia Li, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, and Kashif Rasul. How numina- math won the 1st aimo progress prize

    work page 2024

Show all 59 references
  1. [14]

    Her- ald: A natural language annotated lean 4 dataset,

    [Gao et al., 2025] Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Her- ald: A natural language annotated lean 4 dataset,

    2025

  2. [15]

    Formal proof—the four- color theorem

    [Gonthier, 2008] Georges Gonthier. Formal proof—the four- color theorem

    2008

  3. [17]

    From knowledge generation to knowledge verification: Exam- ining the biomedical generative capabilities of chatgpt

    [Hamed et al., 2025] Ahmed Abdeen Hamed, Alessandro Crimi, Magdalena M Misiak, and Byung Suk Lee. From knowledge generation to knowledge verification: Exam- ining the biomedical generative capabilities of chatgpt. arXiv preprint arXiv:2502.14714,

    2025 arXiv

  4. [18]

    Towards verifiable text gen- eration with symbolic references

    [Hennigen et al., 2023] Lucas Torroba Hennigen, Shannon Shen, Aniruddha Nrusimha, Bernhard Gapp, David Son- tag, and Yoon Kim. Towards verifiable text gen- eration with symbolic references. arXiv preprint arXiv:2311.09188,

    2023 arXiv

  5. [19]

    The coq proof assistant a tutorial

    [Huet et al., 1997] G´erard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant a tutorial. Rap- port Technique, 178:113,

    1997

  6. [20]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

    [Jiang et al., 2023b] Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timoth ´ee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Con...

    2023

  7. [21]

    Jiang, Wenda Li, and Mateja Jamnik

    [Jiang et al., 2024] Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multi-language diversity benefits autoformaliza- tion. In A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and C. Zhang, editors,Advances in Neural Information Processing Systems, volume 37,...

    2024

  8. [22]

    Finding inductive loop invariants using large language models

    [Kamath et al., 2023] Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deli- giannis, Shuvendu K Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma. Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948,

    2023 arXiv

  9. [23]

    The cost of poor software quality in the us: A 2022 report

    [Krasner, 2022] Herb Krasner. The cost of poor software quality in the us: A 2022 report. Proc.Consortium Inf. Softw. QualityTM (CISQTM),

    2022

  10. [24]

    A survey on deep learning for theorem proving

    [Li et al., 2024b] Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939,

    arXiv

  11. [25]

    Hunyuan- prover: A scalable data synthesis framework and guided tree search for automated theorem proving,

    [Li et al., 2025] Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuan- prover: A scalable data synthesis framework and guided tree search for automated theorem proving,

    2025

  12. [26]

    Augmenting smart contract decompiler output through fine-grained dependency analysis and llm-facilitated se- mantic recovery

    [Liao et al., 2025] Zeqin Liao, Yuhong Nan, Zixu Gao, Hen- glong Liang, Sicheng Hao, Peifan Reng, and Zibin Zheng. Augmenting smart contract decompiler output through fine-grained dependency analysis and llm-facilitated se- mantic recovery. arXiv preprint arXiv:2501.08670,

    2025

  13. [27]

    Goedel- prover: A frontier model for open-source automated theo- rem proving,

    [Lin et al., 2025] Yong Lin, Shange Tang, Bohan Lyu, Ji- ayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel- prover: A frontier model for open-source automated theo- rem proving,

    2025

  14. [28]

    Abstraction in mathematics

    [Luigi, 2003] Ferrari Pier Luigi. Abstraction in mathematics

    2003

  15. [30]

    Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008, Proceed- ings, volume

    [Mohamed et al., 2008] Otmane Ait Mohamed, C ´esar Mu˜noz, and Sofi `ene Tahar. Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008, Proceed- ings, volume

    2008

  16. [31]

    The lean 4 theorem prover and programming language

    [Moura and Ullrich, 2021] Leonardo de Moura and Sebas- tian Ullrich. The lean 4 theorem prover and programming language. In Automated Deduction–CADE 28: 28th In- ternational Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28 , pages 625–635. Springer,

    2021

  17. [33]

    Gpt-4 technical report,

    [OpenAI, 2024] OpenAI. Gpt-4 technical report,

    2024

  18. [34]

    A new approach towards autoformalization,

    [Patel et al., 2024] Nilay Patel, Rahul Saha, and Jeffrey Flanigan. A new approach towards autoformalization,

    2024

  19. [35]

    Gflean: An autoformalisa- tion framework for lean via gf,

    [Pathak, 2024] Shashank Pathak. Gflean: An autoformalisa- tion framework for lean via gf,

    2024

  20. [36]

    Isabelle: A generic theorem prover

    [Paulson, 1994] Lawrence C Paulson. Isabelle: A generic theorem prover. Springer,

    1994

  21. [38]

    Instantiation-based formalization of logical reasoning tasks using language models and logical solvers,

    [Raza and Milic-Frayling, 2025] Mohammad Raza and Natasa Milic-Frayling. Instantiation-based formalization of logical reasoning tasks using language models and logical solvers,

    2025

  22. [39]

    [Ren et al., 2025] Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Ad- vancing fo...

    2025

  23. [40]

    Divide and translate: Composi- tional first-order logic translation and verification for com- plex logical reasoning

    [Ryu et al., 2024] Hyun Ryu, Gyeongman Kim, Hyemin S Lee, and Eunho Yang. Divide and translate: Composi- tional first-order logic translation and verification for com- plex logical reasoning. arXiv preprint arXiv:2410.08047 ,

    2024 arXiv

  24. [41]

    Can ai-generated text be reliably detected? arXiv preprint arXiv:2303.11156,

    [Sadasivan et al., 2023] Vinu Sankar Sadasivan, Aounon Kumar, Sriram Balasubramanian, Wenxiao Wang, and So- heil Feizi. Can ai-generated text be reliably detected? arXiv preprint arXiv:2303.11156,

    2023 arXiv

  25. [42]

    Sotana: The open- source software development assistant

    [Shi et al., 2023] Ensheng Shi, Fengji Zhang, Yanlin Wang, Bei Chen, Lun Du, Hongyu Zhang, Shi Han, Dong- mei Zhang, and Hongbin Sun. Sotana: The open- source software development assistant. arXiv preprint arXiv:2308.13416,

    2023 arXiv

  26. [43]

    Mind the gap: Examining the self-improvement capabilities of large language models,

    [Song et al., 2025] Yuda Song, Hanlin Zhang, Carson Eise- nach, Sham Kakade, Dean Foster, and Udaya Ghai. Mind the gap: Examining the self-improvement capabilities of large language models,

    2025

  27. [44]

    Pde-controller: Llms for autoformalization and reasoning of pdes,

    [Soroco et al., 2025] Mauricio Soroco, Jialin Song, Mengzhou Xia, Kye Emond, Weiran Sun, and Wuyang Chen. Pde-controller: Llms for autoformalization and reasoning of pdes,

    2025

  28. [45]

    The coq proof assistant

    [Sozeau et al., ] Matthieu Sozeau, Guillaume Melquiond, and Pierre Roux. The coq proof assistant. [Tall, 1991] David Tall. Advanced mathematical thinking

    1991

  29. [47]

    Dai, Anja Hauth, and Katie Millican

    [Team et al., 2024] Gemini Team, Rohan Anil, Sebastian Borgeaud, Jean-Baptiste Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M. Dai, Anja Hauth, and Katie Millican. Gemini: A family of highly capable multimodal models,

    2024

  30. [48]

    Llama: Open and efficient foundation language models,

    [Touvron et al., 2023] Hugo Touvron, Thibaut Lavril, Gau- tier Izacard, Xavier Martinet, Marie-Anne Lachaux, Tim- oth´ee Lacroix, Baptiste Rozi`ere, Naman Goyal, Eric Ham- bro, Faisal Azhar, Aurelien Rodriguez, Armand Joulin, Edouard Grave, and Guillaume Lample. Llama: Open an...

    2023

  31. [49]

    Kimina-prover preview: Towards large formal reasoning models with re- inforcement learning,

    [Wang et al., 2025] Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jian- qiao Lu, Hugues de Saxc´e, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Z...

    2025

  32. [50]

    Jiang, Wenda Li, Markus N

    [Wu et al., 2022] Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models,

    2022

  33. [51]

    A combi- natorial identities benchmark for theorem proving via au- tomated theorem generation,

    [Xiong et al., 2025] Beibei Xiong, Hangyu Lv, Haojia Shan, Jianlin Wang, Zhengfeng Yang, and Lihong Zhi. A combi- natorial identities benchmark for theorem proving via au- tomated theorem generation,

    2025

  34. [52]

    Mathesis: Towards formal theorem proving from natural languages,

    [Xuejun et al., 2025] Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, She...

    2025

  35. [53]

    Formal mathematical reasoning: A new fron- tier in ai

    [Yang et al., 2024] Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new fron- tier in ai. arXiv preprint arXiv:2412.16075,

    2024 arXiv

  36. [54]

    Formalmath: Benchmarking formal mathematical reasoning of large language models,

    [Yu et al., 2025] Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, and Weiyang Liu. Formalmath: Benchmarking formal mathematical reasoning of large language models,

    2025

  37. [55]

    Leanabell-prover: Posttrain- ing scaling in formal reasoning,

    [Zhang et al., 2025] Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-prover: Posttrain- ing scaling in formal reasoning,

    2025

  38. [56]

    Minif2f: a cross-system benchmark for formal olympiad-level mathematics,

    [Zheng et al., 2022] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics,

    2022

  39. [57]

    Lyra: Orchestrating dual correction in automated theorem proving,

    [Zheng et al., 2024] Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jian- hao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving,

    2024

  40. [58]

    Knowledge augmented com- plex problem solving with large language models: A sur- vey

    [Zheng et al., 2025] Da Zheng, Lun Du, Junwei Su, Yuchen Tian, Yuqi Zhu, Jintian Zhang, Lanning Wei, Ningyu Zhang, and Huajun Chen. Knowledge augmented com- plex problem solving with large language models: A sur- vey. arXiv preprint arXiv:2505.03418,

    2025 arXiv

  41. [59]

    Step-wise formal verification for llm-based mathematical problem solving, 2025

    [Zhou and Zhang, 2025] Kuo Zhou and Lu Zhang. Step-wise formal verification for llm-based mathematical problem solving, 2025

    2025

  42. [1889]

    Improving autoformaliza- tion using type checking,

    [Poiroux et al., 2025] Auguste Poiroux, Gail Weiss, Viktor Kunˇcak, and Antoine Bosselut. Improving autoformaliza- tion using type checking,

    2025

  43. [1991]

    Machine-assisted proof

    [Tao, 2024] Terence Tao. Machine-assisted proof. Notices of the American Mathematical Society, to appear ,

    2024

  44. [2003]

    Specgen: Automated generation of for- mal program specifications via large language models

    [Ma et al., 2024] Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. Specgen: Automated generation of for- mal program specifications via large language models. corr abs/2401.08807 (2024),

    2024 arXiv

  45. [2008]

    A formal proof of the kepler conjecture,

    [Hales et al., 2015] Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nip- kow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai ...

    2015

  46. [2015]

    [Di et al., 2024] Peng Di, Jianguo Li, Hang Yu, Wei Jiang, Wenting Cai, Yang Cao, Chaoyu Chen, Dajun Chen, Hongwei Chen, Liang Chen, et al

    Springer Inter- national Publishing. [Di et al., 2024] Peng Di, Jianguo Li, Hang Yu, Wei Jiang, Wenting Cai, Yang Cao, Chaoyu Chen, Dajun Chen, Hongwei Chen, Liang Chen, et al. Codefuse-13b: A pre- trained multi-lingual code large language model. In Pro- ceedings of the 46th I...

    2024

  47. [2021]

    Auto- formalizing euclidean geometry,

    [Murphy et al., 2024] Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Auto- formalizing euclidean geometry,

    2024

  48. [2022]

    Ai achieves silver-medal stan- dard solving international 178 mathematical olympiad problems

    [AlphaProof and AlphaGeometry, 2024] Team AlphaProof and Team AlphaGeometry. Ai achieves silver-medal stan- dard solving international 178 mathematical olympiad problems. DeepMind blog, 179:45,

    2024

  49. [2023]

    Jiang, Jia Deng, Stella Biderman, and Sean Welleck

    [Azerbayev et al., 2024] Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics,

    2024

  50. [2024]

    Towards a mathematics formalisation assistant using large language models,

    [Agrawal et al., 2022] Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. Towards a mathematics formalisation assistant using large language models,

    2022

  51. [2025]

    Learning guided automated reasoning: a brief survey

    [Blaauwbroek et al., 2024] Lasse Blaauwbroek, David M Cerna, Thibault Gauthier, Jan Jakub ˘uv, Cezary Kaliszyk, Martin Suda, and Josef Urban. Learning guided automated reasoning: a brief survey. Logics and Type Systems in The- ory and Practice: Essays Dedicated to Herman Geuve...

    2024

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.