Pith. sign in

REVIEW 3 major objections 4 minor 67 references

MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?

T0 review · 3 major / 4 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 This paper introduces MATP-BENCH, a benchmark of 1,056 image-plus-text theorems formalized in Lean 4, Coq, and Isabelle, and shows that current multimodal large language models prove only a small fraction of them, with the strongest…

desk verdict Useful benchmark, but the Task 1 metric needs a theorem-fidelity check before the pass rates can be trusted. read the letter →

arxiv 2506.06034 v1 pith:PM3H4E2U submitted 2025-06-06 cs.CL

Zhitao He , Zongwei Lyu , Dazhong Chen , Dadi Guo , Yi R. Fung This is my paper
classification cs.CL MSC 03B3568V20
keywords multimodalautomatedtheoremprovingMLLMbenchmarkformalproofgeometryLean4CoqIsabellepass@10
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

MATP-BENCH is a benchmark that asks a multimodal large language model to read a diagram plus a natural-language theorem statement and produce a proof that a formal proof assistant can verify, with reference formalizations supplied in Lean 4, Coq, and Isabelle. It contains 1,056 geometry-heavy theorems from high school, university, and competition mathematics, and splits the job into end-to-end proving (Task 1) and theorem formalization only (Task 2). The paper reports that the best tested model, OpenAI-o1, reaches only 5.68 percent pass@10 on Lean 4 Task 1, with overall averages in the low single digits, while formalization succeeds far more often. The main conclusion is that current models can often convert a multimodal problem into a formal statement but cannot construct a correct formal proof; proof generation, not problem understanding, is the bottleneck. If the formalizations are faithful, the benchmark gives the field a verifiable target for measuring progress on visual-symbolic reasoning.

What carries the argument

The load-bearing object is the benchmark itself: each of 1,056 problems pairs an image with a natural-language theorem statement, and every problem has a manually written formal theorem in Lean 4, Coq, and Isabelle. The key mechanism is that diagram-only facts are turned into explicit hypotheses in the formal statements, such as axioms stating that a point lies on an extended line or that certain points are distinct and non-collinear, so a model genuinely needs the image to reconstruct the theorem. The evaluation isolates where failure happens by splitting the task into Task 1, generate a formal theorem and a verifiable proof, and Task 2, generate only the formal theorem, measured by pass@10, the fraction of problems a model solves within ten attempts.

What would settle it

Take a sample of MATP-BENCH theorems, delete every axiom that is labeled as derived from the diagram, and run the same provers; if a large fraction of the formal theorems still go through, the benchmark's central claim that images carry indispensable hypotheses would be false.

Watch

Extended reading notes

Core claim

The paper's central discovery is that multimodal automated theorem proving fails at the proof-construction stage, not the formalization stage. On MATP-BENCH's Task 1, in which a model must generate both the formal theorem and its proof from an image and a natural-language statement, the strongest reported result is OpenAI-o1 at 5.68 percent pass@10 on Lean 4, with all models in the low single digits overall. In contrast, Task 2, which asks only for the formal theorem statement, succeeds at roughly ten times that rate, and the error analysis shows the same failure modes across models: unproven proof steps, missing preconditions and hidden assumptions, and under-use of diagram information. Models do attempt auxiliary constructions such as auxiliary lines, and they attempt them more often on harder problems, but they rarely turn those constructions into completed proofs. The paper concludes that visual-symbolic joint reasoning and the construction of correct formal proofs are the open challenges that MATP-BENCH is designed to expose.

Load-bearing premise

The benchmark's conclusions rest on the assumption that the manually written formal theorems faithfully capture all diagram information and none of the answer; if a formalization omits a diagram condition, adds a wrong one, or leaks the known answer, the reported pass rates would measure the wrong thing.

Editorial extensions

If this is right

  • MATP-BENCH makes automated theorem proving measurable in a multimodal setting, since every claimed proof is checked by a formal proof assistant rather than by a judge or by answer matching.
  • The large Task 1 versus Task 2 gap implies that improving proof-search strategies, not better visual perception or formalization, should be the first target for models on this benchmark.
  • Because the better models attempt auxiliary constructions more often as difficulty increases but almost never complete them, methods that make auxiliary-line generation productive could produce the largest gains.
  • Reported capability is sensitive to the formal language: Coq, with its mature tactic library, is easier for current models than Lean 4 and Isabelle, so benchmark results should be compared within the same language.

Reading between the lines

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

  • A natural next experiment the paper does not run is to feed a model the natural-language statement without the image; if pass rates stay nearly as high, MATP-BENCH would not yet be forcing multimodal reasoning.
  • Equally, a model that first formalizes the theorem and then hands the formal statement to an external proof search could lift Task 1 scores without any improvement in visual understanding, a confound future users of the benchmark should check.
  • Re-formalizing a random sample of problems independently, blind to the answers, would test whether the manually written formalizations are complete and uncontaminated; the paper reports only that each formalization is reviewed by one other team member.
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

