PaperlayerView exact revision on arXiv

Source-linked AI summary

Towards Autonomous Mathematics Research

Tony Feng, Trieu H. Trinh, Garrett Bingham, Dawsen Hwang, Yuri Chervonyi, Junehyuk Jung, Joonkyung Lee, Carlo Pagano, Sang-hyun Kim, Federico Pasqualotto, Sergei Gukov, Jonathan N. Lee, Junsu Kim, Kaiying Hou, Golnaz Ghiasi, Yi Tay, YaGuang Li, Chenkai Kuang, Yuan Liu, Hanzhao Lin, Evan Zheran Liu, Nigamaa Nayakanti, Xiaomeng Yang, Heng-Tze Cheng, Demis Hassabis, Koray Kavukcuoglu, Quoc V. Le, Thang Luong

arXiv:2602.10177v3cs.LGcs.AIcs.CLcs.CY

TL;DR

Research mathematics requires synthesizing extensive literature, raising the question of whether AI can autonomously discover and prove theorems. Aletheia iteratively generates, verifies, and revises natural-language solutions, with reported milestones including an AI-generated paper and four semi-autonomously verified Erdős solutions.

  • Problem

    The paper asks whether AI can autonomously discover and prove new mathematical theorems, a challenge that requires synthesizing techniques from extensive research literature.

    Source: §1 · p. 1

  • Method

    Aletheia uses interacting Generator, Verifier, and Reviser subagents to iteratively generate, verify, and revise end-to-end natural-language solutions until approval or a preset attempt limit.

    Source: §2 · p. 3

  • Results

    Reported outcomes include an AI-generated eigenweights paper, a human-AI collaborative paper, four semi-autonomously verified Erdős solutions among 700 problems, and leading performance on FirstProof.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The paper proposes an autonomy-level taxonomy to support transparent public communication about AI-generated mathematics.

    Source: §1 · p. 2

    Success cases were rare in the broader research-level effort, with no autonomous progress on most problems.

    Source: §5.2 · p. 14

Abstract

from arXiv · show

Recent advances in foundational models have yielded reasoning systems capable of achieving a gold-medal standard at the International Mathematical Olympiad. The transition from competition-level problem-solving to professional research, however, requires navigating vast literature and constructing long-horizon proofs. In this work, we introduce Aletheia, a math research agent that iteratively generates, verifies, and revises solutions end-to-end in natural language. Specifically, Aletheia is powered by an advanced version of Gemini Deep Think for challenging reasoning problems, a novel inference-time scaling law that extends beyond Olympiad-level problems, and intensive tool use to navigate the complexities of mathematical research. We demonstrate the capability of Aletheia from Olympiad problems to PhD-level exercises and most notably, through several distinct milestones in AI-assisted mathematics research: (a) a research paper (Feng26) generated by AI without any human intervention in calculating certain structure constants in arithmetic geometry called eigenweights; (b) a research paper (LeeSeo26) demonstrating human-AI collaboration in proving bounds on systems of interacting particles called independent sets; and (c) an extensive semi-autonomous evaluation (Feng et al., 2026a) of 700 open problems on Bloom's Erdos Conjectures database, including autonomous solutions to four open questions. In order to help the public better understand the developments pertaining to AI and mathematics, we suggest quantifying standard levels of autonomy and novelty of AI-assisted results, as well as propose a novel concept of human-AI interaction cards for transparency. We conclude with reflections on human-AI collaboration in mathematics and share all prompts as well as model outputs at https://github.com/google-deepmind/superhuman/tree/main/aletheia.

1. Introduction

Aletheia addresses the gap between Olympiad-level AI performance and research mathematics, where progress requires navigating extensive literature and constructing proofs. The paper presents its research capabilities and proposes ways to communicate AI-assisted mathematical results transparently.

