AlphaProof

AlphaProof is a reinforcement-learning system from Google DeepMind that finds and verifies formal mathematical proofs in the Lean 4 theorem prover, and in July 2024 it was one component of the first AI system to reach silver-medal standard at the International Mathematical Olympiad (IMO).^[1][2] That standard was reached by a combined system, not by AlphaProof on its own: announced on July 25, 2024, AlphaProof paired with AlphaGeometry 2 solved four of the six 2024 IMO problems for a combined score of 28 out of 42 points, one point below the gold-medal threshold.^[1][5] Because every step runs inside Lean, a proof that the verifier accepts is correct by construction, with no hidden errors.^[1] The system was published in Nature in November 2025, and by 2026 it had been folded into a larger agentic framework, AlphaProof Nexus, aimed at open research problems rather than competition mathematics.^[2][11]

Unlike earlier AI math tools that generated plausible-sounding but unverified reasoning, AlphaProof operates entirely within a formal language where every step is machine-checked. This means its proofs cannot contain hidden errors; if the Lean verifier accepts a proof, it is correct by construction.^[1] The methodology was published in Nature on November 12, 2025, under the title "Olympiad-level formal mathematical reasoning with reinforcement learning," by Thomas Hubert, Rishi Mehta, Laurent Sartran and colleagues (Nature 651, 607-613).^[2][18]

What problem does formal theorem proving solve?

Mathematics has two distinct cultures. The informal culture, practiced by most working mathematicians, produces proofs written in natural language, with intuitive reasoning and occasional hand-waving over details that are considered obvious. The formal culture, supported by tools like Lean, Coq, and Isabelle, requires every inference to be spelled out in a logical language that a computer can verify from first principles.^[7]

Formal proofs carry a guarantee that informal proofs do not: they are correct or they do not compile. This property makes formal methods attractive for safety-critical software, hardware verification, and cryptographic protocols.^[7] For AI, the formal setting offers something equally valuable: an exact, binary reward signal. A proof step is either valid or invalid, with no need for a human judge.^[1]

The obstacle has always been data. Informal mathematical writing is abundant, but human-authored formal proofs are scarce. Lean's main community library, Mathlib, has passed two million lines of formalized mathematics, which is remarkable for a volunteer project but small compared to the training corpora available in natural language domains.^[9] Systems trained only on existing Lean proofs quickly hit a ceiling.

Before AlphaProof, neural provers in the automated theorem proving tradition could handle university-level lemmas but struggled with competition mathematics, which requires stringing together novel sequences of nontrivial steps without a clear roadmap. The 2024 IMO problems, in particular, sit near the frontier of what high school students can do with months of preparation, making them a meaningful benchmark for AI reasoning.^[4]

How does AlphaProof work?

AlphaProof combines three components: a language model trained on formal mathematics, a reinforcement learning loop modeled on AlphaZero, and an autoformalization pipeline that converts natural-language problem statements into Lean.^[1][2]

Language model backbone

At its core, AlphaProof uses what the Nature paper calls a 3-billion-parameter encoder-decoder transformer, referred to as the proof network.^[2] The encoder takes the pretty-printed Lean tactic state and feeds a latent representation to two heads: the decoder, which acts as the policy and generates candidate tactics, and a value head that estimates how many steps remain.^[2] Pretraining ran on approximately 300 billion tokens of publicly available code and mathematical texts, using a next-token prediction objective with dropout and masked span reconstruction for regularization.^[2] The pretraining corpus is code and mathematics rather than general web text.

After pretraining, the model undergoes supervised fine-tuning on approximately 300,000 state-tactic pairs extracted from human-authored proofs in the Mathlib library, amounting to roughly five million tokens of tactics.^[2] This phase teaches the model the local tactics available in Lean and what kinds of moves tend to make progress on which kinds of goals.

AlphaZero-style reinforcement learning

AlphaProof adapts the AlphaZero reinforcement learning algorithm, which DeepMind originally developed for board games. In the game setting, AlphaZero uses a neural network to evaluate positions and a Monte Carlo tree search (MCTS) to explore future moves; self-play generates training data without any human supervision. AlphaProof reframes proof search as a similar game: the state is the current proof goal, the moves are tactic applications, and a win occurs when the proof compiles.^[1]