3 major / 4 minor

Summary. The paper introduces MATP-BENCH, a benchmark of 1,056 multimodal mathematics problems (predominantly geometry) with formal theorem statements in Lean 4, Coq, and Isabelle. It defines two tasks: Task 1 (end-to-end theorem formalization plus proof generation from an image and a natural-language statement, verified by the formal proof checker) and Task 2 (formalization only, with outputs judged by GPT-4o against the annotated ground truth). Six multimodal LLMs are evaluated. The main reported finding is that Task 1 success is low (e.g., 5.68% pass@10 for o1 in Lean 4), while Task 2 formalization success is substantially higher, leading the authors to conclude that the primary bottleneck is proof generation rather than formalization.

Significance. If the evaluation protocol is valid, MATP-BENCH is a useful first multi-language multimodal automated-theorem-proving benchmark; the public release of 1,056 problems formalized in Lean 4, Coq, and Isabelle is a substantial resource. The paper's qualitative conclusion—that current MLLMs solve very few end-to-end multimodal theorems—is likely robust, and the error analysis (Figure 2) and auxiliary-construction analysis (Figure 4) provide useful insights. The authors are to be credited for releasing the dataset and for using machine-checked proof verification in three proof assistants. However, the quantitative validity of the benchmark hinges on the semantic-equivalence check in Task 1 and on the reliability of the GPT-4o judge in Task 2, both of which are underspecified in the manuscript.

major comments (3)
  1. [Section 5.1 Metrics; Section 3 Preventing Modality Leakage] The Task 1 pass@10 metric counts a success when Check(T,P)=True for the model-generated theorem T, but the manuscript never states that T is automatically compared with the annotated ground-truth formal statement. The 'Preventing Modality Leakage' paragraph in Section 3 promises a formal theorem verification task, yet Section 5.1 only describes a GPT-4o judge for Task 2; no equivalent filter is described for Task 1. As written, a model can output a trivial theorem (e.g., True) with a one-line proof and be counted as a pass, so the reported Task 1 rates are upper bounds on solving the actual multimodal problems. Please specify the statement-equivalence check and re-report Task 1 results after applying it.
  2. [Section 5.1 Metrics; Table 4] Task 2 uses GPT-4o as the judge to assess whether the generated formal theorem is consistent with the ground truth, but no human agreement study, calibration sample, or error analysis for this judge is reported. Because the paper's main bottleneck conclusion rests on the large gap between Task 2 (e.g., 45.16% overall average in Table 4 for Lean 4) and Task 1 (4.26% in Table 3), a lenient or biased judge would distort the interpretation. Please provide a human-annotated validation subset and report judge accuracy or a kappa-style agreement statistic.
  3. [Section 4 Formalization Effort and Challenges] The ground-truth formalizations are the scoring target for both tasks, but the paper reports only that formalizations were done 'case-by-case' and 'reviewed by at least one other team member.' There is no inter-annotator reliability measure, no independent audit of diagram-derived hypotheses (e.g., the 'From diagram' axioms in Figure 1), and no cross-language consistency check among the Lean, Coq, and Isabelle versions. A missing or erroneous diagram premise would directly change problem difficulty and solve rates, affecting the benchmark's validity as an evaluation tool. Please add a validation protocol, such as independent re-formalization of a sample, cross-language equivalence checks, or a statement-level review log.
minor comments (4)
  1. [Tables 3 and 4] The header 'Avg.OpenAI-o1' is ambiguous: the numeric rows indicate that the average is the last column (e.g., 6.39 is the mean of 7.63, 7.20, 8.47, 9.32, 2.12, 3.58 for Lean high school), but the header places 'Avg.' at the beginning. Several table entries are also run together (e.g., '8.479.322.12' should be '8.47 9.32 2.12'). Please fix the column alignment and separator issues in Tables 3 and 4, and check the same issue in Tables 5-8.
  2. [Section 5.2 Main results] The first paragraph reports average difficulty-level rates of 6.96%, 3.12%, and 2.08%, which do not match Table 3: the Lean 4 averages are 6.39%, 2.85%, and 1.29%, and cross-language averages differ as well. Please reconcile the prose with the tables.
  3. [Section 5.2 Main results] Additional numerical inconsistencies appear throughout Section 5.2: the Coq Task 1 overall rate is given as 12.86% (Table 3: 12.15%), Lean 4 Task 1 as 4.68% (Table 3: 4.26%), Lean 4 Task 2 as 46.81% (Table 4: 45.16%), and Isabelle Task 1 as 4.71% (Table 3: 4.65%). Please correct these values or explain the different aggregation method if one is intended.
  4. [Section 5.1 Metrics; Tables 3-8] No error bars or confidence intervals are reported for the pass@n estimates. Some model comparisons are close (e.g., Lean 4 Task 1 overall: o1 5.68% vs. GPT-4.1 5.87%), so please add bootstrap confidence intervals or explicitly state which differences are within noise.