Introduction

  • Aletheia combines advanced Gemini Deep Think, inference-time scaling from Olympiad problems to PhD-level exercises, and intensive search and browsing in an iterative generate-verify-revise workflow.The agent produces, verifies, and revises end-to-end solutions in natural language.Source: §1 · p. 1
  • Feng26 reports an AI-generated paper without human intervention calculating eigenweights, while LeeSeo26 demonstrates human-AI collaboration proving bounds for independent sets.The works concern structure constants in arithmetic geometry and systems of interacting particles, respectively.Source: §1 · p. 2
  • Aletheia was deployed semi-autonomously on 700 open problems in Bloom’s Erdős database and resolved four questions, including Erdős-1051, with AI grading and human-expert verification.A generalization arising from Erdős-1051 led to BKKKZ26.Source: §1 · p. 2
  • Aletheia also contributed intermediate propositions that improved human authors’ prior proofs in FYZ26 and ACGKMP26.These contributions appeared in two further research papers.Source: §1 · p. 2
  • Feng et al., 2026a reports Aletheia’s leading performance on FirstProof, a collection of ten research-level problems proposed by academic mathematicians as an assessment of AI capabilities.The proposal is attributed to Abouzaid et al., 2026.Source: §1 · p. 2
  • The authors propose an autonomy-level taxonomy with separate axes for mathematical significance and degree of AI contribution, while emphasizing that their autonomous results are not claimed as major mathematical advances.They note that most solved Erdős problems, though listed as open for decades, proved quite elementary.Source: §1 · pp. 2–3
  • The taxonomy is intended to address an evaluation gap: few experts can assess most results’ novelty and significance, enabling misinformation about AI-generated mathematics.The authors suggest the taxonomy as a framework for transparent public communication.Source: §1 · p. 2

2. The Aletheia agent: From Olympiads to Research-level Mathematics

Aletheia extends Gemini Deep Think toward research-level mathematics with a natural-language Generator–Verifier–Reviser loop and tool use. Evaluation shows gains over Deep Think on Olympiad and PhD-level benchmarks, while limitations in accuracy and citation reliability motivate its design.

2. The Aletheia agent: From Olympiads to Research-level Mathematics

  • Aletheia uses Generator, Verifier, and Reviser subagents that iterate until the Verifier approves a solution or attempts reach a preset limit, operating end-to-end in natural language.Each subagent also orchestrates calls to a Gemini base model.Source: §2 · p. 3

2.2. Developing Agentic Harnesses for Research-Level Math

  • Aletheia scored 93% overall on IMO-ProofBench Advanced without tools, outperforming same-base Deep Think at every tested compute scale, and also outperformed it on FutureMath Basic.It returned solutions for 29 of 30 IMO-ProofBench problems, with 96% conditional accuracy; on FutureMath Basic it answered fewer than 60% of problems but exceeded 82% conditional accuracy. With a February 2026 Gemini 3 base model, it scored 95% on IMO-ProofBench Advanced. Aletheia also often admits when it cannot solve a problem, which the authors say improved human-AI research collaboration.Source: Figure 2 · p. 4, §2.2 · p. 5, §2.3 · p. 5

2.1. Scaling Laws and the Evolution of Deep Think

  • Deep Think’s inference-time scaling improved Olympiad performance and transferred to PhD-level tasks, but lower PhD accuracy and hallucinations showed that scaling alone was insufficient for research mathematics.The Jan 2026 advanced model reduced the compute needed for equivalent IMO-ProofBench performance by about 100x; the prior advanced model achieved gold-medal standard at IMO 2025 by solving five of six problems. The authors caution that the model may have had exposure to IMO 2024 problems and that IMO 2025 had been public for six months.Source: §2.1 · pp. 4–5, §2.3 · p. 5

2.3. Importance of Tool Use

  • Extensive training for tool use combined with Google Search and web browsing reduced obvious fabricated-paper citations, but subtler errors in reporting real papers’ results remained.Simply granting internet access was insufficient; tool integration shifted citation mistakes toward misrepresenting results in references that do exist.Source: §2.3 · pp. 5–6

3. Summary of Mathematical Research Results

Aletheia contributed results ranging from fully AI-generated mathematical content to high-level strategies and improvements developed with human mathematicians. The final papers were written by human authors, who retained accountability for the papers’ contents and attributions.

