Aletheia tackles FirstProof autonomously

Tony Feng; Junehyuk Jung; Sang-hyun Kim; Carlo Pagano; Sergei Gukov; Chiang-Chiang Tsai; David Woodruff; Adel Javanmard

cs.AIFeb 24, 2026

Aletheia tackles FirstProof autonomously

Authors: Tony Feng, Junehyuk Jung, Sang-hyun Kim, Carlo Pagano, Sergei Gukov, Chiang-Chiang Tsai, David Woodruff, Adel Javanmard,

Organizations: Google DeepMind · UC Berkeley · Brown University · Korea Institute for Advanced Study ·

Abstract

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.

Figures & tables

	Aletheia (best of 2)	Expert Evaluation (correct/total)
P1	No Output
P2	Correct	4/4
P3	No Output
P4	No Output
P5	Correct	4/4
P6	No Output

Table 1: Summary of Aletheia ’s performance on FirstProof . The Expert Evaluation column displays the number of experts who rated the solution as being Correct, out of the total number of experts consulted. Only the assessment on P8 was not unanimous.

	Aletheia A	Aletheia B	Zulip
P1	No output	No output
P2	Correct	Correct	Link
P3	No output	No output
P4	No output	No output
P5	Correct	Misinterpreted	Link
P6	No output	No output

Table 2: Our current ( post-deadline ) estimation of the results based on the consensus of expert assessments. On P8, the expert assessment was not unanimous. We include links with public comments (on Zulip) for individual problems.

Figure 1: Plot of the inference cost per FirstProof problem, as a multiple of the inference cost of the solution to Erdős-1051 from ( Feng et al., 2026a ) .

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Deprecated (pre-deadline) evaluations
	Aletheia A	Aletheia Af	Aletheia B
P1	N/A	N/A	N/A
P2	Correct	Correct	?
P3	N/A	N/A	Filtered out
P4	N/A	N/A	N/A
P5	Correct	N/A	?

Appendix

Table 3: Our pre-deadline estimation of the results, as sent to the FirstProof authors at 11:07pm PST on February 13. Correct = our first choice solution. Incorrect = we are confident it is incorrect. Filtered out = filtered by the additional verification and extraction prompt. ? = ran for ablation purposes on Friday evening; not read before the deadline. Aletheia A is Aletheia with Gemini 3 Deep Think as base model. Aletheia Af is an extended generation variant of Aletheia A. Aletheia B is Aletheia with base model B, from §2 of ( Feng et al., 2026b ) . ‘N/A’ indicates either Aletheia returned “No solution found” or failed to return a solution within the time limit.

LLM Mathematical Reasoning

Large language model mathematical reasoning studies how AI systems solve, explain, verify, and generalize across mathematical problems and proofs.

See all 270 papers

RMA: Context-Orchestrated Research Math Agents
May 20, 2026Zelin Zhao, Bo Yuan, Yuchen Zhu +2LLM Context Management LLM Mathematical Reasoning
Georgia Institute of Technology
Advancing Mathematics Research with AI-Driven Formal Proof Search
May 21, 2026George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18Large Language Model-Guided Theorem Proving Automated Theorem Proving
1Google DeepMind1 · 2Aarhus University · 3Google
ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
Jul 10, 2026Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck +4LLM Agents Multi-Agent LLMs
ETH Zurich · Aarhus University · Independent Researcher +1

May 20, 2026J/K move · Enter open · S save

RMA: Context-Orchestrated Research Math Agents

Zelin Zhao, Bo Yuan, Yuchen Zhu, Jaemoo Choi+1

Georgia Institute of Technology

LLM Context Management LLM Mathematical Reasoning Autonomous Research Agents Memory-Augmented Language Model Agents

Open paper AskPDF arXiv

Long-horizon mathematical reasoning fails less often because a model cannot produce a valid next step than because an agent fails to maintain and expose the right semantic state across many iterations. Left unmanaged, this produces research-level proofs that are locally convincing yet globally incomplete: a key lemma unproved, an assumption unchecked, a citation unsupported, or a computational claim unverified. We present Research Math Agents (RMA), an agentic framework for long-horizon proof development built around a persistent, typed research store and an orchestrator that compiles operation-specific context from that store. The Research Context Orchestrator is the central state-management layer between the persistent research store and each locally scoped proof operation: it retrieves task-relevant artifacts, compiles them into a bounded context, invokes the appropriate operation, and writes the resulting proof edits, issue updates, literature notes, plans, or evaluations back to the store. This process is designed to keep proof revisions, unresolved issues, prior attempts, literature, and evaluations available across rounds while exposing only task-relevant state to each local operation. We evaluate RMA across complementary research-level settings using independent expert evaluation, blind mathematician review, LLM-based benchmark evaluation, and Lean 4 kernel verification. RMA achieves a 42.5% solve rate on the independently evaluated SOOHAK Challenge Hard set, obtains 8 of 10 correct solutions on First Proof B1 and 8 of 10 passing solutions on B2 under human-expert evaluation, and verifies 213 of 300 sampled Research Solved targets in Formal Conjectures with the Lean 4 kernel.

Abstract

LLM Mathematical Reasoning

Explore similar work

RMA: Context-Orchestrated Research Math Agents

Advancing Mathematics Research with AI-Driven Formal Proof Search

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems