Technical Summary: First Proof Second Batch

Overview

This document presents the results of the "First Proof Second Batch," a formal benchmark designed to evaluate the capabilities of current AI systems in solving research-level mathematics problems. Unlike the preceding "First Batch," which served as an informal community experiment, this second iteration was a controlled, transparent study conducted between March and June 2026. The project aimed to provide accurate, empirical data on the ability of AI systems to generate rigorous proofs for problems arising naturally in human mathematical research, where the proofs were known to the contributors but had not yet been published or appeared on the internet.

Methodology

Problem Selection and Design

Ten problems were selected from a diverse range of mathematical fields, including computability theory, discrete geometry, stochastic PDEs, lattice theory, and von Neumann algebras. The selection criteria prioritized:

• Novelty: Problems requiring non-standard insights rather than standard textbook applications.
• Constraint: Proofs known to the contributors were limited to 8 pages and had not been publicly disclosed.
• Pre-screening: Preliminary tests were conducted in April 2026 using various models (ChatGPT 5.4/5.5, Gemini 3.1, Opus 4.7) with zero data retention. Two problems were discarded because they could be solved by reducing to existing literature or were quickly derivable from LLM-searched references.

Testing Protocol

The testing phase (May 28 – June 1, 2026) involved four distinct AI systems:

1. System A (IMProofBench ProofCouncil): A harness developed by ETH Zürich and Aarhus University, primarily using gpt-5.5-pro as a base model.
2. System B (UCLA Moonshot Harness): A harness developed by the University of California, Los Angeles, using gpt-5.5-pro.
3. System C (OpenAI ChatGPT 5.5 Pro): The base model itself, tested with "xhigh" reasoning settings.
4. System D (Princeton Momus): A harness developed by Princeton University using gemini-3.1-pro-preview.

All systems were required to run as reproducible pipelines on First Proof's AWS infrastructure. They received the ten problems as .tex source files and were tasked with generating complete, compilable LaTeX proofs within 24 hours without further human interaction. The systems were restricted to calling publicly available models via API.

Grading Process

The evaluation (June 4–8, 2026) employed a double-blind journal review model. Thirty expert mathematicians, selected by the problem authors, served as referees. Each solution was assigned 2–3 referees and graded on a four-tier scale:

• Essentially Flawless: All disagreements are stylistic.
• Requires Minor Revisions: Contains a few correctable errors or citation issues.
• Requires Major Revisions: The strategy is potentially viable but requires significant human effort to repair.
• Rejected: The strategy is not salvageable or the solution is fundamentally incorrect.

Key Results

Across the four systems and ten problems, 39 solutions were generated (System A failed to produce a solution for Problem 6 due to a technical API timeout). The results were mixed, with 7 problems receiving at least one passing grade (Essentially Flawless or Minor Revisions).

Successes and Novelty

• Problem 5 (Stochastic PDE): System A produced a solution rated Essentially Flawless. Notably, this solution used a novel approach involving the stochastic sewing lemma and a different drift estimate than the human solution, impressing referees with its correctness and originality.
• Problem 6 (Lattice Theory): Systems B and C both produced solutions rated Essentially Flawless. These solutions followed the general strategy of the human proof but were noted for being mathematically complete, though sometimes lacking in conceptual motivation or "stream of consciousness" in their exposition.
• Problem 7 (Combinatorial Topology): Systems A and C produced Essentially Flawless solutions by correctly identifying a counterexample (showing the CW complex is not contractible), with System A's approach closely mirroring human topological intuition.
• Problem 2 (Discrete Geometry): Three systems (A, B, C) received Minor Revisions. They successfully solved the problem by translating a proof from a previously published paper by the problem author (Richard Schwartz) into the specific category of maps requested. However, they were heavily criticized for failing to cite the source paper, reusing terminology and labels verbatim without attribution.

Failures and Limitations

• Problem 4 (Metric Geometry): All four systems received Rejections. The systems failed to make substantial progress, with some hallucinating theorems from the literature or stating false inequalities.
• Problem 3 (Discrete Probability): Systems B, C, and D were Rejected for relying on false lemmas, hallucinated citations, or failing to make the crucial connection to the Manickam–Miklós–Singhi (MMS) conjecture. System A received Minor Revisions for a correct but incomplete argument that missed the MMS connection.
• Citation and Attribution Issues: A recurring theme in the referee reports was the failure of AI systems to properly cite existing literature. In several cases (e.g., Problems 2, 3, and 9), solutions reproduced arguments or terminology from human papers without citation, which referees noted would constitute plagiarism in a human submission.
• Hallucination: Systems frequently cited non-existent theorems or papers (e.g., Problem 4, Problem 8) or attributed results to authors who did not prove them.

Costs

The financial cost of generating solutions varied significantly. System C (OpenAI's direct model) was the most cost-effective, with a total cost of approximately $117 for all problems. Systems A and B, which utilized complex harnesses and multiple model calls, incurred costs of roughly $3,186 and $4,799 respectively. System D cost approximately $1,014.

Significance and Claims

The paper positions this benchmark as a critical step in assessing the state of AI in mathematical research. Its primary claims and observations include:

1. Capability vs. Limitation: Current AI systems can solve research-level problems that are structurally similar to known results or where the proof strategy is routine. However, they struggle significantly with problems requiring deep, non-standard conceptual leaps or where the "trick" is not present in the training data.
2. The "Routine vs. Insight" Gap: AI systems excel at handling the meticulous, routine parts of an argument but frequently gloss over the most difficult, non-standard steps. They often assert that key claims follow from "standard arguments" without justification or cite papers that do not contain the claimed results.
3. The Role of Harnesses: Academic teams demonstrated that designing specific harnesses (code orchestration) can improve the mathematical quality of a base model's output. However, this improvement comes at a substantial financial cost compared to using the base model directly.
4. Transparency and Plagiarism: The study highlights a significant gap in AI behavior regarding academic integrity. Systems tend to reproduce phrasing and terminology from existing literature without attribution, a behavior that would be flagged as plagiarism in human research.
5. Novelty in AI: The project successfully identified instances where AI generated novel arguments (e.g., Problem 5) that differed from human solutions, suggesting that AI can occasionally contribute new perspectives, not just replicate existing knowledge.

The authors conclude that while AI systems are becoming powerful tools for mathematical research, they are not yet autonomous researchers capable of consistently producing publishable, rigorous proofs for open problems without significant human oversight, particularly regarding verification, citation, and conceptual framing. The paper serves as a baseline for future iterations (Batch 3) and a resource for the community to understand the current boundaries of AI in mathematics.