The system interacts with a custom Lean 4 environment that executes tactics, handles proof states, and supports the operations needed for large-scale tree search.^[2] At each node in the search tree, AlphaProof's neural network evaluates candidate tactics and estimates the likelihood of eventual success. The MCTS guides exploration toward promising branches, with the network's predictions improving as more proofs are discovered.

A notable feature of the search is how it handles what the paper calls AND nodes, which arise when a tactic splits a proof goal into several independent subgoals. During backpropagation through an AND node, the value passed up is the minimum over the child subgoals, that is, the value of the hardest branch, since the overall proof succeeds only when every subgoal is resolved.^[2] Selection at an AND node considers only unproven subgoals, and the selection formula is modified to prioritize the subgoal that looks hardest, so the search concentrates effort on what remains unsolved.^[2]

Every verified proof is fed back into training, updating the model's weights to make similar reasoning steps easier to find on future problems.^[1] This expert iteration loop generates progressively harder training examples, since the system can now prove harder problems and add those to its curriculum.

Autoformalization with Gemini

The training pipeline requires a large supply of formal problems, but human-written Lean problems are limited. AlphaProof solves this through autoformalization: a fine-tuned Gemini 1.5 Pro model translates natural-language mathematics into Lean 4 statements. DeepMind put roughly one million natural-language statements through this pipeline, producing a curriculum of approximately 80 million Lean problems.^[1][2]

The autoformalization model is trained on triplets of (informal statement, formalization reasoning chain, formal Lean statement). For each source problem, the model generates multiple distinct Lean formalizations stochastically, producing roughly 80 times more formal variants than the original problem count.^[2] The point of generating many variants is to raise the chance that at least one is a correct formalization; the paper notes that incorrect ones were often quickly resolved during the main RL phase, or sometimes turned out to be interesting problems in their own right.^[2]

This pipeline was applied to a large corpus of mathematical problems spanning many topics and difficulty levels, building a library of formal problems used for the RL training phase. The system trained by proving or disproving millions of such problems over a period of weeks before the 2024 IMO competition.^[1]

During the actual competition, Gemini was also used on the problems that require identifying an answer before proving it, such as "find all functions" questions. The public Gemini 1.5 Pro model generated 500 candidate answers per problem, optimized for a high chance of including the right one rather than for precision, and AlphaProof then sifted them in a low-compute refutation mode with a ten-minute tree search per candidate. It disproved 99% of the incorrect candidates for P1, 98% for P2 and 7% for P6, isolating the survivors for full proof attempts.^[2]

Test-time reinforcement learning

One of the more unusual aspects of AlphaProof is that training continues during inference on difficult problems. When given a hard problem, the system does not simply run a fixed forward pass. Instead, it generates variations of the target theorem, creates a curriculum of easier sub-problems and related conjectures, and runs additional RL iterations specifically focused on that problem.^[2][18] This allows the model to effectively specialize for the problem at hand, discovering intermediate lemmas that are useful even if they were never seen in pretraining.

For IMO 2024, this test-time RL was applied over extended compute sessions. Each of AlphaProof's three solutions, P1, P2 and P6, required two to three days of test-time RL.^[2] DeepMind's statement that one problem was solved within minutes refers to the geometry problem, which AlphaGeometry 2 rather than AlphaProof handled, in 19 seconds.^[1]

What are Lean 4 and Mathlib?

Lean 4 is the version of the Lean theorem prover that AlphaProof operates in. Lean was originally developed at Microsoft Research and is now maintained by an open-source community.^[7] It is both an interactive theorem prover and a functional programming language based on dependent type theory, specifically the calculus of inductive constructions.^[7]

Lean's type system enforces logical consistency at the language level: a term inhabiting a type corresponds to a proof of the proposition that type encodes, a correspondence known as the Curry-Howard isomorphism. This means that if Lean accepts a program as well-typed, the corresponding mathematical statement has been proven.^[7]

Mathlib is Lean's comprehensive community-maintained mathematical library, covering algebra, analysis, topology, number theory, combinatorics, probability, and many other areas.^[9] It represents years of collective effort by hundreds of contributors and has become one of the most extensive formal mathematics libraries in any proof assistant.

For AlphaProof, Mathlib serves as both a curriculum and a toolbox. The model was fine-tuned on proofs extracted from Mathlib and can leverage all of Mathlib's existing definitions, lemmas, and tactics during search.^[2] When a proof step calls a Mathlib lemma, that call does not need to be re-derived from scratch; the prover simply applies the existing theorem.