3.1. Milestone A: Eigenweights for Arithmetic Hirzebruch Proportionality

  • Aletheia generated all mathematical content in Feng26 without human intervention, deriving general eigenweights through algebraic combinatorics and resolving questions left open in FYZ26.The authors of FYZ26 had first adopted an AI-generated solution to a known eigenweight case, replacing their original proofs.Source: §3.1 · p. 7

3.2. Milestone B: Lower Bounds for Multivariate Independence Polynomials

  • For interacting-particle bounds, Aletheia supplied a high-level dual-set strategy, while Lee and Seo completed rigorous proofs after Gemini 2.5 Deep Think proved a key inequality generalizing SSSZ19.In this workflow, the AI supplied the broader strategy and the humans carried out the rigorous execution.Source: §3.2 · pp. 7–8

3.3. Milestone C: The Erdős Problems

  • Aletheia found first substantive solutions to Erdős-652 and Erdős-1051, and first solutions to one question each in Erdős-654 and Erdős-1040.These four results are the autonomous solutions; experts judged that none individually rose to the level of a research paper.Source: §3.3 · p. 9
  • Aletheia independently rediscovered solutions to Erdős-397, -659, -935, and -1089, and identified existing literature solutions for Erdős-333, -591, -705, -992, and -1105.The authors make no novelty claims for these two categories.Source: §3.3 · p. 9
  • Among 200 candidates adjudicated correct or incorrect, 137 (68.5%) were fundamentally flawed and 63 (31.5%) technically correct; only 13 (6.5%) were meaningfully correct.The evaluation began with 700 open problems; Aletheia flagged 212 responses as potentially correct, and 12 responses were ultimately marked ambiguous. The 13 meaningful results fell into four categories.Source: §3.3 · pp. 8–9, Table 2 · p. 9
  • The authors caution that their initial novelty classifications for the Erdős problems are at best upper bounds, since earlier human solutions may have been missed; significance requires expert mathematicians.Source: §3.3 · p. 10

3.4. Bounds for Polynomial Dyadics

  • Aletheia independently devised a Siegel’s Lemma argument that achieved the best bound among human and autonomous attempts, significantly improving Pagano’s bound and being adopted for publication.The original complexity result depended on a number-theoretic assertion about bounded combinations lying in polynomially many dyadic intervals.Source: §3.4 · p. 10

4. FirstProof

FirstProof provided a rare clean comparison of AI mathematics systems using ten research-level lemmas whose human solutions were not online before the test. Aletheia’s Problem 7 solution was distinct enough from the prior human solution to warrant separate documentation, while the paper contextualizes other systems’ claims and Aletheia’s inference costs.

4. FirstProof

  • FirstProof offered a rare clean comparison through ten research-level lemmas curated by academics, with human solutions withheld online until after the February 5–13, 2026 evaluation window.The problems were sampled from active research mathematicians’ question distribution, and the list was assembled by academics with no connection to AI companies.Source: §4 · p. 11

4.1. Aletheia’s results on FirstProof

  • Two Aletheia runs used different Gemini base models, unchanged FirstProof prompts, and a pre-determined verification and extraction process; only Problem 8’s expert assessment was not unanimous.The reported evaluations were best-of-two by majority expert opinion, and the extraction prompt produced LaTeX directly without manual reformatting.Source: §4.1 · p. 11, Table 3 · p. 12
  • Aletheia’s Problem 7 solution was sufficiently distinct from Cappell–Weinberger–Yan’s prior solution to merit documentation in a separate arXiv paper (FK26).Problem 7 had previously been advertised as open in Weinberger (2023), but the human solution was not published until the FirstProof solutions.Source: §4.1 · p. 11

4.2. Comparisons

  • GPT 5.2 Pro solved Problems 9 and 10 out of the box, while Gemini 3 Deep Think solved Problem 10; these were described as the strongest publicly available model results.OpenAI also claimed likely solutions to Problems 2, 4, 5, 6, 9, and 10, but the authors say Problem 2 was flawed, the other five were regarded as correct, and the work had undisclosed human guidance.Source: §4.2 · pp. 11–12
  • The authors knew of no credible autonomous solutions beyond the Problem 9–10 baseline except Cursor researchers’ Problem 6 solution, which experts reportedly regarded as correct.The paper notes that many parties had attempted the problems.Source: §4.2 · p. 12

