Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

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.

Aletheia tackles FirstProof autonomously

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.
Paper Structure (17 sections, 4 theorems, 67 equations, 1 figure, 3 tables)

This paper contains 17 sections, 4 theorems, 67 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Interpretation of the challenge
  3. Methodology and results
  4. Aletheia (Best of 2)
  5. Evaluations
  6. Further comparisons
  7. Acknowledgments
  8. Verification and Extraction Prompt
  9. Pre-deadline evaluations
  10. Raw prompts and outputs
  11. Problem 2
  12. Problem 5
  13. Problem 7
  14. Problem 8
  15. Problem 9
  16. ...and 2 more sections

Key Result

Theorem 1

Let $\Pi$ be a generic irreducible admissible representation of $\mathrm{GL}_{n+1}(F)$. There exists $W \in \mathcal{W}(\Pi, \psi^{-1})$ such that for any generic irreducible admissible representation $\pi$ of $\mathrm{GL}_n(F)$ with conductor ideal $\mathfrak{q}$, and any generator $Q \in F^\times$ is finite and nonzero for all $s\in\mathbb C$, where $u_Q = I_{n+1} + Q\,E_{n,n+1}$.

Figures (1)

  • Figure 1: Plot of the inference cost per FirstProof, as a multiple of the inference cost of the solution to Erdős-1051 from feng2026semiautonomousmathematicsdiscoverygemini.

Theorems & Definitions (18)

  • Theorem 1
  • proof
  • Remark C.1
  • Definition 2: Balchin, Barnes, and Roitzheim BBR2021
  • Definition 3
  • Definition 4
  • Definition 5
  • Theorem 6
  • Lemma 1
  • proof
  • ...and 8 more