Markdown edition

# OpenAI releases math and ETH proof files, withholds physics artifacts

> OpenAI published math and ETH proof files; physics artifacts remain withheld during expert review.

By BIGCHANGE.AI Editorial

Published: 2026-10-27T11:57:43.094Z
Updated: 2026-10-27T11:57:43.094Z
Canonical: https://bigchange.ai/blog/openai-math-eth-physics-proof-release-review

![Two open shelves hold blank volumes beside a closed cabinet door.](https://bigchange.ai/api/media/file/openai-research-artifact-access-hero-v2.png)
AI-generated conceptual illustration by BIG CHANGE.

OpenAI announced three model-generated research claims on October 26. Its [release](https://openai.com/index/building-scientific-understanding-with-academic-communities/) puts mathematics and computer science papers and Lean files in public view. The physics output remains withheld.

## The big change

- **What changed:** OpenAI uses three release arrangements for its research claims.
- **Why it matters:** A public proof file exposes an exact statement for inspection. A withheld argument leaves outsiders with the company's account.
- **What to watch:** The ETH organizers have invited an open examination and say their involvement is no certification. They are asking researchers to examine the argument, explain its limits and make corrections visible.

## Three research claims

The [October 25 local smoothing manuscript](https://github.com/openai/math/blob/main/preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026/paper.pdf) states a bound for waves averaged over time, across spatial dimensions, and develops claimed consequences for Fourier analysis and Kakeya sets. Its accompanying [Lean scope note](https://github.com/openai/math/blob/main/lean/docs/079.md) points to formal statements. There is no named math review group.

For computer science, OpenAI claims a refutation of the Exponential Time Hypothesis, or ETH. ETH posits exponential worst-case time for 3-SAT. The [released paper](https://github.com/openai/math/blob/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf) proposes a deterministic method that exactly counts satisfying assignments of fixed-width formulas in subexponential time using polynomial space. The [Lean scope note](https://github.com/openai/math/blob/main/lean/docs/378.md) describes a formalized bound for a canonically encoded formula; it separately identifies a sharper bound in the manuscript. We did not run the proof checker or audit the mathematics.

Russell Impagliazzo and Ramamohan Paturi of UC San Diego and Ryan Williams of MIT will organize examination of the ETH claim. In their [letter to the theoretical computer science community](https://docs.google.com/document/d/1adB0IhJgLzsmbfCgoLrtoJTjnlPf74UnyjMo35P5JHo/edit), they say their participation should not be taken as certification. They invite researchers to reconstruct the argument, surface gaps or corrections and explain its consequences. The letter also calls for independent criticism without giving the selected group ownership of the effort.

The unreleased physics work concerns quantum chromodynamics and pure Yang–Mills existence, OpenAI says. A group led by David Gross is writing up the work. OpenAI names Michael Douglas, Arthur Jaffe, Igor Klebanov and Nikita Nekrasov as members. No physics manuscript accompanied the announcement.

## What public proof files let others check

The local smoothing [formalization note](https://github.com/openai/math/blob/main/lean/docs/079.md) names the wave estimate and points to separate comparator statements for its Kakeya and restriction consequences. The ETH [comparator challenge](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/SubexponentialSAT.lean) exposes definitions for formulas, their encoding and a machine, followed by the statement intended for checking. The `sorry` placeholder in that challenge is the hole a separate solution is meant to fill; its presence in the challenge alone says nothing about whether OpenAI's solution checks.

[Lean's own reference](https://lean-lang.org/doc/reference/latest/ValidatingProofs/) explains how a checker can ask whether a submitted proof establishes the specified statement under its declared dependencies. A specialist must also decide whether those definitions and that statement faithfully capture the original research question, whether the manuscript's broader consequences follow, and whether an argument can be understood and used. We did not independently establish either theorem.

The ETH paper says its subexponential bound does not automatically transfer through general polynomial-time reductions to all NP problems. The proposed result would not resolve P versus NP or promise practical speedups elsewhere. The organizers' letter likewise treats the consequences for algorithms and existing work as questions to examine, while observing that earlier techniques and reductions retain value regardless of how interpretations change.

## The physics limit

The Yang–Mills existence claim addresses part of [Clay's prize problem](https://www.claymath.org/millennium/yang-mills-the-maths-gap/). Clay's problem also asks for a mass gap. OpenAI makes no mass-gap or prize-resolution claim.

The ETH organizers note in their letter that early access can help checking, but it can also affect who has the first chance to publish or build on a result.

Our earlier [analysis of private AI discoveries](https://bigchange.ai/blog/private-ai-discoveries-public-science) discussed access and control in general.

## Sources

- [OpenAI, Working with academic communities to build scientific understanding, October 26, 2026](https://openai.com/index/building-scientific-understanding-with-academic-communities/) — Company account of three claims and release arrangements, without independent certification.
- [OpenAI, Local smoothing for the Euclidean wave equation, October 25, 2026](https://github.com/openai/math/blob/main/preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026/paper.pdf) — Public manuscript states the claimed wave estimate and consequences; the proof was not independently audited here.
- [OpenAI, local smoothing Lean scope note](https://github.com/openai/math/blob/main/lean/docs/079.md) — Lists the formalized scope and links comparator statements; no proof execution by BIG CHANGE.
- [OpenAI, The Exponential Time Hypothesis is False, revised October 25, 2026](https://github.com/openai/math/blob/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf) — Public manuscript claims exact counting in subexponential time and explicitly limits transfer to general NP problems.
- [OpenAI, ETH Lean scope note and comparator challenge](https://github.com/openai/math/blob/main/lean/docs/378.md) — The formalization note describes its bound separately from the manuscript's sharper bound; inspect the linked challenge and dependencies before judging the claim.
- [Impagliazzo, Paturi and Williams, Message to the TCS Community on ETH](https://docs.google.com/document/d/1adB0IhJgLzsmbfCgoLrtoJTjnlPf74UnyjMo35P5JHo/edit) — The organizers invite independent examination and expressly say their participation does not certify OpenAI's claim.
- [Lean Language Reference, Validating a Lean Proof](https://lean-lang.org/doc/reference/latest/ValidatingProofs/) — Explains proof checking, dependency audits and the separate question of whether a statement expresses the intended theorem.
- [Clay Mathematics Institute, Yang–Mills and the mass gap](https://www.claymath.org/millennium/yang-mills-the-maths-gap/) — Official problem description includes a mass gap; OpenAI's narrower existence claim is not a prize resolution.