4.3. Inference computation

  • Aletheia’s inference cost exceeded the Erdős-1051 reference for every problem, and Problem 7 exceeded previously observed scales by an order of magnitude.The comparison is only indicative because both base models differed from the model used for Erdős-1051; inference cost is presented as a rough proxy for problem difficulty from the agent’s perspective.Source: §4.3 · p. 12

5. Analysis and Discussion

The analysis finds partial success in comparisons with Gemini Deep Think, but low rates of meaningful correctness on open problems and persistent limitations in autonomous mathematical research.

5.1. Ablation studies

  • Gemini Deep Think solved 8 of Aletheia’s 13 solved Erdős problems, using almost exactly twice Aletheia’s average compute per problem.The results were based on human expert grading.Source: §5.1 · p. 13, Table 4 · p. 13
  • On research-paper prompts, Deep Think reproduced FYZ26, failed all three Feng26 prompts, solved only the first LeeSeo26 prompt, and essentially succeeded on BKKKZ26.It produced a satisfactory but less sharp upper bound for ACGKMP26; total compute was comparable to Aletheia’s on this prompt set.Source: §5.1 · p. 13, Table 5 · p. 13

5.2. Accuracy

  • 31.5% of 200 graded Erdős-problem responses were technically correct under some interpretation, but only 6.5% addressed the intended interpretation meaningfully.The 200 responses were filtered from 700 open problems; the study used a November 2025 Gemini 3 base model, weaker than the January 2026 model used for Section 2 and FirstProof.Source: §5.2 · p. 14, Table 6 · p. 14
  • On FirstProof, Aletheia produced candidates for 6 of 10 problems, all judged correct by majority opinion, but only 1 of 10 was considered publication-grade.For the other four problems both agents returned no solution; P8’s assessment was not unanimous, with 5 of 7 experts rating it correct. Most FirstProof problems are technical lemmas rather than standalone publication-worthy results.Source: §5.2 · p. 14, Table 7 · p. 15
  • The FirstProof accuracy and conditional accuracy on answered problems were consistent with observations on FutureMath Basic, a benchmark at a comparable level.Success on research-level problems was rare: the ACGKMP26, Feng26, and LeeSeo26 papers emerged from spontaneous positive outcomes in a broader benchmarking effort where most problems saw no autonomous progress.Source: §5.2 · p. 14

5.3. Weaknesses of AI

  • Autonomous results have been relatively brief and elementary, with successes seeming to rely on technical manipulations or broad knowledge retrieval rather than genuine creativity.The paper notes that the concept of genuine creativity is subjective.Source: §5.3 · p. 14
  • Despite its verifier, Aletheia remains more error-prone than human experts, can misinterpret ambiguous questions toward easier answers, and commonly hallucinates or misrepresents references.The authors relate the ambiguity behavior to specification gaming and reward hacking; internet search does not eliminate reference-related hallucinations.Source: §5.3 · p. 15

6. Representing AI contributions to mathematics

Because frontier mathematics is difficult to evaluate and AI claims can be misleading, the section proposes a framework for describing autonomy and mathematical significance, alongside transparent documentation of human-AI contributions.

6. Representing AI contributions to mathematics

  • Frontier results can be hard to assess even when correct, while limited public expertise and incentives can foster exaggerated or misleading claims about AI’s mathematical contributions.The authors present their framework as a starting point for responsible communication, not a universal standard; they say any standard should emerge from the mathematical community.Source: §6 · pp. 15–16

6.1. Autonomous Mathematics Levels

  • The proposed taxonomy has separate axes for AI autonomy and mathematical significance, preserving broad distinctions to limit subjective disputes.The autonomy axis describes the relative contributions of humans and AI; the significance axis measures the result regardless of how it was produced.Source: §6.1 · p. 16, Table 8 · p. 16, Table 9 · p. 17