Wenda Li, a lecturer in hybrid AI at the University of Edinburgh who peer-reviewed the research but was not involved in it, described automating the translation of mathematics into a formal language as a significant step for the field: "We can have much greater confidence in the correctness of published results if they are able to formulate this proving system, and it can also become more collaborative."^[4] The formal setting means that any proof the system produces is unambiguously correct, which is not true of AI-generated informal proofs that can sound plausible while containing subtle errors.^[2]

How did AlphaProof perform at IMO 2024?

The 65th International Mathematical Olympiad took place in Bath, England, from July 11 to July 22, 2024. A total of 609 contestants from 108 countries competed.^[5] Each contestant faced six problems worth seven points each, for a maximum of 42 points. Medal cutoffs that year were: gold at 29 points or above (58 contestants), silver from 22 to 28 points (123 contestants), and bronze from 16 to 21 points (145 contestants).^[5][6]

The combined AlphaProof and AlphaGeometry 2 system solved four of the six problems, earning 28 points total, placing it within the silver-medal range and one point below the gold-medal threshold.^[1]

Problem breakdown

Human solve rates below are the official per-problem statistics published in the Mathematics Magazine report on the competition, counting contestants who scored the full seven points.^[5]

Scroll sideways for more →

AlphaProof solved P1, P2, and P6. AlphaGeometry 2, a separate system specialized for Euclidean geometry, solved P4, and did so within 19 seconds of receiving its formalization.^[1] Problems P3 and P5, both in combinatorics, remained unsolved.^[1]

P6 was the most remarkable result. It was the hardest problem at the 2024 competition, solved by only five human contestants out of 609, with a mean score of 0.40 out of 7.^[1][5] AlphaProof found a valid Lean proof for P6, though the approach it used was characterized by extensive case analysis rather than a compact elegant argument. The solution worked by checking many cases systematically, which is a valid mathematical strategy but not the kind of clean argument a human mathematician would typically aim for.^[8]

P2, a number theory problem about sequences of greatest common divisors, was handled by AlphaProof using analysis of behavior modulo ab+1. While the underlying mathematical insight was sound, Greg Burnham, who read the released proofs closely, judged that the Lean code was "also quite ugly by human standards," noting that correctness was the system's only objective.^[8]

P1, an algebra problem that 68% of contestants solved, was the competition's most approachable problem for humans, but that did not make it fast for AlphaProof: like P2 and P6 it required two to three days of test-time RL.^[2][5]

Timing

AlphaProof did not work under the same time constraints as human contestants, who sit two sessions of 4.5 hours each, one per day, with three problems in each session. The system spent two to three days on each problem it solved, using substantial compute. This is a significant caveat when comparing its performance to human results.^[1][2]

External validation

The solutions were evaluated by Professor Sir Timothy Gowers, a Fields Medal winner and IMO gold medalist, and Dr. Joseph Myers, a two-time IMO gold medalist who chaired the IMO 2024 Problem Selection Committee. They judged the formal proofs according to the official IMO point-awarding rules and awarded full marks for each solved problem.^[1][2] Professor Gowers, speaking of a construction the system produced, said: "The fact that the program can come up with a non-obvious construction like this is very impressive, and well beyond what I thought was state of the art."^[1]

How does AlphaProof compare with human IMO performance?

The table below places the AlphaProof-AlphaGeometry 2 combined score in context relative to the 2024 IMO medal cutoffs.

Scroll sideways for more →

Because 28 is the top of the silver band, the result placed the combined AI system in roughly the top 12% of contestants: 75 of the 609 competitors scored 28 points or more.^[6] However, the comparison requires care. Human contestants face three problems per day across two sessions of 4.5 hours each. AlphaProof ran for two to three days on individual problems, used substantial computational resources, and required human experts to translate the problems from natural language into Lean before the system could process them.^[1] Under identical time and resource constraints, the human-comparable score would likely be lower.

The two unsolved problems, P3 and P5, were combinatorics problems that required constructing novel organizational structures and reasoning about strategies. These types of problems seem to be a persistent weakness of the formal-reasoning approach, as they require inventing intermediate abstractions that are not naturally suggested by the problem statement.^[8]

How does AlphaProof differ from the IMO 2025 gold result?

The peer-reviewed account of AlphaProof appeared in Nature on November 12, 2025, more than a year after the IMO result it describes, and gave the first detailed public account of the architecture, training pipeline, and results.^[2] A companion News and Views piece in the same journal assessed how the system looked to working mathematicians.^[15]

