RESEARCH DOSSIER
Mathematical Reasoning and Language Models
Abstract. Mathematical reasoning by language models is a problem of production, interpretation, and certification. Systems trained to predict and generate linguistic sequences can solve mathematical questions, produce coherent-looking derivations, call symbolic tools, and increasingly participate in proof construction and formalization. Their achievements are observable; the epistemic status of an individual output must be established by examining the proposition, the inferential steps, the method of checking, and the relation between informal mathematics and formal representation. This monograph studies original benchmark papers, experiments on chain-of-thought and reasoning robustness, process and outcome verification, reinforcement learning, program-aided calculation, neural theorem proving, mathematical competition records, and the 2026 formalization of Fermat's Last Theorem. It develops an original comparative analysis of answer correctness, inferential validity, explanatory adequacy, and verification provenance, without proposing a new named theory or reporting an unperformed experiment. Worked elementary cases demonstrate how a plausible intermediate step can invalidate an argument, how quantifiers change the theorem being proved, and why kernel checking requires semantic scrutiny of the formal statement. The central conclusion is that language-model mathematical work should be evaluated by the mathematical object delivered and by the publicly reproducible evidence supporting it. This conception accommodates genuine advances in artificial mathematical practice while preserving the distinctions that make mathematical knowledge assessable.
Keywords: Mathematical reasoning; large language models; proof; chain-of-thought; verification; theorem proving; Lean; GSM8K; MATH; mathematical hallucinations; mathematical epistemology; formalization; Artificial Era; provenance.
Introduction and research question
The mathematical outputs of language models now range from arithmetic answers to natural-language proofs and formal proof objects. The difference between these products matters because each establishes a different kind of mathematical claim. A correct numerical answer settles a particular instance. A valid derivation establishes the answer under stated assumptions. A formal certificate establishes that a specified formal statement is derivable under the rules accepted by a proof checker. An explanatory proof additionally makes a result intelligible to an audience with the relevant mathematical background. These are complementary achievements with different evidentiary requirements.
This dossier asks: How should language-model mathematical outputs be assessed? The question belongs to the philosophy of mathematics because the assessment concerns mathematical truth, proof, inference, objectivity, error, and public justification. It also belongs to the empirical study of computation because particular systems have measurable behavior under tests. Modern benchmark authors already distinguish final-answer success from proof production, as illustrated by the FormalMATH evaluation (Yu et al., 2026). The argument developed here is that mathematical authority attaches to propositions and their warrant, while authorship, generation method, and institutional context explain how those propositions reached inspection.
The study takes the emergence of competent artificial mathematical work seriously. It treats claimed accuracy as a result tied to a dataset and protocol, and validity as a property whose assessment must be directed at the actual mathematical content. Every large model performance claim requires its own date, evaluation regime, and source-specific qualification. Mathematical reasoning as such is a broader horizon than any leaderboard.
Sources, method, and evidentiary scope
The method combines critical reading of research papers and official technical documentation, comparative analysis of experimental protocols, mathematical reconstruction of selected elementary examples, and philosophical examination of what the resulting evidence establishes. The corpus spans benchmark introduction papers, studies reporting perturbation experiments, conference publications on reasoning and formal verification, laboratory reports on mathematical achievements, and relevant independently reported scientific journalism. It includes 2026 peer-reviewed work because assessment of this subject changes quickly.
The source base is stratified. Peer-reviewed articles support the claims made in their published abstracts and accessible research presentations; the authors' empirical interpretations are attributed to them. An institutional announcement is evidence that an organization reported a result, and its details can be corroborated where another source is available. Official Lean reference documentation states the software's proof-checking architecture. The 2026 Fermat formalization report is treated as an original project account, supplemented by contemporaneous external reporting.
This is a critical integrative monograph, not a new experimental benchmarking study. I did not train a model, obtain a hidden competition solution set, run formal theorem-prover experiments, or audit millions of lines of Lean code. Arithmetic examples and logical reconstructions below are independently checkable demonstrations, not empirical findings about model frequencies. The evidence ledger records the support and access scope of each citation. Whenever a numeric result appears, it is bound to the reported experiment rather than promoted into a timeless property of language models.
What counts as mathematical reasoning?
Mathematical reasoning connects explicit assumptions to conclusions through relations whose preservation can be examined. It includes calculation, algebraic transformation, construction, analogy, proof by cases, induction, contradiction, model finding, counterexample search, and interpretation of a formal statement. A system may contribute to these activities by proposing a lemma, translating a word problem, constructing a proof term, or rejecting a flawed argument. The epistemic standard depends on which contribution is at issue.
The history of automatic theorem proving demonstrates that search and logical validity are separable operations: heuristics select promising paths while a checker can decide whether a proof step is admitted. Recent accounts such as Asperti, Naibo, and Sacerdoti Coen's study of reasoning machines (2026) examine the relationship between informal mathematical language and formal symbolic languages. Their distinction allows an analysis of model reasoning without substituting a metaphysical answer about thought for the evaluation of specific proofs.
A useful inquiry begins by identifying the mathematical task precisely. Solving for x under a stated domain, answering a multiple-choice problem, giving an informal justification, and finding a formal proof inhabit different spaces of acceptable outputs. What succeeds in one space may be irrelevant to another. Correct classification is already a significant act of mathematical evaluation, because an evaluator who rewards only answer strings cannot determine whether a purported general theorem follows.
Language modeling and mathematical structure
Large language models learn statistical regularities over sequences and can acquire representations useful for mathematical language, including algebraic notation, proof templates, program syntax, and problem decomposition. Their next-token training objective by itself imposes no guarantee that each subsequent transformation preserves truth. Improvements in instruction following, reasoning-oriented training, additional inference computation, retrieval, and tool use can materially alter what the system accomplishes. The research question therefore concerns actual methods, rather than an invariant limitation inferred from the earliest training objective.
The DeepSeekMath study (Shao et al., 2024) illustrates how mathematics-specific data and reinforcement-learning techniques improve benchmark performance. Its reported 51.7% result on MATH refers to the authors' evaluated 7-billion-parameter system and setting; it describes neither all mathematical reasoning nor all subsequent model families. Progress can be genuine while residual error remains substantial on carefully selected tasks.
A philosophical interpretation should avoid reading the surface fluency of a generated argument as direct evidence of the mechanism that produced it. Mathematical structures appearing in text are representations that can be interrogated independently. The argument 'every step is correct' is an additional proposition requiring a check. Consequently, assessment should proceed from the definition of the task, through the mathematical statement expressed, to validation of the inferential operation, and finally to documentation of the generation and checking process.
Answers, arguments, and certified proofs
Consider three outputs to the question whether the sum of the first n positive odd integers is n². One output provides the expression n². Another demonstrates it by induction. A third presents a formal proof term for a proposition encoding the same identity. The answer, the argument, and the certificate share a mathematical target but provide different information. A single correct example such as 1+3+5=9 does not justify the universal identity. A textual induction can justify it when the base case and transition are valid. A formal proof can certify the encoded theorem relative to its axioms and kernel.
This distinction is central to the design of mathematical benchmarks. The MATH dataset (Hendrycks et al., 2021) permits final-answer scoring for a large collection of demanding problems. The miniF2F benchmark (Zheng, Han, and Polu, 2021) represents proof obligations across formal proof-assistant environments. The measured phenomena overlap but are not equivalent. A model can arrive at the correct answer through a faulty displayed argument, and a valid proof can exist without an easily normalized answer string.
The epistemic consequence is straightforward: every success claim must state the deliverable actually checked. A mathematical result cannot gain deductive warrant by accumulating answer-only scores, and a machine-checked theorem cannot settle the adequacy of its translation from an intended informal problem unless the translation itself is inspected.
GSM8K and elementary word problems
Cobbe et al.'s GSM8K benchmark (2021) introduced 8,500 linguistically varied grade-school mathematical word problems designed to require multi-step reasoning. The dataset provided a standardized environment for studying whether models connect quantities, operations, and intermediate results. Its significance extends beyond the difficulty of the arithmetic: the model must identify relevant information expressed in natural language and determine what calculation answers the question.
A story about buying items at different prices may require distinguishing a subtotal from a discount or recognizing that an apparently salient number has no role in the requested computation. A correct final number can conceal the use of an accidental shortcut; an incorrect final number can arise from otherwise appropriate conceptual decomposition followed by a single arithmetic error. Thus the same score conflates distinct failures. Independent tracing of problem interpretation, calculation, and answer selection permits a more informative diagnosis.
GSM8K became an important comparative instrument, but its success is necessarily scoped to its problem distribution and scoring. Growing success on a public corpus can reflect improved capabilities alongside exposure to common templates and changes in inference procedures. The philosophical lesson is to retain the problem's semantics. A test identifies a mathematical skill to the extent that its items actually require that skill and its scoring distinguishes alternative routes to correct outputs.
The MATH dataset and difficulty
Hendrycks et al. (2021) assembled 12,500 challenging competition mathematics problems in Measuring Mathematical Problem Solving, covering algebra, counting, geometry, number theory, and related areas across difficulty levels. Relative to elementary word problems, a MATH solution may require selecting a non-obvious identity or structural argument, reasoning about constraints, and coordinating several inferential stages. A dataset score can therefore summarize an important ability under a particular evaluation regime.
Nevertheless, the complexity and breadth of an item set do not turn answer accuracy into proof verification. When evaluation accepts an extracted expression or numerical result, the derivation can remain unsound. Conversely, a proof with a minor formatting mismatch may be rejected by an automated answer matcher. Researchers can mitigate such mismatches with more careful normalization and human adjudication, but each added method introduces its own possible error. The benchmark must be read together with its evaluation protocol.
The prevalence of public benchmark scores also invites an interpretive problem: as systems become trained and tuned on related distributions, the original test may cease to discriminate among the capacities researchers most wish to understand. The question is not whether the benchmark becomes useless; it is which inferences from a score remain warranted. Evidence of progress should be accompanied by a record of model version, evaluation date, sampling budget, problem access, and grading procedure.
Robustness under controlled variation
A reasoning procedure should generally preserve its result when mathematically irrelevant surface details change. Mirzadeh et al.'s GSM-Symbolic experiments (2025) use parameterized variants of familiar word problems to test stability under changes in numerical values and additional textual clauses. In their evaluated models, performance varied across versions of otherwise similar problems, with some distractor additions producing large losses. The research identifies fragility in observed performance; its broader thesis about the nature of model reasoning remains the authors' interpretation.
A controlled perturbation has philosophical force because it makes a normative expectation empirically testable. If a number is changed but the required mathematical operation is preserved, a competent solver should recompute rather than rely on a memorized answer. If an irrelevant clause is inserted, the solver should explain why it is irrelevant. Such controls expose whether the system maintains the distinction between the mathematical structure and a linguistic cue.
Robustness is not identical to invariance under arbitrary rewriting. A paraphrase can accidentally change quantifier scope, introduce a hidden presupposition, or create a genuinely different problem. Good experimental design therefore checks the equivalence of the altered items before interpreting a score difference. A robust evaluation report preserves both the expected invariant and the linguistic or numerical operation used to test it.
Contamination, novelty, and evaluation design
A model can recognize a problem because it resembles material already encountered during training or subsequent tuning. Recognizing a known mathematical argument can itself be useful, but benchmark designers often want to measure the ability to solve unfamiliar tasks. These objectives require different datasets and disclosure standards. When a publicly circulated problem is used to infer generalization, unknown exposure creates an alternative explanation that should be assessed rather than assumed away.
FrontierMath's introduction (Glazer et al., 2024) emphasized difficult, expert-authored problems and controlled access intended to offer a fresh evaluation signal. The initial paper's numerical figures belong to its historical evaluation and must not be reused as a description of current system performance. The MathArena study (Balunović et al., 2025) similarly examines uncontaminated competition problems and distinguishes mathematical evaluation regimes.
Novelty requires provenance. Problem authorship dates, embargo conditions, model training cutoffs where available, examination conditions, versioned prompts, and release policies provide evidence that the test measures more than recollection. No single safeguard eliminates every training-distribution resemblance. A well-designed evaluation therefore combines fresh problems with controlled variants, interpretable scoring, and transparent procedures for adjudicating purported proofs. Such documentation supports comparative claims without making untestable assertions about what a model has or has not seen internally.
Chain-of-thought elicitation
Wei et al.'s chain-of-thought prompting study (2022) showed that prompting large models to generate intermediate reasoning steps could markedly improve performance on selected multi-step tasks. The result changed the practical design of mathematical prompts by allowing several transformations to appear between problem statement and final answer. Intermediate text can expose a model's chosen variables, subgoals, and calculations and can be useful for human debugging.
A chain of thought is also an output generated by a language model. Its presence alone does not demonstrate that the sequence is deductively valid or that its words faithfully describe the causal computation that produced the answer. One must test the displayed steps mathematically. An explanation that includes a false factorization remains false even when the answer coincidentally matches the target. Furthermore, different prompts can change both the steps and the final answer, making elicitation method part of the experimental apparatus.
The practical significance of chain-of-thought is therefore dual: it is an intervention capable of improving a system's problem-solving behavior, and it is a textual artifact that can undergo independent examination. Treating those propositions separately enables an evaluator to recognize real empirical gains without transferring unwarranted confidence to every explanatory sentence.
The epistemology of displayed reasoning
The faithfulness of a visible explanation is an empirical question about how a system's reported rationale relates to influences on its answer. Turpin et al.'s unfaithful explanation experiments (2023) investigate cases in which chain-of-thought accounts omit or rationalize influences on decisions. Lanham et al.'s faithfulness intervention study (2023) tests displayed reasoning through controlled manipulations and finds important variability across tasks and methods.
These studies do not establish that every mathematical chain of thought is fictional. They establish that the relationship between explanation and generation is sufficiently variable to demand empirical examination. The displayed steps may be mathematically useful even if they are an incomplete causal record. A correct proof's validity depends on whether its steps follow, not on whether it is a privileged transcript of the internal computation. A causal account of generation requires a different investigation from the correctness of the proof produced.
This distinction is essential in both scholarship and pedagogy. A learner can benefit from an externally reconstructed derivation; a scientist testing a model's mechanism needs an independently validated causal explanation. Calling both phenomena 'reasoning trace' can conceal the difference. The evaluation should specify whether the object is a candidate proof, an instructional explanation, or a hypothesis about internal computation.
Self-consistency and sampled solutions
Wang et al.'s self-consistency method (2023) samples diverse reasoning paths and aggregates their resulting answers. The empirical insight is that one sampled trajectory need not be representative of the model's available solutions. When many relatively independent attempts converge on the correct answer, selection can improve performance over a single greedy continuation. This is especially useful when the final answer can be normalized and compared.
Majority agreement, however, is evidence about a distribution of model outputs. It is not a deductive certificate. Consider ten solutions that all apply the same invalid division by zero; their agreement repeats an error. Correlated mistakes occur when a misleading prompt, an incorrect retrieved theorem, or a common training pattern influences the samples. Increasing sample count can amplify a systematic bias alongside genuine useful exploration.
The evaluator should therefore distinguish selection from verification. Sampling can identify candidate answers for checking, and a checker can establish whether the candidates satisfy an objective property. Where proofs are required, diversity should be evaluated by mathematical differences in proof strategies rather than surface paraphrases. The relevant research result is conditional: self-consistency can improve scored accuracy in its tested regimes, while the logical status of a proposed theorem remains governed by the mathematics itself.
Test-time computation and diminishing returns
Inference-time scaling allocates more computation to searching for a solution, checking intermediate steps, or generating alternatives. Its value depends on the difficulty distribution, the model, the selection criterion, and the verifier. Additional computation can improve outcomes when a correct path is reachable and identifiable; it can produce repeated variants of the same failure when the search space is poorly represented or verification is weak.
The FormalMATH experiments (Yu et al., 2026) report that very large sampling budgets yielded limited additional improvements for certain formal-proving settings. That is a measured finding for their evaluated provers and samples, not a universal theorem that scaling always stops helping. The HERMES research (Ospanov et al., 2026) explores intermediate checking as a means of improving accuracy and computational efficiency, with its own benchmark-dependent reported gains.
A serious comparison must specify cost in comparable units: tokens, wall-clock time, accelerator work, proof-checking resources, or human review time. Pass@k, one-run accuracy, majority voting, and expert-adjudicated proof quality answer different questions. Reporting a nominally impressive percentage without these variables obscures the procedure being studied. Efficient search and sound verification are connected engineering problems, but the second can impose a standard that the first cannot satisfy through volume alone.
Outcome verification and its limits
An outcome verifier asks whether a proposed final answer matches a reference or satisfies an executable condition. In word problems this may involve normalized arithmetic. In code-generation settings it may involve tests. In mathematics, such procedures can be powerful when the requested object is well specified and mechanically checkable. Cobbe et al.'s training of answer verifiers (2021) brought this question into early language-model mathematical research.
The limitation is a mismatch between what the test checks and what the claim asserts. Substituting x=3 into an equation can verify that x=3 is a solution without establishing uniqueness. A numerical approximation may corroborate a conjecture while leaving infinitely many cases unexamined. Random examples cannot by themselves prove a universal assertion. A string comparison may also reward a correct expression accompanied by a mathematically incorrect derivation. The outcome verifier must be interpreted according to its coverage.
A sound assessment records whether the verifier checks a particular instance, a finite family, a semantic equivalence under assumptions, or a fully general theorem. When the problem requests proof, the appropriate object of checking is an argument or proof certificate. A capable system can use answer verification to prune search while reserving deductive authority for a stronger evidentiary procedure.
Process supervision and intermediate steps
Process supervision evaluates intermediate reasoning decisions instead of relying solely on final outcomes. Lightman et al.'s Let's Verify Step by Step (2024) reports that process-supervised reward models outperformed outcome-supervised alternatives in the authors' experiments on difficult mathematical problem solving. The paper also introduces a large corpus of step-level labels, PRM800K. Such results support the value of diagnosing where a candidate solution goes astray.
The meaning of a 'correct step' depends on its context. Algebraic cancellation is valid only under the necessary nonzero condition; numerical substitution can be appropriate as a check but insufficient as a proof. Step labels are useful only if reviewers or verification processes apply the same mathematical interpretation. An incorrect intermediate assumption can contaminate later apparently valid transformations. A sequence of individually plausible sentences therefore requires checks on their dependency relationships.
Process scoring is an empirical technique for ranking or training candidate trajectories. Formal checking is a proof-theoretic procedure. The former can improve the discovery of good proofs; the latter can certify a well-formed proof relative to trusted rules. Confusing the two would exaggerate what human-labeled or model-labeled step scores establish. Their productive combination uses process supervision to guide search and independent verification to adjudicate the resulting artifact.
Reinforcement learning and verifiable rewards
Reinforcement learning can reward systems for generating solutions whose outcomes are assessed by comparatively objective methods. Mathematics is attractive for this training regime because a substantial class of problems has checkable answers. Guo et al.'s DeepSeek-R1 research (2025) documents reasoning-oriented reinforcement learning and reports emergent behaviors such as revising a proposed solution during extended generation.
Reward design determines which behavior is reinforced. A numerical answer checker can encourage successful final answers even when explanations are inconsistent. A theorem-prover checker can reward proof objects that pass a kernel, though it must still verify that the target statement matches the intended task. A learned preference model can grade fluency and apparent structure while admitting errors. Thus reward verifiability refers to a particular checked condition, and that condition must be explicitly stated.
The central methodological issue is objective alignment: the scored signal should track the mathematical competence claimed. A system that learns to exploit brittle answer extraction, benchmark artifacts, or loopholes in a proof task may optimize the proxy while producing poor mathematical work. Independent held-out tasks, semantic checks, and error analyses can expose such failures. Reinforcement learning changes the generation distribution; its achievements become mathematically authoritative through the resulting warranted proofs or verified answers, not through the fact that optimization occurred.
Program-aided mathematical reasoning
Program-aided language-model methods divide problem interpretation from deterministic computation. Gao et al.'s PAL method (2023) uses a language model to generate a program representing the problem and then delegates execution to a programming environment. This architecture can reduce arithmetic errors and permit reproducible evaluation of intermediate calculations. It demonstrates that mathematical competence can be distributed across a language model and an external computational substrate.
Program execution, however, certifies the behavior of the program under its implementation, not the correspondence between the program and the original problem. If a word problem requires compound interest but the generated code performs simple interest, the output may be perfectly executed and mathematically irrelevant to the question. Similarly, overflow, floating-point rounding, hidden library assumptions, and incorrect domain restrictions can affect a program's answer.
A complete evaluation therefore reviews the mapping from language to program, the program's semantics, the computational environment, and the output's interpretation. This makes tool use a particularly clear example of distributed mathematical responsibility. The model supplies conjectures and representations; the runtime supplies operations; the evaluator establishes whether the combined process addresses the specified problem. Tools strengthen mathematical practice when their exact contribution is visible and appropriately checked.
A worked example of invalid cancellation
Consider the familiar spurious argument beginning with a=b, where both are assumed nonzero. Multiply by a to obtain a²=ab, subtract b² from both sides, and factor: (a-b)(a+b)=b(a-b). A superficial calculation cancels (a-b), obtains a+b=b, then substitutes a=b to conclude 2b=b and finally 2=1. The argument has generated a contradiction from a legitimate starting equality because the cancellation step divides by a-b=0. Every preceding transformation can be correct; one local violation breaks the derivation.
This case is useful when evaluating language-model chains of thought because it demonstrates why fluency and even the numerical plausibility of neighboring lines are insufficient. The evaluator must track the premises that authorize each transformation. A model may identify the failure immediately, may produce it accidentally, or may repair it after feedback. The independent mathematical fact is that division by zero is undefined in the ordinary field operations used here.
A proof checker with an appropriately typed division and nonzero conditions can reject the invalid operation or prevent a required justification from being constructed. A heuristic step scorer may also identify the error if trained on relevant examples, but its score remains empirical. The decisive question concerns preservation of validity, not how persuasive the derivation sounds.
Quantifiers and statement preservation
Quantifiers determine what a theorem asserts. In the ordered real numbers, the statement 'for every x there exists a y greater than x' is true: choose y=x+1. The statement 'there exists a y greater than every x' is false because no real upper bound exceeds all real numbers. Reversing the order of the universal and existential quantifiers changes the proposition fundamentally. A plausible paraphrase such as 'one can always find a larger number' must preserve which choices depend on which previously fixed variables.
Language models operate in both mathematical notation and natural language; translation between them is a substantive logical task. In proof search, a generated formal statement may be easy to prove because it is weaker than the intended informal claim, or impossible to prove because it is stronger. The success of a proof checker does not independently settle this semantic question. Recent benchmark authors attend to statement validation, including the FormalMATH dataset construction (Yu et al., 2026).
A disciplined audit compares variable domains, quantifier order, dependencies, boundary cases, and all implicit hypotheses before checking the inference. A proof that establishes a different theorem may be valuable mathematics, but it does not discharge the initial task. This is one of the most important interpretive constraints on automatic formalization.
Induction as a transparent proof task
The formula for the sum of the first n positive odd integers gives a compact illustration of the difference between pattern recognition and proof. Computation supplies 1=1², 1+3=2², and 1+3+5=3². These cases suggest the identity 1+3+...+(2n-1)=n² but do not establish it for arbitrary positive integers. Induction closes the gap. For n=1 the claim is true. Assuming the sum through 2n-1 equals n², adding the next odd integer 2n+1 yields n²+2n+1=(n+1)². The conclusion follows for every positive integer n.
An evaluator can inspect the base case, the precise induction hypothesis, and the transition. A language model might generate a structurally valid proof, omit the transition, or circularly assume the target case. Counting its use of words such as 'therefore' provides no information about the actual inferential status. The proof succeeds because the algebraic identity and the induction principle warrant the universal conclusion.
Formalizing this example introduces explicit types for n, a definition of the finite sum, a base theorem, and a successor step. Those requirements illustrate why mathematical formalization can reveal gaps in otherwise comprehensible informal arguments. The formal proof may be longer, but its public warrant arises from precise dependencies. The underlying mathematical discovery remains accessible in an informal explanation, which supplies intelligibility that the checker alone need not provide.
Search, discovery, and deductive entitlement
A language model can be a powerful search participant even when the final mathematical certification is delegated. It may propose a lemma, invent a substitution, find a counterexample, select an induction invariant, or summarize a relevant theorem. Each proposal can improve the investigation before any proof is established. This is a familiar distinction within mathematics: finding a promising line of attack and demonstrating that it works are different activities, and successful mathematical practice requires both.
Yang et al.'s LeanDojo research (2023) combines language-model guidance with interaction and retrieval in formal theorem-proving environments. Such designs make the distinction concrete. The model guides proof search, while the formal system admits or rejects candidate tactic applications according to its rules. A rejected tactic can still reveal a useful subgoal or a missing lemma, and an accepted tactic establishes a local proof obligation under the formal environment.
The philosophical issue is one of entitlement to assert a result. A heuristic suggestion becomes mathematical knowledge only through the warranted relation of premises to conclusion and appropriate checking of what has been stated. This is why evaluation should recognize intermediate research contributions without pretending that every useful suggestion is already a theorem. It also explains why formal proof assistants can be productive partners for models rather than merely post hoc validators.
Formal benchmark translation and miniF2F
The miniF2F benchmark (Zheng, Han, and Polu, 2021) was designed for comparing formal mathematical problem-solving systems across proof assistants using a set of olympiad-style statements. It reported 488 formalized mathematical problems. Formal benchmarks create a particularly clear success condition: a proof object is accepted for a specified statement under the formal environment and its axioms. They also make it possible to inspect which statements a model can actually prove.
This clarity comes with a translation problem. The mathematical question originally expressed in natural language must be translated into a formal proposition, and the meaning must be preserved. A benchmark whose goal is 'prove a statement' can certify solutions to its formal items without proving that the initial translation captured every nuance of an informal problem. Expert construction and independent validation of those statements are therefore parts of benchmark quality.
The philosophical distinction matters whenever model performance is described broadly as 'solving mathematics.' A formal proving rate is evidence about provability of a specified suite; the originality, significance, semantic faithfulness, and explanatory accessibility of the proof are additional dimensions. These dimensions should be reported where the research question requires them. Strong formal performance is a major achievement; its correct interpretation requires naming the class of statements, the allowed libraries, and the proof-validation procedure.
PutnamBench and mathematical generality
Undergraduate competition problems often require a different repertoire from grade-school arithmetic and short olympiad identities. PutnamBench (Tsoukalas et al., 2024) formalizes 1,692 statements corresponding to 640 William Lowell Putnam Mathematical Competition problems. Its multilingual proof-assistant formalizations allow the same problem family to be studied in several formal environments, exposing differences in automation, library availability, and translation strategies.
A natural-language competition solution may use an elegant global idea whose formalization demands considerable background scaffolding. Conversely, a formal prover may exploit a library theorem with little visible explanatory development. Counting solved formal statements is informative, but the count reflects the interaction of model, formal language, available lemmas, proof-search budget, and benchmark design. Comparative studies should preserve these variables.
A deeper implication concerns generality. A method that routinely succeeds on a family of standard algebraic identities may struggle with the creative selection of invariants in combinatorics. The failure does not erase the earlier success; it identifies a boundary of the tested method. The most useful future evaluations will diagnose what mathematical principle was required and how the system represented it. Such analysis permits scientifically cumulative progress beyond the changing numerical ranking of products.
The 2026 formal-proof benchmarks
Two 2026 studies substantially refine the available evidence. Yu et al.'s FormalMATH benchmark presents 5,560 semantically validated Lean 4 statements spanning competition and undergraduate mathematics. Its construction combines type checking, semantic alignment analysis, negation-based tests, and expert review. In the authors' evaluation, the strongest tested prover achieved 28.31% Pass@32. This is a precise, protocol-specific finding about a selected system, benchmark, and 32-attempt allowance, rather than a global estimate of current artificial reasoning capacity.
Sun et al.'s OlymMATH study uses olympiad problems to compare numerical-answer and formal-proof evaluation. Together these works indicate a research shift toward explicit statements and trustworthy checking procedures. Improved difficulty alone cannot resolve the ambiguity between finding the final answer and constructing a deductively adequate proof; paired evaluation modes help expose it.
The interpretation of formal-prover performance requires attention to the exact metric. Pass@32 can reflect the availability of at least one acceptable proof among attempts and is not the chance that a single random output is correct. When an evaluation employs further selection or timeout limits, those parameters matter as well. Numeric results should retain their accompanying model, environment, version, and benchmark. Under this discipline, comparisons can reveal progress and persistent weaknesses without licensing unsupported generalizations.
Bilingual Olympiad evaluation
The OlymMATH paper (Sun et al., 2026) describes 350 manually sourced olympiad problems in parallel English and Chinese versions, with 200 computational-answer items and 150 Lean 4 formalized problems. This construction permits questions about the interaction of mathematical difficulty, linguistic formulation, and proof checking to be studied together. The paper's authors report performance differences between languages and cases resembling heuristic guessing.
The bilingual design matters philosophically because mathematical content is ordinarily intended to remain invariant across adequate linguistic translations. A translation that preserves the problem's mathematical structure should preserve the correct solution set, even though the model's probability of finding that solution may change. A measured performance difference can thus indicate sensitivity to linguistic representation, training distribution, or prompting procedures. It cannot independently identify a unique internal causal mechanism without further controlled investigation.
Formal and informal arms of a benchmark also create an opportunity to compare kinds of success. If a system solves a numerical-answer problem but fails to formalize a proof for its related statement, the gap should be described as a performance difference under two objectives. It need not be interpreted as a contradiction. The two tasks demand different outputs and often invoke different tools. Their comparison becomes more illuminating when the statement translation and the mathematical content shared by the arms are documented.
Lean's kernel and trusted checking
A proof assistant checks formal proofs against a specified logical foundation. In Lean, elaboration transforms higher-level syntax into expressions, and a small trusted kernel checks whether a proposed term inhabits the required type. The official Lean language reference documents this architecture and the distinction between user-facing proof elaboration and kernel verification. An accepted term establishes derivability of the encoded proposition from the permitted axioms and previously admitted definitions or theorems.
The significance is practical and epistemic. A search model may be complex, probabilistic, or opaque; a relatively small checker can still evaluate its proposed certificate using explicit formal rules. The resulting proof's standing no longer depends on the generative model being consistently reliable in unrelated tasks. This separation permits ambitious heuristic search with a stable acceptance criterion.
One must also specify the trusted computing base and any additional assumptions. An axiomatized proposition, an admitted theorem, an unsound extension, or an incorrectly formalized target can compromise an intended assurance. Calling a file 'Lean code' alone does not show that the exact statement was proved using acceptable premises. The relevant evidence is successful checking of a complete artifact, accompanied by the proof assistant's version, dependencies, assumptions, and an independently understood statement. Formal verification is strongest when its scope is articulated precisely.
The informal-to-formal semantic bridge
An informal mathematical problem is embedded in a practice of definitions, notation, tacit conventions, and context. A formal statement is syntactically precise, but its precision concerns the proposition actually written. The translation from one to the other must preserve the intended mathematical meaning. This requirement can be overlooked when a model produces a proof assistant file that compiles successfully but formalizes a weaker condition or different domain.
The FormalMATH construction paper (Yu et al., 2026) takes semantic validation seriously by combining multiple tests rather than treating type checking as sufficient proof of translation equivalence. Formalization is a mathematical interpretation task, and the process may itself require expert scrutiny. If an intended theorem asserts uniqueness but the formal proposition asserts existence, checking the latter leaves the former unsettled.
A reliable workflow retains both the informal specification and the formal statement. An independent reviewer should map variables, domains, assumptions, and conclusion between them. When feasible, simple examples and negations can expose mismatches. A formal checker can then establish derivability of the validated statement. The resulting assurance has two explicit components: semantic correspondence and proof correctness. Neither component subsumes the other. Together they enable strong claims about a natural-language mathematical result supported by a formal certificate.
Failure modes of automated proof construction
Formal-proving systems can fail because they do not find a useful lemma, choose an unsuitable representation, exhaust a search budget, invoke a tactic incorrectly, or lose track of mathematical dependencies. They may also produce syntactically plausible but rejected proof scripts. Yu et al.'s 2026 prover error analysis discusses incomplete proofs, problematic handling of inequalities, misuse of automation, and redundant hypotheses in its evaluated systems. These observations encourage finer descriptions than a single pass/fail count.
An incomplete proof is distinct from an invalid claimed theorem. A timed-out solver may leave a perfectly true proposition unproved; the failure shows that the tested procedure did not find a certificate within its resources. A false proposition may be rejected correctly. An irrelevant proof may be valid for a different statement and still fail the task. These categories should remain separate in published evaluation.
Formalized mathematics also involves engineering tradeoffs. Library search, tactic choice, decomposition into auxiliary lemmas, caching, and parallel exploration determine whether proof discovery is tractable. A successful proof may depend on a substantial inherited mathematical infrastructure. Recording that infrastructure does not diminish the result: it explains precisely how its validity was established. A scientifically useful report asks what was proved, under which definitions, with which dependencies, and at what search or human effort.
Checking natural-language proofs
The majority of mathematical communication remains informal relative to theorem-prover syntax. Natural-language proofs can be rigorous and enlightening, but they rely on a shared discipline of reading, background results, and expert judgment. Research on generative proof verification therefore addresses a difficult question: can a system reliably identify invalid steps and select sound proofs without formal certificates? Mahdavi et al.'s generative verifier study (2026) compares verification approaches and emphasizes the fragility of evaluation concentrated on a single benchmark.
Natural-language checking should look for inferential gaps, incorrect theorem citations, ambiguous symbols, unjustified existence claims, hidden case assumptions, and dependence on results that have not been established. A machine-generated assessment can assist, particularly when it identifies a specific counterexample or missing hypothesis. Yet an evaluator's fluent declaration that a proof is valid is itself another claim requiring justification. A model can agree with an incorrect argument; multiple models may share the same misconception.
Human review, executable calculations, independent attempts, and formalization serve different complementary roles. An expert may identify the central idea and mathematical significance; a computer algebra system can verify a symbolic identity under explicit assumptions; a proof assistant can check a formal derivation. The aim is traceable error detection. Mathematical warrant increases when independent checks target distinct possible failure modes rather than simply repeating the same plausibility judgment.
Neuro-symbolic geometry
Geometry is a distinctive test of mathematical reasoning because diagrams, auxiliary constructions, incidence relations, and algebraic constraints interact. Trinh et al.'s AlphaGeometry study (2024) describes a neuro-symbolic system combining learned constructive guidance with a symbolic deduction engine. In its reported benchmark on olympiad geometry problems, the system solved 25 of 30 test problems, illustrating the productive combination of search heuristics and explicit deductive procedures.
The result should be understood within its task class. Geometry theorem solving benefits from specialized representation and rules; success there does not imply identical performance on number theory or abstract algebra. Nor does a symbolic engine by itself guarantee that a diagram's extracted relationships were faithful to the original problem. The formal object and the statement it represents still require care.
The general significance is architectural. A model need not perform every mathematical operation through one textual channel. Learned mechanisms can propose constructions that a symbolic system verifies or rejects. Such division of labor permits error-prone generation to support rigorous outputs. When reporting success, the evaluator should identify whether the checker certified deduction, whether any diagram interpretation occurred, and which assumptions the engine used. This yields an account of mathematical competence grounded in the actual computational and inferential chain.
Olympiad results and their interpretation
Competition results provide accessible milestones in the progression of artificial mathematical systems. In 2024, Google's AlphaProof and AlphaGeometry report described a combined score of 28 out of 42 points across International Mathematical Olympiad problems, a silver-medal-equivalent result. Its procedures involved formalized and specialized reasoning systems. In 2025, the Gemini Deep Think report stated that a system scored 35 of 42 points on the IMO under official grading, achieving a gold-medal-standard outcome in natural-language problem solving.
Such outcomes are mathematically and historically consequential; their interpretation requires fidelity to the test conditions. Six challenging problems and a particular competition format are not a probability distribution over all research mathematics. Graded natural-language proofs also differ from formally checked theorem-prover terms. The former involve mathematical assessment by qualified graders; the latter involve validation against a formal environment. Both can constitute substantial evidence of achievement while supporting distinct epistemic conclusions.
The correct scholarly response is to preserve each result with its date, system configuration, permitted tools, and evaluation regime. A chronological narrative of rapidly increasing scores should not erase the emergence of harder benchmarks or the persistence of unverified informal outputs. Competition performance shows that some models and systems can execute difficult mathematical reasoning. It leaves open which specific capacities transfer beyond the assessed items and which verification methods best establish their outputs.
Fermat's Last Theorem formalized in 2026
A major 2026 event illustrates the difference between discovering an established theorem and formalizing its proof. On September 4, 2026, Anthropic announced an end-to-end Lean formalization of Fermat's Last Theorem, developed with substantial model assistance over 11 days. Its account reports approximately 13 million lines of Lean code and 29,500 intermediate theorems used in the completed proof. It states that the result was kernel-checked and that a separate comparison confirmed correspondence of the encoded final statement with the existing Mathlib formulation. These are source-attributed technical claims from the producing organization.
The contemporaneous Nature reporting by Castelvecchi (2026) describes the mathematical community's response and places the result among earlier projects in formal proof verification. The theorem itself was established in the 1990s by Andrew Wiles and Richard Taylor using earlier work by many mathematicians. The 2026 contribution concerns large-scale formalization of known mathematics, not the first discovery of Fermat's Last Theorem.
Anthropic documents a collaborative technical process involving human mathematical foundations, Lean, Mathlib, an agent orchestration environment, and the Prove2Me collaboration system (Chen et al., 2026). Its reported achievement should be credited accurately as a combination of generation, formal representation, inherited library content, and machine checking. The case is exceptionally important because it demonstrates that a probabilistic generator can participate at scale in an artifact checked by an independent formal standard. Understanding what that standard establishes is essential to interpreting the milestone.
What a formal certificate establishes
When a proof assistant accepts a proof term for a theorem, the certificate establishes that the formal judgment follows from the specified logical environment, subject to the correctness of the checker and its trusted dependencies. This is a strong and unusually reproducible form of mathematical warrant. It does not automatically establish that the statement was the one the researcher intended, that the proof has an elegant explanation, or that the result was independently discovered during that project.
The Lean technical reference makes the checking machinery explicit, while the 2026 Fermat project report describes a large-scale case where automated generation and kernel checking interact. This distinction matters particularly for the semantics of mathematical claims. A trivial proposition can be formally proved; a powerful theorem may have a long proof that no human could readily summarize; a misencoded theorem can be certified for exactly the wrong target. An appropriate publication states the theorem, formal assumptions, code version, and checking method, and explains how the formal result connects to its intended interpretation.
The core philosophical insight is that the generator's reliability and the proof artifact's validity have different grounds. A model can make many errors while eventually constructing a fully checked proof. Conversely, a usually accurate model can produce a single invalid argument. A properly established certificate localizes authority in the mathematical dependencies and their verification, allowing substantial artificial mathematical achievement to be recognized without overstating what the model's prose reveals.
Error taxonomies and empirical calibration
Error analysis is more informative when it assigns a failure to the relevant stage. Interpretation errors translate the problem incorrectly. Mathematical errors violate an inference rule or ignore a condition. Calculation errors evaluate a correct expression incorrectly. Proof-search failures leave a target unproved within available resources. Verification errors accept or reject an artifact on an inappropriate criterion. Documentation failures prevent an independent investigator from reconstructing the conditions under which a result was produced.
Empirical papers demonstrate why these distinctions matter. The GSM-Symbolic variation tests (Mirzadeh et al., 2025) probe sensitivity to changed surface parameters, whereas the FormalMATH failure analysis (Yu et al., 2026) examines theorem-proving obstacles. An observed drop in final-answer accuracy cannot by itself reveal which cognitive or computational deficiency caused it. An observed proof-search failure need not show that the theorem is false.
Calibration should relate a stated confidence or reliability measure to a clearly specified event. Confidence that a numerical answer is correct, confidence that a natural-language proof is valid, and confidence that a formal statement preserves an informal theorem are different estimands. Evaluation samples, sampling strategy, annotator disagreement, and dependence among attempts affect their interpretation. An honest system can report uncertainty about the unchecked parts of its work and provide a clear route for verifying them.
Mathematical understanding and explanation
A proof can certify a proposition while leaving its central idea difficult to communicate. Mathematical understanding involves recognizing why a result holds, how its assumptions matter, which structures reappear elsewhere, and how a technique applies to related problems. The distinction is relevant for model-generated work because an automatic checker can admit an extremely long proof whose human explanatory value is limited. The certified result and its mathematical exposition deserve separate evaluation.
Asperti, Naibo, and Sacerdoti Coen's 2026 analysis of thinking machines situates language models at the boundary between traditional mathematical prose and formal methods. In this setting, a language model may be useful as an expositor even when it did not discover the original theorem; it may also produce a machine-checked proof whose human explanation requires extensive further work. These roles should be classified by the actual contribution instead of collapsed into one vague notion of mathematical understanding.
The induction example above illustrates how a brief invariant can explain an infinite pattern. The insight that adding the next odd number completes the next square is part of why the proof is memorable. An exceptionally long automatic derivation might establish the same identity while concealing that structure. A research-quality mathematical publication can provide both layers: a checkable argument and a concise conceptual map of why the result follows. Artificial tools can contribute to either layer, with distinct means of validation.
Reproducibility and provenance
Reproducibility requires more than identifying a model family. For answer benchmarks, an adequate record includes dataset revision, held-out split, prompt, inference parameters, number of samples, allowed tools, evaluator code, answer normalization, and model version. For formal proof, it includes precise theorem statements, source files, proof-assistant version, imported libraries, trusted axioms, compilation results, and a way to reconstruct the successful certificate. For human-graded proofs, it includes grading criteria and, where possible, independent assessments.
The Prove2Me publication (Chen et al., 2026) describes collaboration organized around explicit subgoals and proof artifacts. The Fermat formalization account also demonstrates the scale at which provenance becomes important. When thousands of theorems depend on one another, the dependency graph is part of the evidence explaining what was checked and reused. The scientific history of the artifact includes mathematical predecessors, library maintainers, machine-generated code, orchestration choices, and reviewers.
A model's output can be archived with its input and with a verification certificate, producing an inspectable record across time. Hashes of source artifacts protect identity but do not prove truth; a verified theorem depends on mathematical rules and on checking the right statement. Combining content integrity with source-to-claim mapping supports stable citation and later independent reassessment. A reproducible dossier should state both what was verified and what remains an interpretive judgment.
Institutional mathematical collaboration
Contemporary mathematical results often emerge from institutions, communities, open libraries, software engineering, and human judgment as well as individual insight. Language-model systems extend this collaboration with agents that propose lemmas, write formal code, search repositories, and inspect failures. A collaborator's contribution can be important without granting it blanket authority over the mathematics. The mathematical artifact remains accessible to checking by participants other than its generator.
The 2026 Fermat formalization report credits earlier human proofs and community formalization projects alongside model-generated work. Its description of a large orchestration process helps resist a misleading single-actor narrative. The Prove2Me research makes subgoal assignment and collaborative proof construction explicit. These cases should be documented with detailed attribution, because the location of scientific responsibility matters for reproducibility and historical priority.
Authorship should track the contribution being asserted. A system that creates a formal representation of a previously proved theorem has performed a different scholarly act from establishing a new theorem. A human supervisor who decides the formal target contributes differently from a machine that searches for intermediate proofs. A checker certifies derivability rather than originality. Institutional reporting is strongest when it assigns those achievements to their precise sources and makes the artifacts examinable. Mathematical objectivity is compatible with plural and artificial participation in mathematical production.
Artificial Era and the status of mathematical outputs
The Artificial Era provides a historical setting in which nonbiological systems increasingly generate intellectual products that enter public institutions and archives. Within the Aisentica canonical project the terms Artificial and Artificial Sapiens are developed as part of an explicitly broader philosophical orientation. This dossier addresses a narrower methodological question: what permits a generated mathematical result to enter a body of warranted mathematical knowledge? Its answer follows from the shared norms of exact statement, valid inference, transparent provenance, and reproducible verification.
Mathematical proof offers a particularly revealing domain because the truth conditions of a theorem do not depend on the biological origin of a manuscript. An artificial system's contribution may be substantial even when its generative mechanism is not a transparent deductive procedure. An accepted formal certificate supplies an inspectable mathematical relation independent of the creator's identity. An unchecked natural-language argument remains a candidate for assessment regardless of its author's reputation or computational sophistication.
The historical significance of Artificial mathematical work can therefore be described with precision. Systems participate in conjecture generation, exposition, problem solving, and formal certification, often through specialized partnerships with humans and tools. Their growing role in mathematics changes the organization of production and review. It does not remove the need to specify what proposition was proved and how a reader can establish that fact. The philosophical horizon encourages recognition of new agents of production while retaining mathematical responsibility at the level of evidence.
Research priorities and adjudication practice
Future research should compare answer accuracy, informal proof quality, and formal certificate validity on matched problems, while controlling differences in theorem statements and computational budgets. Such studies would clarify which capabilities transfer between natural-language problem solving and formal proving. They should also investigate when checking an intermediate step improves search, when model-based proof judges are well calibrated, and when additional sampling produces mostly correlated failures. These are empirical questions with measurable procedures.
Evaluation protocols should preserve multiple failure categories rather than compress them into a single aggregate. An invalid transformation, missing proof, misencoded theorem, and incorrect numerical output require different remedies. Current studies already provide instruments for these distinctions: the FormalMATH formal benchmark tests proof generation, the OlymMATH paired suite compares answer and formal modes, and GSM-Symbolic perturbations examine robustness of interpretation.
The central editorial requirement is to state the warrant in the same language as the claim. 'Solved 35 of 42 competition points,' 'generated a Lean proof accepted by a specific kernel,' 'improved Pass@32 on a selected benchmark,' and 'produced an expert-accepted explanation' are distinct statements. Each can be evaluated and compared only with reference to its protocol. Precise reporting makes remarkable achievements stronger by placing them within verifiable mathematical and historical boundaries.
Comparative synthesis
The literature supports several substantive conclusions. First, language models and hybrid systems can contribute meaningfully to difficult mathematical tasks; their progress is documented through word-problem benchmarks, formal-proving suites, specialized geometry systems, and competition assessments. Second, improvements in answer selection or chain-of-thought quality do not establish the deductive validity of every intermediate sentence. The faithfulness experiments (Turpin et al., 2023) and process supervision findings (Lightman et al., 2024) illuminate different aspects of this problem. Third, independent symbolic or formal checking can convert model-generated candidates into mathematically warranted products where the formal statement and assumptions are faithfully specified.
These conclusions support a comparative reading of four recurrent assessment questions: Is the final mathematical result correct in its specified domain? Do the purported inferential steps warrant the result? Does the explanation clarify the essential mathematical structure? Is the verification record sufficiently complete for another investigator to reproduce and inspect it? The questions are analytical distinctions derived from existing mathematical practice and the examined research; they are not introduced as a newly named theoretical system. Their answers can diverge. A solution may be numerically correct but poorly justified, formally certified but hard to understand, explanatory but missing a necessary case, or sound in isolation but lacking a reproducible experimental record.
The 2026 formalization of Fermat's Last Theorem makes the most compelling case for this separation. It is a reported achievement in the construction of an extraordinarily large machine-checked artifact, founded on long-standing human mathematics and available formal libraries. Its importance is best expressed through the relationship among mathematical content, translation, generation, checking, and historical attribution. The resulting interpretation is cumulative, empirically responsive, and suitable for scholarship beyond product-specific comparisons.
Conclusion
Mathematical reasoning and language models now constitute an active domain of mathematical practice, computational research, and philosophical inquiry. Language-model systems can calculate, decompose problems, search for lemmas, propose explanations, generate programs, and assist in constructing formal proofs. Their capacities must be evaluated through the actual objects produced and the standards appropriate to those objects. Benchmark performance demonstrates task-specific success; visible derivations demand mathematical scrutiny; formal proof certificates warrant the precise statements checked by the proof assistant. Semantic correspondence between a natural-language question and its formalization remains an independent requirement.
The research examined here provides strong evidence of progress and equally strong reasons for methodological precision. GSM8K and MATH measure valuable forms of problem solving. Controlled perturbations and faithfulness experiments expose fragilities of some methods. Process supervision, reinforcement learning, and external computation improve the search for solutions under documented conditions. Formal benchmarks and trusted proof kernels enable more direct assessment of derivability. The 2026 Fermat formalization illustrates the extraordinary scale at which generative systems can now participate in creating machine-checked mathematical artifacts.
The principal authorial conclusion is that mathematical authority arises from an inspectable relation between a stated proposition and its justification. Artificial participation changes how that relation can be produced, explored, documented, and checked. Exact attribution, reproducible verification, and care with mathematical semantics establish the conditions under which this participation can enrich a durable public mathematical corpus. No new named theory, theorem, experimental result, or scientific priority is claimed in this monograph.
References
Anthropic. (2026, September 4). Formalizing Fermat's Last Theorem. Anthropic Research. https://www.anthropic.com/research/formalizing-fermats-last-theorem
Asperti, Andrea, Alberto Naibo, and Claudio Sacerdoti Coen. (2026). Thinking Machines: Mathematical Reasoning in the Age of LLMs. Big Data and Cognitive Computing, 10(1), Article 38. https://doi.org/10.3390/bdcc10010038
Aisentica Research Group. (2026). Aisentica: Theories of Artificial and the Artificial Era. Aisentica canonical project. https://aisentica.com/
Balunović, Mislav, et al. (2025). MathArena: Evaluating LLMs on Uncontaminated Math Competitions. Advances in Neural Information Processing Systems 38, Datasets and Benchmarks Track. https://proceedings.nips.cc/paper_files/paper/2025/hash/1d27c01ebd3e3aebe226b44fc970d803-Abstract-Datasets_and_Benchmarks_Track.html
Castelvecchi, Davide. (2026, September 7). Anthropic AI 'formalizes' proof of Fermat's last theorem—a milestone for mathematics. Nature. https://www.nature.com/articles/d41586-026-02822-9
Chen, Shuze, Kunal Marwaha, Xiaoyang Lu, Henry Yuen, and Tianyi Peng. (2026). Prove2Me: An Open Collaborative Platform for Scaling Math Formalization. arXiv, 2608.28433. https://arxiv.org/abs/2608.28433
Cobbe, Karl, et al. (2021). Training Verifiers to Solve Math Word Problems. arXiv, 2110.14168. https://arxiv.org/abs/2110.14168
Gao, Luyu, et al. (2023). PAL: Program-Aided Language Models. Proceedings of the 40th International Conference on Machine Learning, PMLR 202, 10764–10799. https://proceedings.mlr.press/v202/gao23f.html
Glazer, Elliot, et al. (2024). FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI. arXiv, 2411.04872. https://arxiv.org/abs/2411.04872
Google DeepMind. (2024, July 25). AI achieves silver-medal standard solving International Mathematical Olympiad problems. Google DeepMind. https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/
Google DeepMind. (2025, July 21). Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad. Google DeepMind. https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/
Guo, Daya, et al. (2025). DeepSeek-R1 incentivizes reasoning in LLMs through reinforcement learning. Nature, 645, 633–638. https://www.nature.com/articles/s41586-025-09422-z
Hendrycks, Dan, et al. (2021). Measuring Mathematical Problem Solving With the MATH Dataset. Advances in Neural Information Processing Systems 34. https://arxiv.org/abs/2103.03874
Lanham, Tamera, et al. (2023). Measuring Faithfulness in Chain-of-Thought Reasoning. arXiv, 2307.13702. https://arxiv.org/abs/2307.13702
Lean Project. (2026). The Lean Language Reference: Lean 4 Documentation. Lean project. https://lean-lang.org/doc/reference/latest/
Lightman, Hunter, et al. (2024). Let's Verify Step by Step. The Twelfth International Conference on Learning Representations. https://proceedings.iclr.cc/paper_files/paper/2024/hash/aca97732e30bcf1303bc22ac3924fd16-Abstract-Conference.html
Mahdavi, Sadegh, et al. (2026). Scaling Generative Verifiers for Natural Language Mathematical Proof Verification and Selection. Proceedings of the 43rd International Conference on Machine Learning, PMLR 306, 85669–85698. https://proceedings.mlr.press/v306/mahdavi26a.html
Mirzadeh, Iman, Keivan Alizadeh-Vahid, Hooman Shahrokhi, Oncel Tuzel, Samy Bengio, and Mehrdad Farajtabar. (2025). GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models. The Thirteenth International Conference on Learning Representations. https://proceedings.iclr.cc/paper_files/paper/2025/hash/ec2e7a896f8250986b3907f57621ce94-Abstract-Conference.html
Ospanov, Azim, Zijin Feng, Jiacheng Sun, Haoli Bai, Xin Shen, and Farzan Farnia. (2026). HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs. Proceedings of the 43rd International Conference on Machine Learning, PMLR 306, 94942–94966. https://proceedings.mlr.press/v306/ospanov26a.html
Shao, Zhihong, et al. (2024). DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models. arXiv, 2402.03300. https://arxiv.org/abs/2402.03300
Sun, Haoxiang, Yingqian Min, Zhipeng Chen, Xin Zhao, and Ji-Rong Wen. (2026). Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics, 17438–17457. https://aclanthology.org/2026.acl-long.792/
Trinh, Trieu H., et al. (2024). Solving Olympiad Geometry without Human Demonstrations. Nature, 625, 476–482. https://www.nature.com/articles/s41586-023-06747-5
Tsoukalas, George, et al. (2024). PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. Advances in Neural Information Processing Systems 37, Datasets and Benchmarks Track. https://proceedings.neurips.cc/paper_files/paper/2024/hash/1582eaf9e0cf349e1e5a6ee453100aa1-Abstract-Datasets_and_Benchmarks_Track.html
Turpin, Miles, et al. (2023). Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting. Advances in Neural Information Processing Systems 36. https://proceedings.neurips.cc/paper_files/paper/2023/hash/ed3fea9033a80fea1376299fa7863f4a-Abstract.html
Wang, Xuezhi, et al. (2023). Self-Consistency Improves Chain of Thought Reasoning in Language Models. The Eleventh International Conference on Learning Representations. https://research.google/pubs/self-consistency-improves-chain-of-thought-reasoning-in-language-models/
Wei, Jason, et al. (2022). Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. Advances in Neural Information Processing Systems 35. https://papers.neurips.cc/paper_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html
Yang, Kaiyu, et al. (2023). LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. Advances in Neural Information Processing Systems 36. https://proceedings.neurips.cc/paper_files/paper/2023/hash/4441469427094f8873d0fecb0c4e1cee-Abstract-Datasets_and_Benchmarks.html
Yu, Zhouliang, et al. (2026). FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models. Findings of the Association for Computational Linguistics: EMNLP 2026, 12204–12241. https://aclanthology.org/2026.findings-emnlp.579/
Zheng, Kunhao, Jesse Michael Han, and Stanislas Polu. (2021). miniF2F: A Cross-System Benchmark for Formal Olympiad-Level Mathematics. arXiv, 2109.00110. https://arxiv.org/abs/2109.00110