Fields Model Day

I survey the space of large-scale reasoning competition, and how the AI Math Olympiad series of competitions fits into this space. Results, stories and take-away points from the past 4 competitions (AIMO 1-3 and AIMO Proof Pilot) are highlighted, as well as from a collaboration between OpenAI and the AIMO. The talk concludes with general points about how competitions can act as an engine and focussing lens for open-source research.

Recent progress in mathematical reasoning is often attributed to larger models and more compute. My work for the AI Mathematical Olympiad (AIMO) suggests two other bottlenecks: the quality of verifiable training signals and the ability to turn reasoning models into deployable proof systems. I will present two complementary projects. CrystalMath studies difficulty saturation in reinforcement learning with verifiable rewards: as models improve, easy valid problems stop providing useful learning signals, while mislabeled problems remain concentrated in the apparently hard tail. We introduce Contrast-Augmented Verification (CAV), which asks a verifier to compare a label-supporting solution against independently generated solutions that reach conflicting answers. On a manually adjudicated diagnostic set, CAV reduces false acceptance of incorrect solutions from 55% to 15%. We use it to curate 2,129 competition-level problems from over 800,000 candidates across 12 public sources. In tool-integrated RLVR experiments, CrystalMath improves average pass@1 by 8.3 points over a size-matched DAPO subset and by 5.9 points over a difficulty-matched pre-CAV pool. Proof Pilot moves from exact-match answers to long-form natural-language proofs, where verification becomes part of the inference system itself. Under a restricted open-model whitelist and a single-GPU offline deployment budget, we built an OLMo-based 32B system combining tokenizer transplantation, attention sinks, supervised and on-policy distillation, quantization, and a single-model prove-verify-refine-select loop. The final system scored 29/42 in the AIMO Proof Pilot. I will conclude with practical lessons on verifier design, data-model co-evolution, and why system constraints can matter as much as model scale.

In this talk, I will introduce my AIMO3 solution and the ideas behind it. The main improvement was prompt design based on analyzing LLM-generated answers and identifying common error patterns. I will also introduce two topics that interested me during the competition: AI for business mathematics and AI for mathematics in Kaggle.

Recent LLMs are approaching and surpassing world-class mathematical ability. Identifying the correct answer given problems and traces that the average human cannot solve becomes a central challenge in achieving artificial superintelligence. Solving a problem with LLMs involves two steps: generating candidate solutions and verifying them. Through our AIMO 3 effort, we found that the relative difficulty of these steps is task-dependent and that competition mathematics is "easy to guess, hard to verify," in contrast to tasks like integer factorization or multi-hop QA benchmarks, where a single trace can be checked easily. This talk introduces existing approaches and discusses challenges for future AI-for-Math research. It also examines competition dynamics — why optimizing the mean score loses to optimizing the upper confidence bound — and the practical challenges of training math models, concluding with our publicly released model and SFT dataset.

We develop a statistical theory of LLM-guided theorem proving with proof assistants such as Lean and Rocq. We formulate interactive theorem proving as a finite-horizon deterministic Markov Decision Process, and a tactic-proposing LLM as a stochastic policy with trainable parameters. Statistical provability is defined as the average probability of reaching a proof goal over a distribution of problems. Although theorem proving is hard in the worst case, modern AI-assisted provers often succeed in practice. We explain this gap by studying biased problem distributions. We formalize two types of bias and show that, when the distribution is sufficiently skewed, learning can make statistical provability positive: the model can prove new theorems similar to those it has seen. For hierarchical problems, hierarchical LLMs can improve learning efficiency, giving a principled justification for subgoal decomposition in agentic theorem provers.