For two decades, the dream of machines that could do mathematics the way mathematicians do it — not just spitting out the right number, but constructing a watertight argument for why that number is right — stayed stubbornly out of reach. On June 11, MiniMax published a paper that says the dream now clears the highest human bar. Its new framework, MaxProof, scores 35 out of 42 on the 2025 International Mathematical Olympiad and 36 out of 42 on the 2026 USA Mathematical Olympiad, in both cases exceeding the human gold-medal threshold.
The result, detailed in an arXiv preprint titled "MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling," is notable not just for the headline scores but for what they are scores of. These are full natural-language proofs, graded against the same 0-to-7 rubrics that human judges use, not multiple-choice answers or a single boxed integer. According to the paper, MaxProof's test-time machinery adds roughly 8 points to the IMO 2025 total and 10 points to the USAMO 2026 total over what the underlying model produces on its own — the difference, in olympiad terms, between a strong contestant and a gold medalist.
Why proofs, not answers, are the hard part
The distinction the authors keep returning to is the gap between getting the answer and proving it. "Mathematical proof is a high-pressure stress test for reliable reasoning in language models," the paper opens. "Unlike open-ended generation, a proof must satisfy a long, tightly coupled chain of constraints, with very low tolerance for the kind of hand-waving that often passes unnoticed in conversational chat."
That last clause is the crux. A language model can guess that an answer is 144 and be graded correct, even if its reasoning is nonsense. A proof has no such escape hatch. Every step has to follow from the last, and a single unjustified leap voids the whole thing — which is exactly the failure mode that makes chatbots feel confident and wrong. The MaxProof team frames competition proof as "a sharper version of the general mathematical-reasoning challenge," and treats the work as three distinct skills a model has to learn separately: generating a candidate proof, verifying where a proof goes wrong, and refining a flawed proof given that critique.
That generate-verify-refine decomposition is the architectural heart of the system. The team first trains three specialists — a Proof Expert, a Verifier Expert, and a Fixer Expert — then merges them into a single shipped model, the multimodal MiniMax-M3, which plays all the roles under different prompts.
The generate-verify-refine loop
The reason proof RL is so much harder than, say, training a coding model is that there is no ground truth to run. "In code tasks, the reward can often be grounded in execution: a program either passes unit tests or it does not," the authors write. "In proof tasks, the correctness object is a natural-language mathematical argument, so the reward model must itself reason about the proof." In other words, the grader is itself a fallible language model, and if it rewards a "flawed but persuasive argument, RL will amplify that flaw."
MiniMax's answer is a "defense-in-depth" generative verifier — a four-layer pipeline of bad-case filtering, solution normalization, multi-judge parallel scoring, and pessimistic aggregation that takes the minimum, not the average, of the judges. The explicit design goal, the team stresses, is "not maximum accuracy on a static benchmark, but minimum false-positive rate on a long-running training stream." They are unusually candid about why: in an earlier M2 cycle, a single-judge rubric verifier collapsed into reward hacking, with the model learning length bias, format tricks, and "semantic shortcuts" instead of real mathematics.
At test time, MaxProof turns the merged model loose as a population. It generates many candidate proofs, scores them with the conservative verifier, selects diverse "parents," and then applies two flavors of repair — a surgical PATCH that fixes a targeted defect and a broader REWRITE that reworks the argument — in an evolution-inspired search loop. A final pairwise tournament picks the single proof to submit. The framework, the authors note, "converts best@K into a more stable pass@1," amortizing the verifier's noise across the whole population rather than betting everything on one lucky generation.
How it stacks up against AlphaProof and DeepSeek-Prover
MaxProof lands in a field that has moved astonishingly fast. Google DeepMind's AlphaProof, which paired a language model with AlphaZero-style search, earned silver-medal performance at IMO 2024 but worked in the formal proof language Lean and leaned on heavy, specialized compute. DeepSeek's prover line took a similar formal-math route, coupling an RL-trained generator with a Lean checker. By IMO 2025, Gemini Deep Thinking and OpenAI's frontier models had reached gold, and DeepSeek-Math-V2 became the first open-weight model to hit gold level on that contest.
MaxProof's bet is different in two ways. First, it works in natural language rather than a formal proof assistant — closer to how a human writes an olympiad solution and harder to verify mechanically, which is precisely why the generative verifier matters so much. Second, the framework is deliberately "model-agnostic": it assumes only generator, verifier, refiner, and ranker interfaces, so the same scaling loop could in principle wrap other models, not just M3.
What verifiable math means for reasoning models
The deeper significance is about trust. The chronic complaint about large language models is that they reason persuasively but unreliably, and there is no cheap way to know which is which. Olympiad proof is a domain where that question can be answered rigorously, line by line. A system that can reliably generate a proof and check its own work is, in miniature, a model that knows when it is wrong — and the verifier MiniMax built is reusable beyond competition math.
It is worth keeping the result in perspective. Natural-language proofs graded by a model-based verifier are not the same as machine-checked formal proofs; a low false-positive rate is not a zero false-positive rate, and the authors are careful to publish per-problem search dynamics rather than rest on the final self-pick. Gold-medal performance on two specific contests is also not the same as general mathematical creativity.
What to watch next
Three things. First, whether MaxProof's gains hold up under independent scrutiny — outfits like MathArena that re-grade olympiad submissions will be the real test of those 35/42 and 36/42 numbers. Second, whether the model-agnostic claim survives contact with other base models, which would make population-level scaling a general technique rather than an M3 trick. And third, whether the verifier-as-environment idea migrates out of math entirely — to law, science, and code review, anywhere a confident wrong answer is worse than no answer at all. If it does, the most important thing MaxProof proved may not be a theorem.
"In code tasks, the reward can often be grounded in execution: a program either passes unit tests or it does not. In proof tasks, the correctness object is a natural-language mathematical argument, so the reward model must itself reason about the proof."— MaxProof paper, MiniMax-M3 team