OpenAI vs Google DeepMind in Mathematics: Proofs, People and Compute

OpenAI has released 722 mathematical manuscripts grouped into 372 result families. Google DeepMind has published research on Aletheia, an agent that generates, critiques and revises mathematical arguments. Both releases give readers material to examine beyond benchmark headlines. They expose different parts of the work, and neither provides a matched experiment that establishes which lab is better at mathematical research.

Our assessment is that OpenAI’s release offers a substantial opportunity to inspect selected formal proof artifacts, while DeepMind’s Aletheia reports offer more detailed accounts of human participation and the filtering of unsuccessful candidates. Those are useful differences in disclosure. A reader assessing a particular theorem still needs evidence about that theorem.

For the catalogue and its major claims, see our examination of OpenAI’s 722-manuscript release. This follow-up compares verification, human involvement, reproducibility and compute accounting.

What the public evidence lets us compare

The sources for these distinctions are OpenAI’s release README, its formalization manifest, and DeepMind’s Aletheia report and FirstProof report. The differences below explain why each column needs qualifications.

OpenAI’s Lean artifacts create a specific verification opportunity

OpenAI’s formalization manifest describes its scope as “Partial progress.” and its review status as unchecked. Those fields describe the published metadata. They neither establish that the proofs are wrong nor supply an independent receipt showing that the collection passed verification. Formalization metadata.

Comparator provides a way to test a more precise proposition. Under its documented trust assumptions, a successful run establishes that the selected solution proves the challenge’s statement, uses only permitted axioms and is accepted by the Lean kernel. Its assumptions include trusted challenge dependencies and a correctly functioning checking environment. A file containing Lean code is an available artifact; a successful check is an observed outcome. Comparator’s verification contract.

Scope also matters. Family 017’s documentation selects the claim that π’s irrationality exponent is exactly two. The same page explicitly excludes the paper’s Flint–Hills series convergence consequence from that selected statement. A receipt for the selected target would therefore need to be described at that scope. Family 017 formalization scope.

For a journalist or researcher, the useful next step is to follow one claim from its manuscript to its formal statement, inspect the definitions and assumptions, and retain the output of a trusted check. This would establish something concrete about that target. It would leave separate questions about whether the formal statement captures the advertised mathematics and whether every claimed consequence follows.

DeepMind’s verifier is part of the research system

Aletheia’s Generator, Verifier and Reviser work through candidate solutions in natural language. The verifier can identify a flaw and trigger revision or another attempt. That architecture differs from accepting a formal proof through Lean’s kernel: the verifier is itself a reasoning system whose judgments need evaluation. Aletheia report, section 2.

The Erdős case study shows why the distinction matters. Aletheia attempted 700 problems and returned 212 potentially correct responses. Human assessment classified 200 candidates definitively, leaving 12 ambiguous. Of those 200, 137 were fundamentally flawed. Sixty-three were technically correct, but only 13 addressed the intended problem meaningfully; those 13 included results already present in the literature. This was a December 2025 deployment, not a measurement of Google’s latest model. Erdős case study, section 1.1.

That failure accounting is valuable. It shows the work that remains after the AI’s internal filter and distinguishes a valid argument from an answer to the intended question. It also makes clear why a list of successful examples cannot, by itself, quantify how much expert time a research system saves.

A later FirstProof study reports six of ten problems solved under majority expert assessment, using a best-of-two evaluation across two agent configurations. “Correct” meant publishable after minor revisions. Problem 8 received five positive assessments from seven experts. Each configuration had at least one false positive, and humans used expertise to designate preferred outputs. These details belong beside the six-of-ten headline. FirstProof report, sections 2–3.

Autonomous generation still has human decisions around it

An example with unusually clear attribution is Tony Feng’s eigenweights paper. Its AI-usage declaration attributes the core mathematical content to Aletheia. Feng describes his contribution, apart from developing the agent, as rewriting the output into paper form and adding the introduction. This documents a division of work between mathematical generation and exposition. Eigenweights paper, section 2.

Other projects involve substantive human mathematical contributions. DeepMind’s framework distinguishes autonomy from mathematical significance, and its FirstProof report separates autonomous production from subsequent human evaluation and selection. Those distinctions prevent a single label such as “AI-generated” from hiding several different research workflows. Autonomy framework; FirstProof methodology.

OpenAI identifies zeta zero-free-region work and Hodge work for CM abelian varieties as exceptions to its usual result-generation procedure. It also discloses human editing for readability of the alternate zeta write-up reaching the region Re(s) > 11/12. The README does not provide an equivalent interaction record for every manuscript. That limits what we can conclude about human involvement across the collection. OpenAI’s procedure disclosure.