6.1.1. Discussion and Examples for Level of Autonomy.

  • The authors classify (Feng26) and as Level A, (LeeSeo26) and (BKKKZ26) as Level C, and (FYZ26) and (ACGKMP26) as Level H.Level A involves humans mainly posing questions or correcting minor inaccuracies; Level C involves essential human and AI contributions, whereas Level H denotes AI contributions that are non-trivial but minor or inspirational.Source: §6.1.1 · pp. 16–17

6.1.2. Discussion and Examples for Level of Significance.

  • The authors classify their Erdős-652, 654, 935, and 1040 solutions as A0, Erdős-1051 as A1, (Feng26) as A2, (BKKKZ26) and (LeeSeo26) as C2, and (ACGKMP26) and (FYZ26) as H2.Significance levels are deliberately coarse because judgments are subjective and domain-specific; Level 2 spans very minor to extremely influential work and does not imply AI has reached the level of human mathematicians.Source: §6.1.2 · pp. 17–18

6.2. Documenting Human-AI Collaboration

  • Human-AI Interaction Cards document examples including Aletheia’s fully correct eigenweight solution in (Feng26), Gemini’s correct solution and Aletheia’s proof outline for (LeeSeo26), and Aletheia’s correct solution for (BKKKZ26).The LeeSeo26 outline includes dual sets and log convexity, reduction techniques, and key lemmas; humans worked out its details and devised simpler proofs.Source: §6.2 · pp. 18–19
  • When a card template is unsuitable, the authors propose exposing the most important raw prompts and outputs containing essential AI-generated insights for Level C or Level A results.They leave specific standards to mathematicians and describe the proposal as a possible common baseline for transparency.Source: §6.2 · p. 19

7. Reflections on the Impact of AI in Mathematics

The authors say AI’s impact on pure mathematics research remains limited: solving some problems that eluded experts does not show that AI matches human mathematicians. Instead, they argue that AI’s distinct strengths may help with certain kinds of problems.

Reflections on the Impact of AI in Mathematics

  • The reported solutions to some problems that eluded experts do not indicate that AI has matched or will match human mathematicians.The authors frame these results as evidence that AI’s comparative advantages can help with certain kinds of problems.Source: §7 · pp. 19–20
  • Frontier models have shallower subject knowledge than domain experts but superhuman breadth, which may suit problems requiring vast memory, computation, or knowledge breadth.Source: §7 · p. 20
  • AI’s lack of human physical limitations may help address open questions left unresolved because experts have limited time and attention, as the Erdős problems illustrate.The authors note that AI is bottlenecked by different factors than humans, which can be advantageous in the right context.Source: §7 · p. 20

8. Related Work

Prior work has advanced mathematical reasoning to Olympiad-level performance and applied AI to mathematical research, while exploring varied human–AI collaboration frameworks. The community nevertheless needs transparent standards for documenting, evaluating, and communicating AI-generated mathematics.

Advances in Mathematical Reasoning

  • Recent reasoning systems have reached gold-medal standards at the IMO, while new benchmarks target research-level mathematics.Prior systems also show proficiency on IMO-ProofBench; cited examples include (Deep Think team, 2025; OpenAI, 2025),, (Luong et al., 2025), (Glazer et al., 2024; Nie et al., 2025; Tao, 2026).Source: §8 · p. 20

AI-Assisted Research Results

  • AI has assisted mathematical research on specific problems, broader mathematical subfields, accessible conjectures, and mathematics-adjacent domains.Examples include work on moduli spaces, genus-zero maps, Nesterov’s method, discrete and convex analysis, combinatorics, and case studies across theoretical computer science, economics, and physics (Schmitt25; BEMSV26; JangRyu25; IvanisviliXie25; Salim25; FeldmanKarbasi25; GGTW25; Woodruff et al., 2026).Source: §8 · p. 20

Frameworks for Human-AI Collaboration

9. Conclusion · A. Case Study: FutureMath Basic

The paper presents Aletheia as a specialized math-reasoning agent intended to enhance mathematicians through informal natural-language verification, given current limitations in language models and formal verification systems. The case study introduces a FutureMath Basic Ph.D.-level exercise on which Gemini 3 Deep Think made negligible progress.