Circularity Check

1 steps flagged · score 6.0 of 10

Task 1's pass@10 is self-referential: the model supplies both theorem and proof, and success is defined as Check(T,P)=True, so a trivial self-written theorem can count as a solve.

  1. self definitional [Section 3 (Problem Formulation) and Section 5.1 (Experimental settings, Metrics)]
    "ProverM AT P(I, S)→(T, P),whereCheck(T, P) =True. ... For Task 1, which requires the model to generate both a correct formal theorem and its proof, we follow prior studies [62; 49; 24] and adopt pass@ n (n=10) as the evaluation metric. This metric evaluates whether the prover can successfully complete a valid proof within n attempts in the formal proof environment."

    In a standard ATP benchmark, the theorem T is a fixed input, so pass@n measures proof of the target statement. Here, Section 3 makes T an output of the model (Prover(I,S)->(T,P)) and the only stated condition is Check(T,P)=True. The Section 5.1 metric repeats only 'complete a valid proof within n attempts in the formal proof environment' and never states that T is compared to the annotated ground-truth theorem or filtered for semantic equivalence. Consequently, a model may emit a trivial theorem such as True with a one-line proof and be counted as a pass. The measured 'solve rate' is therefore by construction the rate of proving a model-selected statement, not the rate of proving the multimodal problem.

full rationale

MATP-BENCH's construction is otherwise not circular: the 1056 problems come from external datasets and public Olympiad examinations, the formal statements are human-authored in Lean 4, Coq, and Isabelle and reviewed by another team member, and Task 2's formalization scores are measured against an annotated ground truth with a GPT-4o judge. No fitted parameters or derived laws are involved. The sole load-bearing circular element is the Task 1 metric: because the theorem T is generated by the model and the stated criterion is only Check(T,P)=True, a pass does not by construction require T to equal the benchmark's annotated theorem. The paper says in Section 3 that a 'formal theorem verification task' is incorporated to prevent arbitrary fabrication, but Section 5.1 reports that judge only for Task 2, and the Task 1 pass rates are not reported as being filtered for semantic equivalence. This makes the central Task 1 solve rates self-referential upper bounds: they measure proof of the model's own statement, not proof of the stated multimodal problem. The self-citation [54] shares an author (Yi R. Fung) but is used only as general motivation and is not load-bearing. The qualitative conclusion that current MLLMs struggle with multimodal theorem proving probably survives even after re-scoring, but the exact pass@n numbers and the bottleneck analysis would need a semantic-equivalence filter before they can be read as proof-generation performance.

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

The benchmark's validity rests on domain assumptions about formalization faithfulness and the LLM judge, but no free parameters or invented entities are introduced.

assumptions (3)
  • domain assumption The manually authored formal theorem statements are faithful and complete translations of each multimodal problem, including all diagram-derived hypotheses.
    Section 4 states formalizations were done manually and reviewed in-team; no independent or automated check of statement faithfulness is described.
  • domain assumption The correct answer provided in source datasets can be used to construct theorem statements for MCQ and fill-in-the-blank questions without changing problem semantics.
    Section 4 describes converting question formats into declarative theorems using the correct answer, which may leak the answer into the theorem target.
  • domain assumption GPT-4o judge reliably assesses consistency between model-generated formal theorems and ground truth.
    Section 5.1: Task 2 uses GPT-4o as judge; no human agreement or calibration is reported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?." pith.science (2026). https://pith.science/paper/PM3H4E2U

@misc{pith2026250606034,
  author       = {Pith},
  title        = {Pith review of: MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PM3H4E2U}},
  note         = {Machine review of arXiv:2506.06034}
}
read the original abstract

Numerous theorems, such as those in geometry, are often presented in multimodal forms (e.g., diagrams). Humans benefit from visual reasoning in such settings, using diagrams to gain intuition and guide the proof process. Modern Multimodal Large Language Models (MLLMs) have demonstrated remarkable capabilities in solving a wide range of mathematical problems. However, the potential of MLLMs as Automated Theorem Provers (ATPs), specifically in the multimodal domain, remains underexplored. In this paper, we introduce the Multimodal Automated Theorem Proving benchmark (MATP-BENCH), a new Multimodal, Multi-level, and Multi-language benchmark designed to evaluate MLLMs in this role as multimodal automated theorem provers. MATP-BENCH consists of 1056 multimodal theorems drawn from high school, university, and competition-level mathematics. All these multimodal problems are accompanied by formalizations in Lean 4, Coq and Isabelle, thus making the benchmark compatible with a wide range of theorem-proving frameworks. MATP-BENCH requires models to integrate sophisticated visual understanding with mastery of a broad spectrum of mathematical knowledge and rigorous symbolic reasoning to generate formal proofs. We use MATP-BENCH to evaluate a variety of advanced multimodal language models. Existing methods can only solve a limited number of the MATP-BENCH problems, indicating that this benchmark poses an open challenge for research on automated theorem proving.