To compare autonomy fairly, record who chose the problem, supplied mathematical hints, selected candidates, repaired arguments, checked references and wrote the final paper. Human involvement can improve a result. Disclosing it lets other researchers understand both the achievement and the workflow they might try to reproduce.

Inspecting a proof and reproducing its discovery are separate tasks

There are three practical levels of reproducibility here. Readers can inspect a published argument. They can attempt to execute a published proof-checking artifact. They can also try to reproduce the research process that generated the argument. Success at one level does not automatically supply the materials needed for the next.

For OpenAI’s formal artifacts, even building the library is a concrete part of the work. The Lean README recommends compiling small portions and documents a Linux memory-mapping issue that can affect whole-library builds. A reproducible checking report should preserve the source version, toolchain, dependencies, selected target, command and complete outcome. OpenAI’s build guidance.

DeepMind’s repository links prompts and responses for individual projects, including FirstProof. Its README also notes that two included outputs came from systems other than Aletheia. These records help readers compare what a model produced with what a human-authored paper retained. They need to be read with their attribution intact. Aletheia’s published output index.

OpenAI identifies its model as unreleased, while the Aletheia report describes orchestration around advanced Gemini models. The materials examined here do not establish a complete, equivalent public environment for rerunning either research pipeline. Our assessment is therefore that the releases support inspection more directly than independent reproduction of discovery. OpenAI model disclosure; Aletheia architecture.

The compute disclosures cannot support a price ranking

OpenAI’s announcement describes average compute per result as equivalent to roughly three hours of ChatGPT Pro thinking. It also announces ten reasoning summaries and says the company is working toward releasing the model. That compute equivalent gives readers a reference point, but the announcement provides no aggregate dollar bill, token ledger or accelerator-hour account. OpenAI’s October 6 announcement.

DeepMind’s FirstProof report plots candidate inference costs relative to an earlier solution of Erdős-1051. It explicitly cautions that the base models differ, so the comparison is not on equal footing. Those relative costs indicate variation in effort within the reported work. They do not provide an absolute dollar cost that we can compare with OpenAI’s compute equivalent. FirstProof inference-cost disclosure.

A fair cost comparison would require the same problems, a common acceptance standard, attempt limits, tool access and measured resource use. It should include failed attempts, formalization and checking costs, and human review. A cheap candidate that requires hours of specialist repair may have a higher total cost than an expensive candidate that survives scrutiny quickly.

Neither a subscription price nor a company’s relative compute chart supplies that accounting. We cannot infer which system produces accepted research more cheaply from these disclosures.

DeepMind’s earlier formal results need their own context

Google’s work includes a formal approach as well as Aletheia. In the 2024 IMO evaluation, AlphaProof and AlphaGeometry 2 jointly solved four of six problems for a silver-medal-standard score. Humans translated the problems into formal language, and some solutions took up to three days. These conditions matter when discussing the achievement. They also show why “DeepMind uses informal verification” would be too broad a claim. DeepMind’s IMO 2024 report.

Contest problems, research lemmas and proposed resolutions of long-standing conjectures are different evaluation populations. Their scores and counts should retain those labels. A historical formal-proof result helps explain a verification method; it does not serve as a matched baseline for OpenAI’s October 2026 research collection.

What would make the comparison more decisive?

Independent scrutiny is still central. The Advisory Group on Mathematics and Artificial Intelligence explicitly says its advisory role does not endorse OpenAI’s process or judge the impact of the results. Its responsible-release recommendations ask for model identities, prompts, reasoning summaries, time and estimated computation cost, along with formalization status and information about problem selection and failures. October 6 statement; responsible-release recommendations.

For an individual claim, the most useful evidence would connect an exact manuscript version to a precise theorem statement, a documented checking outcome, a specialist assessment of scope and novelty, and an account of the human and computational work. This would let readers distinguish a promising candidate from a checked formal target and from a result accepted into the research literature.

OpenAI’s artifacts make selected formal checks a useful next investigation. DeepMind’s records make its generation, selection and human review more inspectable in the reported projects. A capability winner would require a separate evaluation on shared problems. The next useful Kingy test is to select a small set of released formal targets, state the selection rule, run the documented checks and publish the outcomes at their exact scope.

Sources and reporting method

We examined OpenAI’s October 6 announcement and commit-pinned release documentation, its formalization metadata and family 017 scope note; Comparator’s checking contract; the cited versions of DeepMind’s Aletheia, Erdős, FirstProof and eigenweights reports; Google’s output index and historical IMO report; and AGMAI’s statements. Numerical outcomes are attributed to their authors. The comparison table summarizes disclosures, not independently measured performance. All mathematical correctness assessments in the studies remain attributed to the researchers and reviewers who made them.