9. Conclusion

  • The authors envision AI as a tool that enhances rather than replaces mathematicians.They note that current language models need human correction for unreliable reasoning and hallucinations, while formal verification systems cannot yet formulate questions on most research frontiers.Source: §9 · p. 21
  • Current natural-language models struggle to reason reliably without human correction of mistakes and hallucinations.Source: §9 · p. 21
  • Formal verification systems are not yet capable of formulating questions of interest on most research frontiers.Source: §9 · p. 21
  • Aletheia uses specialized math-reasoning agents with informal natural-language verification to help mathematicians harness AI.Source: §9 · p. 21

A. Case Study: FutureMath Basic

Large Deviation Analysis of the Phase Transition in the Mean-Field Potts Model … B. Case Study: FutureMath Basic

Aletheia analyzes the mean-field Potts model’s phase transition by reducing its free-energy optimization to one dimension and identifying when the uniform distribution ceases to maximize it. The paper also presents the problem as a FutureMath Basic case solved using search, where Gemini Deep Think made little progress.

Large Deviation Analysis of the Phase Transition in the Mean-Field Potts Model

  • Large deviation theory reduces the free-energy optimization to a one-dimensional problem, yielding the exact critical temperature of the first-order transition.The analysis solves the resulting algebraic equations to determine the maximum inverse temperature for which the uniform empirical distribution determines the free-energy density.Source: Large Deviation Analysis of the Phase… · p. 26

Introduction and Formulation via Empirical Measures

  • Sanov’s Theorem and Varadhan’s Lemma express the asymptotic free-energy density as the supremum of the energy-minus-entropy functional over the probability simplex.Configurations are represented by empirical measures of occupation frequencies.Source: Introduction and Formulation via… · pp. 26–27

The Uniform Distribution and Symmetry Breaking

  • The uniform distribution is globally maximizing exactly when it attains the global maximum, and the only other candidate is a state with one large component and q−1 equal small components.Stationarity and strict convexity imply at most two distinct component values; second-order stability restricts local maxima to multiplicities 1 or q.Source: The Uniform Distribution and Symmetry… · p. 27

Determination of the Critical Inverse Temperature

  • For q≥3, the first-order transition occurs when a secondary local maximum at x>1/q rises to match the uniform state’s height.The critical inverse temperature βmax is defined by this equal-height condition.Source: Determination of the Critical Inverse… · p. 27

1. Stationarity: ℎ′(𝑥𝑐) = 0

  • The unique non-trivial stationary solution in (1/q, 1] is xc=(q−1)/q.The analysis substitutes this value into the stationarity equation and checks the equal-height condition against the uniform state.Source: §1 · p. 28

Conclusion

  • For β≤βmax, the uniform distribution globally maximizes the free-energy functional; for β>βmax, a non-uniform configuration has strictly greater free energy.The free-energy density limit in the uniform regime is β/(2q) + log q.Source: Conclusion · p. 28

B. Case Study: FutureMath Basic

  • Aletheia solved the FM-Grad-011 FutureMath Basic problem using search, while Gemini Deep Think made little progress.The problem asks for the maximum β for which the stated equality holds.Source: B. Case Study: FutureMath Basic · p. 29

Large Deviation Analysis of the Phase Transition in the Mean-Field Potts Model … 1. Theoretical Lower Bound

The paper uses large deviations and symmetry analysis to characterize the mean-field Potts model’s critical temperature, then presents an IMO tiling case study with a subsequence-based lower bound. Together, these sections connect the Potts model’s global-maximizer change to a geometric bound for a 2025-grid tiling problem.

Large Deviation Analysis of the Phase Transition in the Mean-Field Potts Model

  • Large deviation theory reduces the Potts-model free-energy optimization to a one-dimensional problem and identifies the exact critical temperature.The analysis determines the maximum inverse temperature for which the uniform empirical distribution determines the free energy density.Source: Large Deviation Analysis of the Phase… · p. 29

Introduction and Formulation via Empirical Measures

  • Configurations are represented by empirical state frequencies, allowing the energy to depend on the empirical measure; Sanov’s theorem and Varadhan’s lemma then express asymptotic free energy as a simplex supremum.The empirical measure lies in the (q−1)-dimensional probability simplex.Source: Introduction and Formulation via… · pp. 29–30