At IMO 2025, Google DeepMind fielded a different approach: an advanced version of Gemini with Deep Think capability. This system operated entirely in natural language, without requiring expert translation into Lean, and solved five of the six IMO 2025 problems within the standard 4.5-hour competition time limit, achieving a score of 35 out of 42 points, exactly the gold-medal threshold.^[3] The IMO 2025 result was certified by official IMO coordinators using the same criteria applied to student solutions, the first time AI submissions were officially graded by the IMO, and IMO President Gregor Dolinar said the solutions were "astonishing in many respects," adding that "IMO graders found them to be clear, precise and most of them easy to follow."^[3] OpenAI separately announced a 35 out of 42 result on the same problem set from an experimental reasoning model, graded internally by former IMO medalists rather than by the competition itself.^[17] Both are covered in more detail at AI gold medals at the 2025 IMO.

The contrast between 2024 and 2025 illustrates two different philosophies. AlphaProof's approach relies on formal verification: proofs are machine-checked and guaranteed correct, but the system requires formalization infrastructure and extended compute. The 2025 Gemini approach trades formal guarantees for speed and generality, producing rigorous-sounding natural language proofs within a competition-compatible time frame.^[3]

Scroll sideways for more →

AlphaProof Nexus and the turn to research mathematics

In 2026 AlphaProof stopped being a standalone competition system and became a component inside a larger agentic framework. A team of 21 authors, almost all at Google DeepMind, with George Tsoukalas as first author, Pushmeet Kohli and Swarat Chaudhuri as the corresponding authors, and Gergely Berczi of Aarhus University as the one external collaborator listed, posted "Advancing Mathematics Research with AI-Driven Formal Proof Search" to arXiv on May 21, 2026, and revised it on June 8, 2026.^[11] The abstract does not use a product name; the body of the paper introduces AlphaProof Nexus as "a new framework for agents that query frontier LLMs and the Lean compiler."^[11] There was no accompanying DeepMind blog post. The release consisted of the preprint plus a GitHub repository of the resulting Lean proofs and prose translations.^[11][12]

The architecture inverts the 2024 design. Where AlphaProof was a purpose-built prover with a large language model used mainly for autoformalization, Nexus puts the LLM in charge: Gemini 3.1 Pro subagents write candidate Lean proofs in an agentic loop against the compiler, with cheaper Gemini 3.0 Flash subagents acting as raters. AlphaProof itself survives as an optional tool the prover subagents can call to discharge a specific subgoal, running in a low-compute tree-search mode rather than its full test-time RL mode, at roughly 27.5 TPU hours (about $60) per problem on v6e hardware.^[11]

Scroll sideways for more →

DeepMind reports the inference cost as a few hundred dollars per solved problem.^[11] Two of the nine Erdos results answered questions the paper traces to 1970, open for 56 years.^[11]

Those counts deserve careful reading, and the paper itself supplies most of the caveats. Terence Tao maintains a public wiki cataloguing AI contributions to Erdos problems, and the DeepMind authors logged their results there under the tool name "DeepMind prover agent."^[11][13] That wiki grades each contribution on two axes: completeness (full resolution, partial progress, incorrect, or unverified) and independence (AI standalone, AI alongside literature, AI building on literature, or AI with human collaboration).^[13] The entries are mixed rather than uniformly clean solutions. As reviewed on July 27, 2026, problems 125, 138 and 741 sit under "AI standalone," but 138 is logged only as a partial result; problems 152 and 846 sit under "AI alongside literature," and 846 was solved independently by an OpenAI internal model at the same time; problems 12 and 26 sit under "AI building on literature," with 12 citing the 1970 Erdos and Sarkozy paper and logged as a partial result, and 26 recorded as a solution to a stronger problem than the one listed.^[13] Four further entries on that wiki are filed under the name "AlphaProof" rather than "DeepMind prover agent" (problems 198, 477, 835 and 949, dated between 2025 and January 2026); those predate this paper and are not among the nine.^[13] The paper is candid on the same point, noting that some of the resolved problems had already received attention in multiple prior works.^[11]

