Source-linked AI summary
First Proof
Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, Lauren Williams
TL;DR
The paper addresses how to assess whether AI systems can solve research-level mathematics independently, beyond artificial contest-style benchmarks. It proposes ten naturally occurring, unpublished research questions with author-known proofs, focusing on the final proof-writing stage and testing current systems under a controlled protocol. Preliminary one-shot tests indicate that the best publicly available systems struggle with many questions, while the collection remains a preliminary, human-graded methodology rather than a formal benchmark.
Problem
Existing math benchmarks do not establish where AI systems stand on solving naturally occurring research-level questions independently, while search capabilities and problem-solving capabilities are difficult to disentangle.
Method
The paper presents ten unpublished questions drawn from authors’ research, with proofs supplied by the authors, and evaluates systems on the final stage of producing answers to well-formed statements.
Results
The best publicly available AI systems struggle with many questions when given one shot to produce an answer.
Takeaways & Limitations
The project provides a preliminary methodology for assessing autonomous research-level mathematical proof solving and for developing a more structured benchmark.
Takeaways & Limitations
The question set is not yet a formal benchmark because it is small, lacks formal grading, and requires human experts to assess answers that may not be unique.
Abstract
from arXiv · showhide
To assess the ability of current AI systems to correctly answer research-level mathematics questions, we share a set of ten math questions which have arisen naturally in the research process of the authors. The questions had not been shared publicly until now; the answers are known to the authors of the questions but will remain encrypted for a short time.
1 Introduction
The paper proposes a preliminary, realistic assessment of AI systems on research-level mathematics by testing questions drawn from mathematicians’ work and not previously published. The experiment focuses on producing proofs for well-formed questions, while highlighting contamination, grading, scale, and scope limitations.
- Design: The proposed test uses questions that arose naturally in mathematicians’ research, were solved by their authors, and had not been posted publicly.This design is intended to separate problem-solving from literature-search capabilities and reduce data contamination.
- Design: The collection contains 10 questions across diverse mathematical fields, with author-written proofs generally limited to roughly five pages or less.The page restriction reflects technical limitations of current publicly available AI systems, and many questions are components of larger works.
- Scope: Research-level mathematics includes question selection, definition-building, and theory development, but this experiment targets the final stage of proving well-formed statements.The authors describe this as a first step rather than a complete evaluation of mathematical research.
- Limitations: The question set is not yet a formal benchmark because it is small, lacks a formal grading scheme, and requires human experts to assess potentially non-unique proofs or counterexamples.The authors invite community experimentation to inform prompting, answer formats, grading, contamination analysis, and a future structured benchmark.
- Initial evaluation: Preliminary one-shot tests indicate that the best publicly available AI systems struggle with many questions.The authors did not iteratively interact with systems or rerun queries under their stated protocol.
2 The questions
The paper presents ten research-level questions spanning multiple areas of mathematics, each formulated as a concrete proof, existence, construction, or computational problem. The questions include measure equivalence, representation theory, Markov chains, polynomial inequalities, topology, graph Laplacians, symplectic geometry, tensor relations, and iterative numerical methods.
- Question 4: One problem asks whether finite free convolution preserves a reciprocal Fisher-information inequality for monic real-rooted polynomials.The question defines Φ_n and asks whether 1/Φ_n(p ⊞_n q) ≥ 1/Φ_n(p) + 1/Φ_n(q).
- Question 5: The equivariant-topology problem asks for an O-slice filtration and a geometric-fixed-point characterization of O-slice connectivity.It is posed for a finite group and an incomplete transfer system associated with an N∞ operad.
- Questions 6–9: The remaining geometric and algebraic questions ask about light vertex subsets, acyclic universal covers, Lagrangian smoothings, and polynomial relations among determinant-defined tensors.The tensor problem requires a polynomial map with degree bounds independent of n and a specified characterization of rescaling relations.
- Question 10: The final question asks for an efficient preconditioned conjugate-gradient method for an unaligned tensor CP-decomposition subproblem with an infinite-dimensional RKHS-constrained mode.The method must avoid O(N) computation, explain matrix-vector products and preconditioning, and provide complexity analysis; direct solving costs O(n^3r^3).
3 Related work
The paper distinguishes its question set from existing research-mathematics benchmarks by emphasizing proof-based, naturally occurring questions and a different balance between privacy, public inspection, and grading.
- Existing benchmarks: FrontierMath contains several hundred private expert-level problems whose final answers are structured as integers or symbolic expressions.A subset of its problems and solutions is available to OpenAI, while EpochAI has access to the full solutions.
- Existing benchmarks: IMProofBench evaluates research-level proof creation with automatically gradable subquestions, but full correctness still requires human experts and its questions are private.Its design differs from the paper’s public question set.
- Existing benchmarks: RealMath scrapes post-cutoff arXiv questions, emphasizes fields with constructive theorems, and uses short symbolic or numeric answers to facilitate automatic grading.Unlike FrontierMath and IMProofBench, it makes questions public and refreshes them periodically to reduce contamination.
4 Implementation details
The implementation process tested more questions than the final ten to identify the boundary of current systems’ capabilities while preserving question privacy and applying selection criteria.
- Selection process: Roughly 20 research-level questions were tested over several weeks using Gemini 3 Pro, GPT-5.1 Pro, and GPT-5.2 Pro.The final selection required that testing reveal no previously unknown answer and that a one-page statement suffice for system understanding.
- Selection process: The selected questions also required author agreement to release human-generated proofs within specified length and timeframe constraints.The criteria were intended to support a consistent public release.
- Privacy and probing: Testing beyond ten questions was used to probe the boundary between solvable questions and questions beyond the models’ reach.The authors disabled training-data sharing but note that providers retained data for three days at Google and thirty days at OpenAI.
5 Discussion
The First Proof experiment targets the final, most measurable stage of mathematical research: finding and rigorously proving answers to selected research questions. The authors plan additional question sets, gradually relaxing constraints and expanding evaluation to other aspects of research mathematics.
- Mathematical research includes selecting questions, developing theories, and finding and proving answers.
- The experiment focuses on finding answers to selected questions, not creating research questions or developing novel theories.
- The authors plan a second set of similar questions that could serve as a benchmark for testing AI capabilities.
- Future releases may remove artificial constraints such as length and measure performance across additional aspects of research mathematics.
A First Proof Solutions and comments
The authors tested Gemini 3.0 Deep Think and ChatGPT 5.2 Pro on the questions using prompts requesting rigorous, complete answers in compilable LaTeX. One prompt explicitly discouraged web search, and the authors then reviewed the best solutions.
- Gemini 3.0 Deep Think and ChatGPT 5.2 Pro were tested on February 4 and 5, 2026.
- The primary prompt requested a rigorous, complete answer formatted as a compilable LaTeX document.
- A second prompt requested reasoning without web search while retaining the same rigor and formatting requirements.
- The authors commented on the best LLM solutions obtained in these internal tests.
A.10 Question 10: Tammy Kolda
For Question 10, the best LLM solution was correct and reduced computational complexity relative to the author's solution, but its central idea was also found in prior work and its citations were inadequate.
- The best LLM solution was correct and lowered computational complexity relative to the author's solution.
- A search found the solution's main idea in an earlier arXiv paper, although the authors were unsure whether it was the only source.
- The solution lacked appropriate citations, though the authors otherwise considered it good and planned to borrow aspects of it.
B The human-generated solutions to our problems
The authors' solutions are identical to those encrypted on February 5, 2026, and released on February 13, 2026.
- The presented solutions match the solutions encrypted on February 5, 2026, and released on February 13, 2026.
Proof of the lemmas
The lemmas establish the required probabilistic and analytic bounds using Sobolev embeddings, Gaussian-polynomial moment equivalence, integral estimates, and Borel–Cantelli. Lemma B.3 specifically provides a lower bound on γ that distinguishes shifted from non-shifted measures.
- The proof of Lemma B.2 uses the embedding W β,2p ,→W β−d and equivalence of moments for Gaussian polynomials.
- The proof concludes with a standard Borel–Cantelli argument.
- Lemma B.3 provides a lower bound on γ ensuring that Aγ or Bγ is distinguishable under the shifted measure from the non-shifted measure.
- The proof of Lemma B.3 expands cN,2 and bounds the resulting sum from below by an integral multiple of Z N.
These are compatible with the natural nullification functors
The appendix develops O-slice connectivity through suspension, geometric fixed points, isotropy separation, and geometric Mackey functors. It characterizes connectivity using subgroup data and shows that the resulting descriptions are compatible with natural nullification constructions.
- These are compatible with the natural nullification functors: Ordinary suspension yields maps between O-slice structures because suspension commutes with homotopy colimits and induction.
- These are compatible with the natural nullification functors: For any k ≥0, the ∞-category of O-k-slices is discrete.
- These are compatible with the natural nullification functors: Geometric fixed points detect slice connectivity, making geometric connectivity a central subgroup-indexed notion.
- These are compatible with the natural nullification functors: The characteristic function χO and admissible G-sets determine the connectivity bounds through orbit cardinalities.
- These are compatible with the natural nullification functors: For a geometric Mackey functor M, HM is a k[G : χO(G)]-slice.
- These are compatible with the natural nullification functors: The full O-slice connectivity is obtained by combining geometric-spectrum estimates with isotropy separation and induction on the subgroup lattice.
B.10 Question 10: Tammy Kolda
This section introduces the system to be solved and surveys direct, transformed, and iterative approaches. It also compares their costs and performance while addressing the indefiniteness of the original symmetric system.
- The system to be solved is introduced as the central problem of the section.
- The paper considers direct, eigendecomposition-based transformed, and iterative methods, with regularization used in the direct and iterative approaches.
B.10.1 Direct Solution of UI Subproblem (Symmetric Form)
The direct method regularizes and restructures the symmetric system while avoiding explicit formation of a large Kronecker product. It computes the needed matrix through sampled rows associated with known tensor entries.
- Regularization with ρ > 0 modifies the indefinite symmetric system to ensure positive definiteness.
- The right-hand side is rewritten by pulling K inside the vectorization, with F = ST(Z ⊗K).
- The method avoids forming the N × nr Kronecker product Z ⊗K explicitly by constructing special matrices ˆK and ˆZ.
- Rows of ˆZ and ˆK correspond to known tensor-entry indices, and their elementwise products determine rows of F.
B.10.2 Transforming the UI Subproblem
The subproblem is transformed using the eigendecomposition of K into an equivalent system in transformed variable W̄, with regularization incorporated in the transformed formulation.
- B.10.2 Transforming the UI Subproblem: K = UDU^T enables factoring the original system through (I_r ⊗ U) to obtain an equivalent transformed system.The transformed formulation is intended to improve conditioning.
- B.10.2 Transforming the UI Subproblem: The transformed variable is W̄ = U^T W, and the original solution is recovered as W = U W̄.D cannot be absorbed into W̄ because it is indefinite.
- B.10.2 Transforming the UI Subproblem: The transformed system defines F̄ using Z ⊗ UD and B̄ using DU^T B before adding regularization.The modified system includes λ(I_r ⊗ D) and ρI_rn.
B.10.3 Key Lemmas for PCG Solution of UI Subproblem
The section develops reusable identities for matrices whose rows are Kronecker products, allowing PCG products and preconditioner terms to be computed without explicitly forming the large matrix.
- Matrix structure: The rowwise Kronecker structure C(ℓ,:) = A(ℓ,:) ⊗ B(ℓ,:) underlies the subsequent matrix-vector identities.For vectorization, index k corresponds to matrix entry (i,j) with k = i + (j − 1)n.
- Matrix-vector products: O(q(r + n)) operations compute Cx without explicitly forming C, reducing memory from O(qrn) to O(q(r + n)).The identity is Cx = (A ∗ BX)1_r for x = vec(X).
- Transpose products: C^T v = vec(B^T diag(v)A) computes the transpose matrix-vector product without forming C, while retaining O(qrn) arithmetic cost.This identity is used for efficient products involving the structured matrix.
B.10.4 PCG Solution of Transformed UI Subproblem
The transformed system is solved with PCG by exploiting structured products involving F̄ and by using a diagonal preconditioner rather than explicitly forming Kronecker products.
- Matrix-vector products: For x = vec(X), Lemmas 1 and 2 provide the structured computation of F̄^T F̄x used in conjugate-gradient iterations.The matrix-vector products avoid forming Kronecker products explicitly.
- Preconditioning: A diagonal preconditioner is proposed, with its final construction relying on Lemma 3.The preconditioner uses the efficiently computed diagonal terms described in the preceding lemmas.
B.10.5 Comparison of Costs
The cost comparison contrasts a direct solve of the original system with PCG on the transformed system, emphasizing lower computational and storage demands for PCG under the stated incomplete-data regime.
- Assumptions and setup: d < n and r ≪ q are assumed, while n and r need not have a fixed relative ordering.Here d is tensor order, n is the mode-k size, r is target rank, and q is the number of known entries.
- Shared costs: O(qrd) computes Ẑ, while the incomplete-tensor MTTKRP B can be reduced from O(qrd) to O(qr) using Ẑ.These costs are shared by both direct and PCG methods.
- Direct method: O(qrn) storage and O(qr^2n^2) work arise when explicitly forming F and F^T F for the direct solve.The direct system has size rn × rn and also requires forming the right-hand side.
- PCG method: The PCG method is orders of magnitude cheaper than the direct method, with cost depending on the iteration count p and substantially lower storage requirements.The eigendecomposition of K costs O(n^3) but is performed once before the outer alternating-optimization iterations.