The Uniform Distribution and Symmetry Breaking

  • Strict convexity of the stationarity equation limits critical points to two component values, while stability leaves only the uniform state or one large and q−1 small components as global-maximizer candidates.The nonuniform candidate has the form (x, y, …, y), with x + (q−1)y = 1.Source: The Uniform Distribution and Symmetry… · p. 30

Determination of the Critical Inverse Temperature

1. Stationarity: ℎ′(𝑥𝑐) = 0

  • The equal-height and stationarity conditions have the unique nontrivial solution xc=(q−1)/q in (1/q, 1].Source: §1 · p. 31

Conclusion

  • For β≤βmax, the uniform distribution globally maximizes the free energy; for β>βmax, a nonuniform configuration has strictly larger free energy, marking a first-order transition.The free energy density equals β/(2q) + log q in the uniform-maximizer regime.Source: Conclusion · p. 31

C. Case Study: Solving IMO 2025 Problem 6

  • The IMO 2025 case study asks for the minimum number of rectangular tiles on a 2025×2025 grid with exactly one uncovered square in every row and column; Gemini Deep Think received only the raw problem under restricted conditions.The model was run at extreme scale, equivalent to 2^12 in Figure 2a.Source: C. Case Study: Solving IMO 2025… · p. 32

1. Theoretical Lower Bound

  • For 2025 holes, the increasing and decreasing subsequence lengths satisfy ab≥2025, and their sum is minimized at a=b=45, yielding the stated tile-count lower bound.The lengths correspond geometrically to the longest diagonally down-right and down-left sequences of holes.Source: §1 · pp. 32–33

2. The Optimal Tiling Construction … 3. Forcing Penalties via Monotonic Subsequences

The sections establish that Matilda’s grid can be tiled with exactly 2112 rectangles, matching the theoretical minimum. They give a symmetric construction and develop a lower-bound argument using rectangle-corner counting, segment bounds, and monotone subsequences.

2. The Optimal Tiling Construction

  • With k = 45, a symmetric 45 × 45 macro-block arrangement limits both a and b to below 45 and places one hole in each block.The shifted pattern makes one hole occur in every absolute row and column, while leaving orthogonal channels for the tiles.Source: §2 · p. 33
  • Matilda’s optimal tiling uses exactly 2112 rectangles, matching the theoretical lower bound.The construction has one hole in every row and column and partitions the remaining squares without wasted cuts.Source: §2 · p. 33, §3 · p. 36
  • An expert assessment gave the preliminary solution only 1–3 points because it relied on unproved advanced results, so the model was prompted to produce an elementary, self-contained proof.At inference scale 28, the refinement prompt yielded a correct solution.Source: §2 · p. 34

1. The Rectilinear Partition Formula

  • Corner counting gives the exact relation T = H + V + I + 1 − N for the number of tiles T.The count includes rectangle corners at grid corners, internal crossings, and T-junctions formed by maximal internal segments.Source: §1 · pp. 34–35

2. Segment Bounds and Chords

  • Each internal horizontal line contains at least 1 + u_y maximal horizontal segments, yielding a lower bound on H; crossing indicators similarly bound I.The bounds are substituted into the corner-counting formula to obtain the main lower bound.Source: §2 · p. 35

3. Forcing Penalties via Monotonic Subsequences

  • Each gap between adjacent terms of a longest increasing subsequence forces a segment or crossing penalty in the lower bound.The empty box between consecutive subsequence holes forces the intervening hole columns to jump across it.Source: §3 · pp. 35–36
  • Longest decreasing subsequence gaps force analogous penalties, and their evaluated coordinates are disjoint from those for increasing-subsequence gaps.The opposite directions of the required column inequalities prevent double-counting; the resulting penalties are substituted into the main bound.Source: §3 · p. 36

4. The Optimal Construction … Step 5: Eventual Periodicity via Deterministic Transitions