Two further findings temper the headline. The paper reports that the basic configuration, using only an LLM and Lean compiler feedback with no AlphaProof involvement at all, solved all nine Erdos problems, though at higher cost on the harder ones.^[11] And the raw hit rate is low: 9 of 353 is under 3%, concentrated in combinatorics and number theory where Mathlib's coverage is deepest, with most of the catalogue still out of reach.^[11][16] The authors also describe characteristic failure modes, including agents that offloaded a problem's core difficulty into a single unproven sorry or invoked hallucinated lemmas, which is precisely what end-to-end Lean checking is there to catch.^[11]

Detail on the agent configurations, the individual problems, and the OEIS pipeline is covered at AlphaProof Nexus.

What is AlphaProof used for?

AlphaProof's IMO performance is a demonstration of a capability with broader applications in mathematics and software.

Availability to mathematicians

AlphaProof has never been released as a public product. Access has come through curated research partnerships. On October 29, 2025, Google DeepMind and Google.org announced the AI for Math Initiative, giving five institutions, Imperial College London, the Institute for Advanced Study, the Institut des Hautes Etudes Scientifiques, the Simons Institute for the Theory of Computing at UC Berkeley, and the Tata Institute of Fundamental Research, funding plus access to DeepMind systems including Gemini Deep Think, AlphaEvolve, and what the announcement calls "our formal proof completion system, AlphaProof."^[14] The AlphaProof Nexus work extended the same pattern, embedding the system in collaborations across combinatorics, optimization, graph theory, algebraic geometry, and quantum optics.^[11]

Mathematical research assistance

Formal theorem proving systems can serve as verification backends for mathematical research. A mathematician can state a conjecture in Lean and use AlphaProof-like systems to search for proofs of supporting lemmas, check that a proposed proof strategy does not have gaps, or verify that a known result from one area of mathematics applies in another context. The formal output provides a machine-checkable certificate of correctness. This is the sense in which formal proof search has become part of the wider AI for science agenda.

Google DeepMind subsequently published a set of formalized conjectures in the formal-conjectures GitHub repository, explicitly inviting the formal mathematics community to use these as benchmarks and training targets.^[10] That repository later supplied the 353 open Erdos statements used in the AlphaProof Nexus evaluation.^[11]

Software and hardware verification

Formal methods have long been used in safety-critical software and hardware design.^[7] The same mechanisms that AlphaProof uses to verify mathematical proofs apply directly to verifying that a program or circuit satisfies a formal specification. AI-assisted formal verification could reduce the cost of verifying complex systems that are currently too large to check manually.

Automated theorem proving pipelines

In multi-stage discovery pipelines, AlphaProof functions as a verification backend. A discovery system identifies a conjecture or candidate result; an informal reasoning system sketches a proof strategy; AlphaProof formalizes and verifies the argument within Lean. Each successful proof extends the formal library available to future reasoning, creating a compounding effect as the library grows. The Nexus agents are a direct instance of this pattern, with the LLM supplying strategy and Lean supplying the guarantee.^[11]

Education and proof checking

Formal proof assistants have been proposed as educational tools that give students immediate feedback on proof attempts. An AlphaProof-like system could help students understand where a proof attempt breaks down and what additional lemmas are needed, without requiring a human instructor to check each step.

What are AlphaProof's limitations?

AlphaProof has several significant limitations that affect its practical usefulness compared to informal mathematical reasoning.

Formalization requirement. As of its 2024 announcement, AlphaProof required human experts to translate competition problems from natural language into Lean before the system could process them.^[1] This is not a quick task; the IMO 2024 combinatorics problem P5 (Turbo the Snail) defeated the team's experts on the first day of formalization, because the statement quantifies over a winning strategy, an object that is natural to reason about informally but awkward to define in Lean.^[2][8] The autoformalization pipeline addresses this partially but does not yet handle all problem types without human oversight.

Compute requirements. AlphaProof used far more computational resources and time than human contestants. Problems that took human contestants hours required the system days of continuous search on substantial hardware.^[1] The silver-medal score was achieved under conditions that are not comparable to competition constraints.

Weakness on combinatorics. The two unsolved IMO 2024 problems were both combinatorics problems.^[1] Combinatorics often requires inventing the right abstraction or proof structure, which is not suggested by the problem statement. AlphaProof's search-based approach works well when useful intermediate lemmas can be discovered incrementally but struggles when the key insight requires a conceptual leap to a new organizational framework.^[8]

Proof style. AlphaProof's proofs, while correct, are not always written in a style that mathematicians find illuminating. The P6 solution used extensive case enumeration rather than a general argument.^[8] Such proofs verify the truth of a statement but do not necessarily convey why it is true, which limits their value for mathematical understanding.

