Source-linked AI summary
Aletheia tackles FirstProof autonomously
Tony Feng, Junehyuk Jung, Sang-hyun Kim, Carlo Pagano, Sergei Gukov, Chiang-Chiang Tsai, David Woodruff, Adel Javanmard, Aryan Mokhtari, Dawsen Hwang, Yuri Chervonyi, Jonathan N. Lee, Garrett Bingham, Trieu H. Trinh, Vahab Mirrokni, Quoc V. Le, Thang Luong
TL;DR
The paper examines how Aletheia, a mathematics research agent, performed on the inaugural FirstProof challenge under an explicit interpretation of autonomy and correctness. It describes the autonomous solution pipeline and expert evaluation, reporting majority-approved solutions for 6 of 10 problems, with non-unanimous assessment only for Problem 8.
Problem
The paper addresses where AI systems stand on solving research-level mathematics questions independently, without an expert in the loop.
Method
Aletheia received unmodified FirstProof problems, passed its outputs through a predetermined verification and extraction prompt, and was evaluated without interacting with the model.
Results
6 of 10 FirstProof problems received candidate solutions that majority expert opinion judged Correct under the minor-revisions interpretation.
Takeaways & Limitations
Aletheia’s best-of-2 evaluation produced credible solutions to all six problems for which either agent generated candidates.
Takeaways & Limitations
The study reflects the authors’ own interpretation of FirstProof, and the challenge is not intended as a formal benchmark.
Abstract
from arXiv · showhide
We report the performance of Aletheia (Feng et al., 2026b), a mathematics research agent powered by Gemini 3 Deep Think, on the inaugural FirstProof challenge. Within the allowed timeframe of the challenge, Aletheia autonomously solved 6 problems (2, 5, 7, 8, 9, 10) out of 10 according to majority expert assessments; we note that experts were not unanimous on Problem 8 (only). For full transparency, we explain our interpretation of FirstProof and disclose details about our experiments as well as our evaluation. Raw prompts and outputs are available at https://github.com/google-deepmind/superhuman/tree/main/aletheia.
1. Introduction
Aletheia’s FirstProof performance is summarized alongside transparency materials describing its human-AI interaction and evaluation process. The study is explicitly limited to the team’s own effort.
- Table 1 summarizes Aletheia’s performance on the FirstProof challenge using expert ratings of solution correctness.The expert-evaluation column reports the number of experts rating each solution Correct out of those consulted.
- Only the assessment on Problem 8 was not unanimous.
- The authors emphasize that this is a limited study by the Aletheia team and is not representative of Google’s collective FirstProof efforts.
- The authors provide a Human-AI Interaction Card describing how they obtained the FirstProof solutions.
- The study includes the verbatim FirstProof problem prompt, a verification and extraction prompt, and the Gemini 3 Deep Think response.
2. Interpretation of the challenge
The authors interpret FirstProof as requiring autonomous mathematical proofs meeting literature standards, while acknowledging ambiguity in autonomy and correctness. They stress that this interpretation is their own and that FirstProof is not a formal benchmark.
- The authors interpret a solution as an autonomous proof conforming to prevailing standards of mathematical rigor and scholarship.Their interpretation excludes human input for mathematical ideas or for isolating the problem’s core.
- The authors identify unresolved ambiguity over whether human clarification during peer review is compatible with an autonomous solution.For FirstProof-level problems, expertise may be needed to identify weak points before clarification can be requested.
- Human expertise selecting the best solution among multiple attempts could offer a potentially huge performance advantage.The authors view that advantage as orthogonal to evaluating AI capability.
- They define Correct as publishable after minor revisions within the established range of peer review, rather than publication-ready as originally generated.Some generated solutions did not meet the challenge’s stated citation requirements, although they met prevailing literature standards.
- The authors state that this is their own interpretation, other reasonable interpretations exist, and FirstProof is not intended as a formal benchmark.
3. Methodology and results
Aletheia received unmodified FirstProof problems, passed its outputs through a predetermined verification and extraction prompt, and was evaluated without model interaction. Best-of-2 evaluations judged six problems solved, with disagreement only on Problem 8, while four problems yielded no solution.
- 3. Methodology and results: Aletheia was prompted with unmodified FirstProof problem statements, and its outputs were filtered through a predetermined verification and extraction prompt.The prompt produced LaTeX directly so manual reformatting was unnecessary.
- 3. Methodology and results: The evaluation process did not interact with the model, including by requesting clarification or elaboration.
- 3.1. Aletheia (Best of 2): 6 of 10 FirstProof problems produced candidate solutions that majority expert opinion judged Correct under the minor-revisions interpretation.The problems were P2, P5, P7, P8, P9, and P10; P8 was the only non-unanimous assessment.
- 3.1. Aletheia (Best of 2): 4 problems produced no solution from either agent within the time limit.These were P1, P3, P4, and P6; the authors describe self-filtering as a key design principle focused on reliability.
- 3.2. Evaluations: Problem 8’s evaluation involved five Correct judgments among seven experts, with disagreement centered on whether missing detail exceeded the minor-revisions threshold.
- 3.3. Further comparisons: Each agent individually produced at least one false positive, while their best-of-2 performance yielded credible solutions to all six candidate problems.The authors associate this outcome with improved accuracy over the December 2025 Aletheia version and changes to agentic scaffolding and base models.
- 3.2. Evaluations: The extraction prompt filtered out a P3 submission, marked P5 and P7 from Aletheia A as fixable, and left other outputs unchanged after marking them Correct.
B. Pre-deadline evaluations
The pre-deadline evaluation used best-of-2 submissions and was later superseded by broader expert assessment, with several initial judgments revised. These records document both the original choices and important corrections, including disagreement over Problem 8.
- Evaluation setup: Best-of-2 submissions were recorded for each problem sent to the FirstProof authors on February 13, 2026.Aletheia Af was aborted after solutions to P2 and P9, while Aletheia B was later run on selected problems to preserve the best-of-2 setup.
- Revised judgments: P2 and P9 submissions initially left unread were later found Correct, whereas P5 was later judged a Misinterpretation of the question.These verdicts concerned Aletheia B’s submissions.
- Revised judgments: P7 was initially guessed Incorrect because of late appearance and limited expertise, but later closer examination found the solution Correct.The initial judgment was explicitly described as conservative.
- Revised judgments: Problem 8 changed from an initial Correct assessment to Inadequate after experts identified gaps and possible errors that fell short of typical proof standards.The reassessment was not unanimous in the supplied commentary.
- Revised judgments: Aletheia A’s P10 solution was unanimously restored to Correct after a miscommunication, and its precomputation removed the O(q) dependency from the iterative PCG loop.The authors instead presented Aletheia B’s solution as their initial first-choice submission in Appendix C.6.
C. Raw prompts and outputs
The appendix reproduces the FirstProof prompts, selected outputs, and evaluation context across several mathematical problems. It includes problem statements, formal conditions, computational settings, and an independent public-model comparison for Problem 10.
- C. Raw prompts and outputs: The appendix presents raw prompts and first-choice outputs for FirstProof problems, alongside selected expert commentary from the original evaluation.These materials correspond to the pre-deadline submissions sent to the FirstProof authors.
- C.1. Problem 2: Problem 2 asks whether a Whittaker-model function exists with a specified property for a generic representation of GL_{n+1}(F).The setup uses a non-archimedean local field, an upper-triangular unipotent subgroup, and a nontrivial additive character.
- C.5. Problem 9: Problem 9 asks for algebraic relations among determinant-defined 3×3×3×3 tensors generated from Zariski-generic matrices.It seeks a polynomial map F independent of the matrices and with degree bounds independent of n.
- C.5. Problem 9: The Problem 9 condition requires F to vanish exactly when nonzero coefficients factor as λαβγδ=uαvβwγxδ over non-identical index quadruples.The tensors’ entries are determinants formed by vertically concatenated matrix rows.
- C.7. Independent Public Deep Think Evaluation for Problem 10: Problem 10 asks for an efficient iterative preconditioned conjugate-gradient method for an RKHS-constrained CP-decomposition subproblem with missing tensor entries.The formulation fixes all factor matrices except the mode-k factor matrix and compares against the O(n^3r^3) cost of a standard linear solver.
- C.7. Independent Public Deep Think Evaluation for Problem 10: The independent Problem 10 evaluation used publicly available Gemini 3 Deep Think with human-guided sampling and concatenation of several generated outputs.The resulting solution was sent to the FirstProof authors before the deadline.
- C.7. Independent Public Deep Think Evaluation for Problem 10: The public-model output reduces per-iteration cost to O(n^2r+nr^2) by pre-aggregating geometry and using an exact block-Jacobi preconditioner, removing q from the iterative loop.This is stronger than Aletheia Agent B’s O(qr) per-iteration term when q=ω(n).
- C.7. Independent Public Deep Think Evaluation for Problem 10: The setup defines the mode-k unfolding, observed-entry count q, Khatri–Rao product Z, MTTKRP B, kernel matrix K, and unknown matrix W.The dimensions and missing-entry representation establish the variables used in the linear system.
The Main Theorem
The paper generalizes slice-connectivity characterization to incomplete transfer systems. Its main theorem gives a sharp equivalence between O-slice membership and connectivity bounds on all geometric fixed points.
- The Main Theorem: The paper generalizes Hill and Yarnall’s characterization of slice connectivity to incomplete transfer systems.The result concerns the O-adapted slice filtration for finite-group equivariant spectra.
- The Main Theorem: The theorem provides a sharp equivalence between the O-slice filtration and geometric-fixed-point connectivity.This identifies the slice condition through a family of non-equivariant connectivity requirements.
- The Main Theorem: Theorem 6 states that a connective G-spectrum X belongs to the O-slice category Σ^O_{≥n} exactly when every geometric fixed point Φ^J(X) is ⌈n/∥J∥_O⌉-connective.The equivalence ranges over every subgroup J≤G.
- The Main Theorem: The proof begins by establishing a strict lower bound on fixed-point dimensions for O-admissible representations.This bound is the structural ingredient connecting admissible orbit data to geometric fixed-point connectivity.
Proof of Necessity
The necessity proof reduces the geometric fixed-point condition to generators and propagates it through exactness, wedges, extensions, and homotopy colimits. Representation dimensions yield the required ceiling bound for each subgroup.
- Proof of Necessity: It suffices to verify the connectivity condition on generators Y=G+∧_H S^V because Φ^J is exact and preserves wedges and homotopy colimits.The generators satisfy dim_R(V)≥n.
- Proof of Necessity: For each contributing double coset, the fixed representation is identified with V^{J′}, whose dimension is bounded below by n/∥J∥_O.Conjugation invariance gives ∥J′∥_O=∥J∥_O, and integrality yields the ceiling bound.
- Proof of Necessity: The resulting geometric fixed points lie in Sp_{≥⌈n/∥J∥_O⌉}, and closure under wedges, extensions, and homotopy colimits extends the bound to X.This completes the necessity direction of the theorem.
Proof of Sufficiency
The proof establishes sufficiency by applying isotropy separation and strong induction to control both terms of the cofiber sequence, then handling geometric fixed points through localization.
- The proof uses the isotropy separation cofiber sequence for a G-spectrum satisfying fixed-point bounds for every subgroup J≤G.
- Closure under homotopy colimits, cofibers, extensions, and suspensions propagates the required connectivity through the constructions.
- Step 1: The term E_P+ ∧ X: Step 1 filters E_P+ by cells induced from proper subgroups, reducing the claim to connectivity of induced spectra built from restricted fixed-point data.
- Step 2: The term Ẽ_P ∧ X: Step 2 identifies the localized term with inflation of geometric G-fixed points and reduces it to suspended spheres generated from Φ^G X.
- The representation V=kℝ[G/G_O] satisfies proper-subgroup fixed-point bounds, while dim(V^G)=k, completing the inductive connectivity argument after localization.
Proof of Property 3: Sufficiency
The sufficiency proof factors each flattening through four cofactor terms, forcing rank at most 4 and hence the vanishing of all 5×5 minors.
- The assumed factorization λ_αβγδ=u_αv_βw_γx_δ can be absorbed globally through determinant multilinearity without changing X on excluded monochromatic configurations.
- Laplace expansion along the leading row of the first flattening extracts four scalar cofactor terms.
- Because the cofactors depend only on the column configuration and not the localized row index, M(1) factors through dimensions 3n×4 and 4×27n^3.
- Symmetric parity across the exterior maps gives rank(M(m))≤4 for every flattening m∈{1,2,3,4}, verifying F(X)=0.
Proof of Property 3: Necessity
The necessity argument starts from F(X)=0 and uses universal vanishing of the 5×5 minors to bound every principal flattening's rank by 4.
- rank(M(m))≤4 across all four principal flattenings follows from the universal vanishing of their 5×5 minors.
A Comparative Algorithmic Analysis
The paper compares two matrix-free PCG solvers for an RKHS-constrained CP tensor-decomposition subproblem, focusing on how they exploit Kronecker structure while differing in geometry, preconditioning, and Krylov-loop tracking.
- The study compares two highly optimized, matrix-free PCG solvers for the same unaligned, RKHS-constrained mode-k subproblem.
- Both methods exploit Kronecker algebra but differ in their treatment of unaligned geometry, preconditioner design, and variable tracking inside the Krylov loop.
- The RKHS factor matrix is A_k=KW, with K a symmetric positive semi-definite kernel matrix and W the unknown weight matrix.
- Directly assembling H requires O(qn^2r^2) memory, while dense solvers require O(n^3r^3) time.
- Explicit vectors of size N and the Khatri–Rao product introduce prohibitive O(N) and O(M) complexities.
- The proposed iterative PCG solvers act directly on the matrix representation W∈ℝ^n×r rather than explicitly forming the prohibitive ambient objects.
2. Comparative Analysis of the Two Approaches
Approach 1 pre-aggregates data geometry and uses row-wise Block-Jacobi preconditioning, while Approach 2 accumulates observations on the fly and uses kernel-based preconditioning. Their trade-offs span iteration cost, setup cost, numerical stability, and scalability.
- Computational cost: Approach 1 costs O(n^2r+nr^2) per iteration, removing q from the PCG loop, whereas Approach 2 costs O(n^2r+qr).Approach 2 therefore processes all q observations at every iteration.
- Computational cost: Approach 1 requires heavier setup, including O(n^2r^2) block construction and O(nr^3) factorization, while Approach 2 has effectively zero setup time.The approaches shift computational work between setup and iterations.
- Numerical strategy: Approach 1 uses standard PCG with two dense K multiplications per iteration, while Approach 2 uses inverse-free tracking to reduce this bottleneck to one dense kernel multiplication.Approach 2 tracks pseudo-residuals so the K^-1 inversion cancels algebraically, but accumulated floating-point drift requires periodic refreshes.
- Practical trade-offs: Approach 1 is presented as practically superior for large-scale datasets, whereas Approach 2 is better suited to lightweight setups or huge ranks.The stated comparison links Approach 1’s q-independent iterations and robust Block-Jacobi preconditioner to large-scale use.
3. Approach 1: Pre-Aggregated Geometry & Block-Jacobi Preconditioner
Approach 1 avoids explicit ambient-dimensional tensor operations by precomputing sparse Khatri-Rao rows and slice-specific geometry matrices, then applies an exact Hessian operator and block preconditioner efficiently within PCG.
- Geometry construction: Each observed Khatri-Rao row is computed in O(dr), and all q rows are precomputed in O(qdr) without forming the full unfolded tensor.This construction bypasses the ambient dimension M.
- Geometry construction: The method captures unaligned data geometry through n independent symmetric matrices E(i), each corresponding to one mode-k slice.Observations are grouped by the mode-k slice index.
- Operator application: The implicit Hessian action maps W to V using U=KW and row-wise products Y_i,:=U_i,:E(i), in O(n^2r+nr^2) time independent of q, M, and N.Sparse masking and slice-wise accumulation avoid explicit full-grid computations.
- Preconditioning: Exact diagonal Hessian blocks are positive semidefinite and become symmetric positive definite for λ>0, enabling Cholesky-like factorizations for the Block-Jacobi preconditioner.The blocks are constructed through flat dense matrix multiplication.
- Algorithm: Algorithm 1 initializes the right-hand side and PCG state, repeatedly applies the kernel and slice matrices, updates the iterates, and stops when the Frobenius residual falls below τ.The listed procedure includes block-factor construction before the PCG loop.
4. Approach 2: On-the-fly Sparse Accumulation & Kernel Preconditioner
Approach 2 reformulates the system with a kernel preconditioner and avoids explicit kernel inversion through inverse-free residual tracking. It preserves sparse observation processing but retains q-dependent work in each iteration.
- System reformulation: The system is factored with P=I_r⊗K, yielding a reduced operator that separates the kernel component from the sparse observation geometry.The reformulation uses Kronecker-product identities to rewrite the exact system.
- Kernel preconditioning: Preconditioning with P bounds the effective operator’s condition number regardless of the kernel spectrum, addressing ill-conditioning from decaying RKHS eigenvalues.The preconditioned operator is P^1/2 H_red P^1/2+λI_nr.
- Inverse-free tracking: Inverse-free tracking replaces repeated z_k=P^-1r_k computations by analytically updating factored residuals, so the P^-1 inversion cancels algebraically.The right-hand side and operator remain in the range of P, enabling the factorization by induction.
- Sparse accumulation: The sparse operator applies selection to q observed entries, computes their predicted scalars, and adjoint-accumulates contributions into the output rows.For each observation, the predicted value is formed from the corresponding row and Khatri-Rao vector.
- Algorithm: The algorithm initializes B from observed tensor values, updates W, Z, D, and tracked kernel states, and explicitly refreshes tracked products every 50 iterations to control drift.The refresh recomputes KZ_k and KD_k.