Figures

Figures reproduced from arXiv: 2506.06034 by the authors.

Figure 1
Figure 1. We illustrate the differences between traditional ATP and MATP through examples from miniF2F (above) and MATPBENCH (below). Multimodal theorems consist of an image paired with a natural language theorem statement, which complement each other to convey complete theorem information. Furthermore, additional auxiliary constructions are often essential for their proof (as shown in the bottom left subfigure). In tradition… view at source ↗
Figure 2
Figure 2. We perform an error analysis on the results of a reasoning model (Claude-3.7-Sonnet-Thinking) and two non-reasoning models (GPT4.1 and Qwen2.5-VL-Instruct-70B) , all three being competitive on MATP tasks (Lean 4), with the figure illustrating the seven most frequent error types. severe than in Lean 4. The o1 model ranks first with an overall success rate of 19.43%, performing particularly well at the high school lev… view at source ↗
Figure 3
Figure 3. We present the performance of different MLLMs (Gemini-2.0-flash-thinking, OpenAI-GPT4.1, and Qwen2.5-VL-Instruct-70B) on multimodal theorem automated proving (Task 1) and theorem formalization (Task 2) across varying difficulty levels, evaluated using Pass@1, Pass@5, and Pass@10 metrics. generally increases the success rate. However, the pass@n success rate for Task 1 is significantly lower than the pass@n success r… view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Auxiliary construction analysis by question difficulty level and model, evaluated using Pass@10. A characteristic distinguishing multimodal the￾orem proving from pure text theorem proving is that many theorems require the construction of auxiliary lines to aid thinking…
Figure 5
Figure 5. Figure 5: An example of a high school level mathematics problem, requiring the calculation of a triangle’s area within a configuration of two adjacent squares (ABGH and BCDF) of differing side lengths [PITH_FULL_IMAGE:figures/full_fig_p015_5.png]
Figure 6
Figure 6. Figure 6: An example of a university level mathematics problem, requiring the determination that the number of non-repeating paths from the top to bottom vertex of a regular icosahedron, under downward or horizontal movement constraints, is 810. 15 [PITH_FULL_IMAGE:figures/full…
Figure 7
Figure 7. Figure 7: We present the performance of different MLLMs (Gemini-2.0-flash-thinking, OpenAI-GPT4.1, and Qwen2.5-VL-Instruct-70B) on multimodal automated theorem proving task across varying difficulty levels, evaluated using Pass@1, Pass@5, and Pass@10 metrics. D Performance Compa…
Figure 8
Figure 8. Figure 8: Prompt for multimodal automated theorem proving task (part1). 20 [PITH_FULL_IMAGE:figures/full_fig_p020_8.png]
Figure 9
Figure 9. Figure 9: Prompt for multimodal automated theorem proving task (part2). 21 [PITH_FULL_IMAGE:figures/full_fig_p021_9.png]
Figure 10
Figure 10. Figure 10: Prompt for multimodal theorem formalization task. 22 [PITH_FULL_IMAGE:figures/full_fig_p022_10.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

67 extracted references · 27 canonical work pages

  1. [1]

    Mathqa: Towards interpretable math word problem solving with operation-based formalisms.arXiv preprint arXiv:1905.13319, 2019

    Aida Amini, Saadia Gabriel, Peter Lin, Rik Koncel-Kedziorski, Yejin Choi, and Hannaneh Hajishirzi. Mathqa: Towards interpretable math word problem solving with operation-based formalisms.arXiv preprint arXiv:1905.13319, 2019. URL https://arxiv.org/abs/1905. 13319

    arXiv 1905

  2. [2]

    Claude Sonnet

    Anthropic. Claude Sonnet. https://www.anthropic.com/claude/sonnet, 2024. Ac- cessed: 2025-04-29

    work page 2024

  3. [3]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics.arXiv preprint arXiv:2302.12433, 2023

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics.arXiv preprint arXiv:2302.12433, 2023. URL https://arxiv.org/abs/2302. 12433

    arXiv 2023

  4. [4]

    Llemma: An open language model for mathematics.arXiv preprint arXiv:2310.10631, 2023

    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.arXiv preprint arXiv:2310.10631, 2023. URL https://arxiv.org/ abs/2310.10631

    arXiv

  5. [5]

    Springer Science & Business Me- dia, 2013

    Wolfgang Bibel.Automated theorem proving. Springer Science & Business Me- dia, 2013. URL https://books.google.com.hk/books?hl=zh-CN&lr=&id= MNcACAAAQBAJ&oi=fnd&pg=PR5&dq=Automated+theorem+proving&ots=eFxi0-SoaB& sig=2dh8ZtPhDfhfmxFjt8ncsQ1HT1k&redir_esc=y#v=onepage&q=Automated% 20theorem%20proving&f=false

    work page 2013

  6. [6]

    An augmented benchmark dataset for geometric question answering through dual parallel text encoding

    Jie Cao and Jing Xiao. An augmented benchmark dataset for geometric question answering through dual parallel text encoding. InProceedings of the 29th international conference on computational linguistics, pages 1511–1520, 2022. URL https://aclanthology.org/ 2022.coling-1.130/

    work page 2022

  7. [7]

    Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression.arXiv preprint arXiv:2212.02746, 2022

    Jiaqi Chen, Tong Li, Jinghui Qin, Pan Lu, Liang Lin, Chongyu Chen, and Xiaodan Liang. Unigeo: Unifying geometry logical reasoning via reformulating mathematical expression.arXiv preprint arXiv:2212.02746, 2022. URLhttps://arxiv.org/abs/2212.02746

    arXiv 2022

  8. [8]

    Towards reasoning era: A survey of long chain-of-thought for reasoning large language models.arXiv preprint arXiv:2503.09567, 2025

    Qiguang Chen, Libo Qin, Jinhao Liu, Dengyun Peng, Jiannan Guan, Peng Wang, Mengkang Hu, Yuhang Zhou, Te Gao, and Wanxiang Che. Towards reasoning era: A survey of long chain-of-thought for reasoning large language models.arXiv preprint arXiv:2503.09567, 2025. URLhttps://arxiv.org/abs/2503.09567

    arXiv 2025

Show all 67 references
  1. [9]

    MIT Press, 2013

    Adam Chlipala.Certified programming with dependent types: a pragmatic introduction to the Coq proof assistant. MIT Press, 2013. URLhttp://adam.chlipala.net/cpdt/

    2013

  2. [10]

    Training verifiers to solve math word problems.arXiv preprint arXiv:2110.14168, 2021

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems.arXiv preprint arXiv:2110.14168, 2021. URL https://arxiv. org/abs/2110.14168. 10

    arXiv

  3. [11]

    Compfiles

    compfiles. Compfiles. https://github.com/dwrensha/compfiles, 2023. Accessed: [2025-04-25]

    2023

  4. [12]

    Start building with gemini 2.5 flash

    Tulsee Doshi. Start building with gemini 2.5 flash. https://developers.googleblog. com/en/start-building-with-gemini-25-flash/, April 2025. Accessed: 2025-04-29

    2025

  5. [13]

    Mathematical capabilities of chatgpt.Advances in neural information processing systems, 36:27699–27744,

    Simon Frieder, Luca Pinchetti, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Petersen, and Julius Berner. Mathematical capabilities of chatgpt.Advances in neural information processing systems, 36:27699–27744,

  6. [15]

    Measuring massive multitask language understanding.arXiv preprint arXiv:2009.03300, 2020

    Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. Measuring massive multitask language understanding.arXiv preprint arXiv:2009.03300, 2020. URLhttps://arxiv.org/abs/2009.03300

    2009 arXiv

  7. [16]

    Measuring mathematical problem solving with the math dataset

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021. URLhttps://arxiv.org/abs/2103.03874

    2021 arXiv

  8. [17]

    Visual sketchpad: Sketching as a visual chain of thought for multimodal language models.arXiv preprint arXiv:2406.09403, 2024

    Yushi Hu, Weijia Shi, Xingyu Fu, Dan Roth, Mari Ostendorf, Luke Zettlemoyer, Noah A Smith, and Ranjay Krishna. Visual sketchpad: Sketching as a visual chain of thought for multimodal language models.arXiv preprint arXiv:2406.09403, 2024. URL https://arxiv.org/abs/ 2406.09403

    2024 arXiv

  9. [18]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.arXiv preprint arXiv:2210.12283, 2022

    Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs.arXiv preprint arXiv:2210.12283, 2022. URL https: //arxiv.org/ab...

    arXiv

  10. [19]

    Lisa: Language models of isabelle proofs

    Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In6th Conference on Artificial Intelligence and Theorem Proving, pages 378–392, 2021. URLhttps://aitp-conference.org/2021/abstract/paper_17.pdf

    2021

  11. [20]

    Hypertree proof search for neural theorem proving.Advances in neural information processing systems, 35:26337– 26349, 2022

    Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving.Advances in neural information processing systems, 35:26337– 26349, 2022. URL https:/...

    2022

  12. [21]

    Perception, reason, think, and plan: A survey on large multimodal reasoning models.arXiv preprint arXiv:2505.04921, 2025

    Yunxin Li, Zhenyu Liu, Zitao Li, Xuanyu Zhang, Zhenran Xu, Xinyu Chen, Haoyuan Shi, Shenyuan Jiang, Xintong Wang, Jifang Wang, et al. Perception, reason, think, and plan: A survey on large multimodal reasoning models.arXiv preprint arXiv:2505.04921, 2025. URL https://arxiv.org...

    2025 arXiv

  13. [22]

    Goedel-prover: A frontier model for open-source automated theorem proving.arXiv preprint arXiv:2502.07640, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving.arXiv preprint arXiv:2502.07640, 2025. URL https://arxiv. org/abs/2502.07640

    2025 arXiv

  14. [23]

    Program induction by ratio- nale generation: Learning to solve and explain algebraic word problems.arXiv preprint arXiv:1705.04146, 2017

    Wang Ling, Dani Yogatama, Chris Dyer, and Phil Blunsom. Program induction by ratio- nale generation: Learning to solve and explain algebraic word problems.arXiv preprint arXiv:1705.04146, 2017. URLhttps://arxiv.org/abs/1705.04146

    2017 arXiv

  15. [24]

    Fimo: A challenge formal dataset for automated theorem proving, 2023

    Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, and Qun Liu. Fimo: A challenge formal dataset for automated theorem proving, 2023. URL https://arxiv.org/abs/2309.04295. 11

    2023 arXiv

  16. [25]

    Improved baselines with visual instruction tuning, 2023

    Haotian Liu, Chunyuan Li, Yuheng Li, and Yong Jae Lee. Improved baselines with visual instruction tuning, 2023. URL https://openaccess.thecvf.com/content/CVPR2024/ html/Liu_Improved_Baselines_with_Visual_Instruction_Tuning_CVPR_2024_ paper.html

    2023

  17. [26]

    Cmm-math: A chinese multimodal math dataset to evaluate and enhance the mathematics reasoning of large multimodal models.arXiv preprint arXiv:2409.02834, 2024

    Wentao Liu, Qianjun Pan, Yi Zhang, Zhuo Liu, Ji Wu, Jie Zhou, Aimin Zhou, Qin Chen, Bo Jiang, and Liang He. Cmm-math: A chinese multimodal math dataset to evaluate and enhance the mathematics reasoning of large multimodal models.arXiv preprint arXiv:2409.02834, 2024. URLhttps:...

    2024 arXiv

  18. [27]

    Inter-gps: Interpretable geometry problem solving with formal language and symbolic reasoning.arXiv preprint arXiv:2105.04165, 2021

    Pan Lu, Ran Gong, Shibiao Jiang, Liang Qiu, Siyuan Huang, Xiaodan Liang, and Song-Chun Zhu. Inter-gps: Interpretable geometry problem solving with formal language and symbolic reasoning.arXiv preprint arXiv:2105.04165, 2021. URL https://arxiv.org/abs/2105. 04165

    2021 arXiv

  19. [28]

    Mathvista: Evaluating mathematical reasoning of foundation models in visual contexts.arXiv preprint arXiv:2310.02255, 2023

    Pan Lu, Hritik Bansal, Tony Xia, Jiacheng Liu, Chunyuan Li, Hannaneh Hajishirzi, Hao Cheng, Kai-Wei Chang, Michel Galley, and Jianfeng Gao. Mathvista: Evaluating mathematical reasoning of foundation models in visual contexts.arXiv preprint arXiv:2310.02255, 2023. URLhttps://ar...

    arXiv

  20. [29]

    Chartqa: A benchmark for question answering about charts with visual and logical reasoning.arXiv preprint arXiv:2203.10244, 2022

    Ahmed Masry, Do Xuan Long, Jia Qing Tan, Shafiq Joty, and Enamul Hoque. Chartqa: A benchmark for question answering about charts with visual and logical reasoning.arXiv preprint arXiv:2203.10244, 2022. URLhttps://arxiv.org/abs/2203.10244

    2022 arXiv

  21. [30]

    Lila: A unified benchmark for mathematical reasoning.arXiv preprint arXiv:2210.17517, 2022

    Swaroop Mishra, Matthew Finlayson, Pan Lu, Leonard Tang, Sean Welleck, Chitta Baral, Tanmay Rajpurohit, Oyvind Tafjord, Ashish Sabharwal, Peter Clark, et al. Lila: A unified benchmark for mathematical reasoning.arXiv preprint arXiv:2210.17517, 2022. URL https: //arxiv.org/abs/...

    arXiv

  22. [31]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. InAutomated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28, pages 625–635. Springer, 2021. URLhttps://link.spr...

    2021 doi

  23. [32]

    Autoformalizing euclidean geometry.arXiv preprint arXiv:2405.17216, 2024

    Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing euclidean geometry.arXiv preprint arXiv:2405.17216, 2024. URL https: //arxiv.org/abs/2405.17216

    2024 arXiv

  24. [33]

    GPT-4.1.https://openai.com/index/gpt-4-1/, 2024

    OpenAI. GPT-4.1.https://openai.com/index/gpt-4-1/, 2024. Accessed: 2025-04-29

    2024

  25. [34]

    Introducing o3 and o4-mini

    OpenAI. Introducing o3 and o4-mini. https://openai.com/index/ introducing-o3-and-o4-mini/, 2024. Accessed: 2025-04-29

    2024

  26. [35]

    Generative language modeling for automated theorem proving

    Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. URLhttps://arxiv.org/abs/2009.03393

    2009 arXiv

  27. [37]

    Artificial intelligence mathematical olympiad (aimo) prize, 2023

    AIMO Prize. Artificial intelligence mathematical olympiad (aimo) prize, 2023. URL https: //aimoprize.com/

    2023

  28. [38]

    A survey of efficient reasoning for large reasoning models: Language, multimodality, and beyond.arXiv preprint arXiv:2503.21614, 2025

    Xiaoye Qu, Yafu Li, Zhaochen Su, Weigao Sun, Jianhao Yan, Dongrui Liu, Ganqu Cui, Daizong Liu, Shuxian Liang, Junxian He, et al. A survey of efficient reasoning for large reasoning models: Language, multimodality, and beyond.arXiv preprint arXiv:2503.21614, 2025. URL https://a...

    2025

  29. [39]

    Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.arXiv preprint arXiv:2504.21801, 2025

    ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.arXiv preprint arXiv:2504.21801, 20...

    2025 arXiv

  30. [40]

    Elsevier,

    Alan JA Robinson and Andrei V oronkov.Handbook of automated reasoning, volume 1. Elsevier,

  31. [41]

    Imo grand challenge.URL https://imo-grand-challenge

    Daniel Selsam, Leonardo de Moura, Kevin Buzzard, Reid Barton, Percy Liang, Sarah Loos, and Freek Wiedijk. Imo grand challenge.URL https://imo-grand-challenge. github. io, 2020. URL https://imo-grand-challenge.github.io

    2020

  32. [42]

    Solving geometry problems: Combining text and diagram interpretation

    Minjoon Seo, Hannaneh Hajishirzi, Ali Farhadi, Oren Etzioni, and Clint Malcolm. Solving geometry problems: Combining text and diagram interpretation. InProceedings of the 2015 conference on empirical methods in natural language processing, pages 1466–1476, 2015. URL https://ac...

    2015

  33. [43]

    Deepseekmath: Pushing the limits of mathematical reasoning in open language models.arXiv preprint arXiv:2402.03300, 2024

    Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang, Mingchuan Zhang, YK Li, Y Wu, et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models.arXiv preprint arXiv:2402.03300, 2024. URL https: //arxiv.org/abs/2402.03300

    2024 arXiv

  34. [44]

    Math-llava: Bootstrapping mathematical reasoning for multimodal large language models.arXiv preprint arXiv:2406.17294, 2024

    Wenhao Shi, Zhiqiang Hu, Yi Bin, Junhua Liu, Yang Yang, See-Kiong Ng, Lidong Bing, and Roy Ka-Wei Lee. Math-llava: Bootstrapping mathematical reasoning for multimodal large language models.arXiv preprint arXiv:2406.17294, 2024. URL https://arxiv.org/abs/ 2406.17294

    2024 arXiv

  35. [45]

    What does clip know about a red circle? visual prompt engineering for vlms

    Aleksandar Shtedritski, Christian Rupprecht, and Andrea Vedaldi. What does clip know about a red circle? visual prompt engineering for vlms. InProceedings of the IEEE/CVF International Conference on Computer Vision, pages 11987–11997, 2023. URL https://openaccess.thecvf.com/co...

    2023

  36. [46]

    Qwen2.5-vl, January 2025

    Qwen Team. Qwen2.5-vl, January 2025. URL https://qwenlm.github.io/blog/qwen2. 5-vl/

    2025

  37. [47]

    An in-context learning agent for formal theorem-proving.arXiv preprint arXiv:2310.04353, 2023

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving.arXiv preprint arXiv:2310.04353, 2023. URLhttps://arxiv.org/abs/2310.04353

    2023 arXiv

  38. [48]

    Solving olympiad geometry without human demonstrations.Nature, 625(7995):476–482, 2024

    Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations.Nature, 625(7995):476–482, 2024. URL https://www. nature.com/articles/s41586-023-06747-5

    2024

  39. [49]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition.arXiv preprint arXiv:2407.11214, 2024

    George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition.arXiv preprint arXiv:2407.11214, 2024. URL https://arxiv.org/a...

    2024 arXiv

  40. [50]

    Proving theorems recursively.arXiv preprint arXiv:2405.14414, 2024

    Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, et al. Proving theorems recursively.arXiv preprint arXiv:2405.14414, 2024. URLhttps://arxiv.org/abs/2405.14414

    2024 arXiv

  41. [51]

    Measuring multimodal mathematical reasoning with math- vision dataset.Advances in Neural Information Processing Systems, 37:95095–95169,

    Ke Wang, Junting Pan, Weikang Shi, Zimu Lu, Houxing Ren, Aojun Zhou, Mingjie Zhan, and Hongsheng Li. Measuring multimodal mathematical reasoning with math- vision dataset.Advances in Neural Information Processing Systems, 37:95095–95169,

  42. [52]

    Mv- math: Evaluating multimodal math reasoning in multi-visual contexts.arXiv preprint arXiv:2502.20808, 2025

    Peijie Wang, Zhong-Zhi Li, Fei Yin, Xin Yang, Dekang Ran, and Cheng-Lin Liu. Mv- math: Evaluating multimodal math reasoning in multi-visual contexts.arXiv preprint arXiv:2502.20808, 2025. URL https://openaccess.thecvf.com/content/CVPR2025/ html/Wang_MV-MATH_Evaluating_Multimod...

    2025 arXiv

  43. [53]

    Theoremllama: Transforming general-purpose llms into lean4 experts.arXiv preprint arXiv:2407.03203, 2024

    Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theoremllama: Transforming general-purpose llms into lean4 experts.arXiv preprint arXiv:2407.03203, 2024. URLhttps://arxiv.org/abs/2407.03203

    2024 arXiv

  44. [54]

    Fung, and Tong Zhang

    Ruida Wang, Yuxin Li, Yi R. Fung, and Tong Zhang. Let’s reason formally: Natural-formal hybrid reasoning enhances llm’s math capability, 2025. URL https://arxiv.org/abs/ 2505.23703

    2025

  45. [55]

    The isabelle framework

    Makarius Wenzel, Lawrence C Paulson, and Tobias Nipkow. The isabelle framework. In International Conference on Theorem Proving in Higher Order Logics, pages 33–38. Springer,

  46. [58]

    Leandojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems, 36:21573–21612, 2023

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems, 36:21573–21612, 2023. URL h...

    2023

  47. [59]

    Lean workbook: A large-scale lean problem set formalized from natural language math problems.arXiv preprint arXiv:2406.03847, 2024

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems.arXiv preprint arXiv:2406.03847, 2024. URLhttps://arxiv.org/abs/2406.03847

    2024 arXiv

  48. [60]

    Mmmu: A massive multi-discipline multimodal understanding and reasoning benchmark for expert agi

    Xiang Yue, Yuansheng Ni, Kai Zhang, Tianyu Zheng, Ruoqi Liu, Ge Zhang, Samuel Stevens, Dongfu Jiang, Weiming Ren, Yuxuan Sun, et al. Mmmu: A massive multi-discipline multimodal understanding and reasoning benchmark for expert agi. InProceedings of the IEEE/CVF Conference on Co...

    2024

  49. [61]

    Mathverse: Does your multi-modal llm truly see the diagrams in visual math problems? InEuropean Conference on Computer Vision, pages 169–186

    Renrui Zhang, Dongzhi Jiang, Yichi Zhang, Haokun Lin, Ziyu Guo, Pengshuo Qiu, Aojun Zhou, Pan Lu, Kai-Wei Chang, Yu Qiao, et al. Mathverse: Does your multi-modal llm truly see the diagrams in visual math problems? InEuropean Conference on Computer Vision, pages 169–186. Spring...

    2024

  50. [62]

    Limitations

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics.arXiv preprint arXiv:2109.00110, 2021. URL https: //arxiv.org/abs/2109.00110. 14 A Examples of questions at different levels In Figure 5 and Figure 6, w...

    2021 arXiv

  51. [63]

    URLhttps://arxiv.org/abs/2408.08152

    arXiv

  52. [65]

    URLhttps://arxiv.org/abs/2310.11441

    arXiv

  53. [71]

    Guidelines: • The answer NA means that the paper does not involve crowdsourcing nor research with human subjects

    Institutional review board (IRB) approvals or equivalent for research with human subjects Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals...

    2025

  54. [2001]

    URL https://books.google.com.hk/books?hl=zh-CN&lr=&id=HxaWA4lep_ kC&oi=fnd&pg=PP1&dq=Handbook+of+automated+reasoning&ots=SOVKBxf0Jd& sig=I1BbPB9nkIm1qEsHPsux0VqxqQU&redir_esc=y#v=onepage&q=Handbook%20of% 20automated%20reasoning&f=false

  55. [2008]

    URLhttps://link.springer.com/chapter/10.1007/978-3-540-71067-7_7

    doi

  56. [2022]

    URLhttps://arxiv.org/abs/2202.01344

    arXiv

  57. [2023]

    URL https://proceedings.neurips.cc/paper_files/paper/2023/hash/ 58168e8a92994655d6da3939e7cc0918-Abstract-Datasets_and_Benchmarks.html

    2023

  58. [2024]

    URL https://proceedings.neurips.cc/paper_files/paper/2024/hash/ ad0edc7d5fa1a783f063646968b7315b-Abstract-Datasets_and_Benchmarks_Track. html

    2024

  59. [2025]

    URLhttps://arxiv.org/abs/2504.15780

Pith tools

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