Library coverage. Novel mathematical territory that falls outside Mathlib's existing coverage requires extending the library before AlphaProof can reason about it effectively. Adding new mathematical areas to Mathlib is a significant undertaking that still requires substantial human effort. The AlphaProof Nexus results cluster in the areas where Mathlib is strongest, which is consistent with this constraint.^[11][16]

No informal reasoning. AlphaProof does not produce informal mathematical intuition. It finds formal proofs but cannot explain its reasoning in the way a mathematician would explain why a proof idea works. This makes it difficult to use as a collaborative tool in the way that informal AI assistants can be. The Nexus framework works around this by publishing natural-language prose translations alongside the Lean proofs rather than by making the prover itself explain anything.^[12]

Low absolute success rate on research problems. On the first large-scale test against genuinely open questions, the success rate was under 3% of the Erdos problems attempted and under 10% of the OEIS conjectures.^[11] Formal proof search has moved from competition problems to research problems, but it resolves a small minority of what it is pointed at.

See also

• AlphaProof Nexus
• AlphaGeometry
• AlphaGeometry 2
• Lean (theorem prover)
• Mathlib
• Automated theorem proving
• AI gold medals at the 2025 IMO
• Google DeepMind
• Gemini
• AlphaEvolve
• AlphaZero
• Reasoning
• Reinforcement learning
• Mathematical reasoning
• Terence Tao

References

1. ^"AI achieves silver-medal standard solving International Mathematical Olympiad problems." Google DeepMind, 2024-07-25. deepmind.google/...-problems-at-silver-medal-level
2. ^Hubert, T., Mehta, R., Sartran, L. et al. "Olympiad-level formal mathematical reasoning with reinforcement learning." Nature 651, 607-613, 2025-11-12. nature.com/...s41586-025-09833-y
3. ^"Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad." Google DeepMind, 2025-07-21. deepmind.google/...rnational-mathematical-olympiad
4. ^"Google DeepMind's new AI systems can now solve complex math problems." MIT Technology Review, 2024-07-25. technologyreview.com/...olve-complex-math-problems
5. ^Bajnok, B., Berman, J., Trevino, E. "Report on the 65th Annual International Mathematical Olympiad." Mathematics Magazine 98(2), 130-138, 2025-04. campus.lakeforest.edu/...2024IMO.pdf
6. ^"65th IMO 2024, individual results." International Mathematical Olympiad, 2024. imo-official.org/...2024
7. ^"Lean programming language." Lean FRO. lean-lang.org
8. ^Burnham, G. "AlphaProof and the IMO." Lemmata, 2025-04-28. lemmata.substack.com/...alphaproof-and-the-imo
9. ^"Mathlib: A Foundation for Formal Mathematics Research and Verification." Lean FRO. lean-lang.org/...mathlib
10. ^"formal-conjectures." Google DeepMind, GitHub. github.com/...formal-conjectures
11. ^Tsoukalas, G., Kovsharov, A., Shirobokov, S. et al. "Advancing Mathematics Research with AI-Driven Formal Proof Search." arXiv:2605.22763, v1 2026-05-21, v2 2026-06-08. arxiv.org/...2605.22763
12. ^"alphaproof-nexus-results." Google DeepMind, GitHub, 2026-05. github.com/...alphaproof-nexus-results
13. ^Tao, T. et al. "AI contributions to Erdos problems." teorth/erdosproblems wiki, GitHub. github.com/...contributions-to-Erd%C5%91s-problems
14. ^"Google DeepMind and Google.org announce AI for Math Initiative." Google, 2025-10-29. blog.google/...ai-for-math
15. ^Ringer, T. "Mathematicians put AI model AlphaProof to the test." Nature 651, 595-597, 2025. nature.com/...d41586-025-03585-5
16. ^"Google Deepmind's AlphaProof Nexus solves decades-old math problems for a few hundred dollars." The Decoder, 2026-05-25. the-decoder.com/...blems-for-a-few-hundred-dollars
17. ^"OpenAI Model Earns Gold-Medal Score at International Math Olympiad and Advances Path to Artificial General Intelligence." Scientific American, 2025-08-21. scientificamerican.com/...tional-math-olympiad-and
18. ^"Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning." Google Research publications. research.google/...ing-with-reinforcement-learning