The paper presents a 2112-tile construction matching a proven lower bound and a model-generated proof that at least one gender’s sequence is eventually periodic. The proof reduces the generation rule to occurrence counts, characterizes recurring values, and derives periodicity from a finite deterministic state system.

4. The Optimal Construction

  • A symmetric macro-block arrangement restricting both a and b to exactly 45 achieves the absolute minimum of exactly 2112 tiles, matching the proven lower bound and ruling out covers with fewer tiles.Source: §4 · pp. 36–37

D. IMO 2024 Case Studies / D.1. Problem 3: Success at 27 Scale

  • Gemini Deep Think solves a variant of IMO 2024 Problem 3 at inference compute scaled to 27, with a miscellaneous mistake; the paper cautions that post-cutoff knowledge leaves possible contamination.The authors argue that the substantial scaling required suggests robust reasoning rather than mere memorization.Source: §D.1 · p. 37, D. IMO 2024 Case Studies · p. 37

Model-Generated Solution / Step 1: Reformulating the Generation Rule

Step 2: Bounding the Frequencies of Large Numbers

  • No integer greater than M0 can appear more than M0 times, bounding the global frequencies of all sufficiently large values.M0 is the maximum of N and the initial terms a_1 through a_N.Source: Step 2: Bounding the Frequencies of… · p. 38

Step 3: Characterizing the Infinitely Occurring Elements

  • The set S of infinitely recurring values is nonempty and equals {1, 2, …, L}; every integer V > M2 appears exactly L times.Each such V can be reached only by the counts of the L elements in S, and its appearances generate counts 1 through L.Source: Step 3: Characterizing the Infinitely… · p. 38

Step 4: Strict Alternation Between Small and Large Numbers

  • After a sufficiently large step, the sequence alternates between values in S and values outside S, so one gender eventually chooses only from S.The other gender chooses values greater than M2.Source: Step 4: Strict Alternation Between… · p. 39

Step 5: Eventual Periodicity via Deterministic Transitions

  • The recurring choices s_n evolve through a deterministic transition on occurrence-count vectors, and bounded gaps between the sorted counts make the normalized state space finite.The state X_n = (s_(n+1), v_n − min(v_n)1) therefore eventually cycles, making {s_n} periodic.Source: Step 5: Eventual Periodicity via… · pp. 39–40
  • Because {s_n} is eventually one gender’s sequence, at least one of the boys’ or girls’ sequences is eventually periodic.The argument applies whether the recurring choices belong to the girls or, symmetrically, the boys.Source: Step 5: Eventual Periodicity via… · p. 40

D.2. Problem 5: Success at 28 Scale … Conclusion

Aletheia solved the IMO 2024 Problem 5 variant only at scale 28, with a state-tracking strategy establishing that the smallest penalty threshold is 3. The solution pairs a lower bound showing Peter can force two penalties with an upper bound showing James can still win after at most two.

D.2. Problem 5: Success at 28 Scale

  • The variant required more compute, with success achieved only at scale 28.Source: §D.2 · p. 40
  • Rather than use shape-based path heuristics, the model tracks safe and trapped columns and avoids the first-row case split common in public solutions.The passage characterizes this as an alternative strategy derived from first principles.Source: §D.2 · p. 40

Model-Generated Solution

1. Lower Bound: Peter can force at least 2 penalties (𝑛≥3)

  • Peter can force two penalties by placing traps at the first row-2 and then row-3 cells James visits, so James requires n≥3.The second trap can occupy a different column from the first, preserving the at-most-one-trap-per-column rule.Source: §1 · p. 41

2. Upper Bound: James can always win with at most 2 penalties (𝑛≤3)

  • James probes available columns row by row, stopping at a trap; after his second penalty, the discovered-column structure lets him reach the finish safely.If he completes probing with at most one penalty, the remaining column is trap-free and provides a safe route.Source: §2 · pp. 41–42

Conclusion

  • The smallest positive integer n is 3: Peter can force two penalties, while James can reach the last row with at most two.Thus, James wins before reaching 3 penalty points.Source: §1 · p. 41, §2 · p. 41, Conclusion · p. 42

Related papers

Loading 2602.10177v3…