OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Covers the entire closed regular tetrahedron by finitely many cylinders with compact triangular perpendicular bases whose total area is less than half its smallest orthogonal projection area. This disproves Bang’s half-area cylinder-covering bound and the stronger directionwise normalized conjecture in dimension three. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
Both independent assessments find that the Lean statements express or imply the whole result described above.Read the assessments
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
The tetrahedron (1.4) has A_{\min}(K)=\sqrt2. For every 0<\eps\le1/2000, it admits a covering by m=2\lceil2/\eps^2\rceil cylinders with compact triangular perpendicular bases such that
for a continuous real function \lambda. For any finite partition \alpha=t_0<t_1<\cdots<t_N=\beta, put I_i=[t_{i-1},t_i] and choose arbitrary tags c_i\in I_i. There are N cylinders covering \mathcal S, with axes parallel to e+w(c_i) and nondegenerate compact triangular perpendicular bases. These covers can be chosen so that their total base area tends to \mathcal A as the mesh \delta=\max_i|I_i| tends to zero, uniformly over the partitions and tags.
Alternatively, take each base to be the perpendicular projection of the actual compact sweep with t\in I_i, in the same frozen direction e+w(c_i). These N cylinders cover \mathcal S, and their total base area also tends to \mathcal A, uniformly over the partitions and tags.
The release does not say which paper theorem its catalogue describes. The statements above share the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.
Six more possible matches
Corollary 1.2in Finite angular cylinder covers below the half-area bound, 27 September 2026.
Theorem 1.2(Finite approximation by square tiles)in Finite cylinder approximation of ruled sets, 27 September 2026.
Theorem 1.1in Slope-field perturbations of the two-cylinder covering, 27 September 2026.
Corollary 1.2in Finite triangular approximation of radial sweeps, 27 September 2026.
Proposition 1.1(Perpendicular base area)in Finite cylinder approximation of ruled sets, 27 September 2026.
Corollary 1.2in Slope-field perturbations of the two-cylinder covering, 27 September 2026.
Reported proof verification
Three Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
A regular tetrahedron admits a finite cylinder covering with compact triangular perpendicular bases whose total area is less than half its minimum orthogonal projection area. This disproves the half-area cylinder-covering conjecture. By affine invariance, the same construction gives a counterexample to the directionwise normalized half-bound for every nondegenerate tetrahedron.
We approximate compact ruled families of segments by finitely many cylinders with square intercept tiles and perpendicular-base area at most their integral projection cost plus any positive error. The velocity field is C1, and its differential has opposite real eigenvalues whose magnitudes are strictly below the inverse segment half-length; both eigenvalues may vanish. The result includes square-zero differentials with unrestricted shear and fields that pass between the two regimes. It holds for arbitrary compact label sets.
The two-cylinder covering of a regular tetrahedron can be perturbed to give finite covers with total perpendicular base area strictly below half its minimum projection area. These covers give negative answers to both the half-area question and the directionwise normalized half-bound conjecture. By affine invariance, the directionwise conclusion holds for every nondegenerate tetrahedron.
We prove that radially aligned segment sweeps admit finite cylinder covers with one triangular base for each interval of any tagged partition. As the mesh tends to zero, the total perpendicular base area converges to a weighted parameter area. An explicit application covers every regular tetrahedron with total base area below half its minimum projection area, giving negative answers to the half-area question and the directionwise normalized 1-Codimensional Cylinder Covering Conjecture.
Three Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
CylinderCovering
The paper states
It is paired with Theorem 1.1 and Corollary 1.2, each shown below.
for a continuous real function \lambda. For any finite partition \alpha=t_0<t_1<\cdots<t_N=\beta, put I_i=[t_{i-1},t_i] and choose arbitrary tags c_i\in I_i. There are N cylinders covering \mathcal S, with axes parallel to e+w(c_i) and nondegenerate compact triangular perpendicular bases. These covers can be chosen so that their total base area tends to \mathcal A as the mesh \delta=\max_i|I_i| tends to zero, uniformly over the partitions and tags.
Alternatively, take each base to be the perpendicular projection of the actual compact sweep with t\in I_i, in the same frozen direction e+w(c_i). These N cylinders cover \mathcal S, and their total base area also tends to \mathcal A, uniformly over the partitions and tags.
Every regular tetrahedron K\subset\R^3 of positive edge length has a finite cylinder cover B_i+\R u_i, with unit axes u_i and nondegenerate compact triangular bases B_i\subset u_i^\perp, such that
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
The tetrahedron (1.4) has A_{\min}(K)=\sqrt2. For every 0<\eps\le1/2000, it admits a covering by m=2\lceil2/\eps^2\rceil cylinders with compact triangular perpendicular bases such that
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).
Their note:None for the headline; the aggregate file additionally states ruled-set and radial-sweep approximation results.
Definitions the group asks readers to compare with the paper:CylinderCovering.lean contains ten run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {} lines (environment-resetting metaprogramming inside a challenge file; a memory/performance hack that does not change statements)
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
The half-area cylinder-covering conjecture predicts that a cylinder cover of a convex body has total perpendicular-base area at least half its smallest projection area. The formalization constructs finite covers of a regular tetrahedron by cylinders with compact triangular bases whose total area is strictly below that bound. For the explicit small parameter $\varepsilon$, the normalized area is $1/2-(13/6000)\varepsilon^2+O(\varepsilon^4)$, giving the strict saving.
It also gives a counterexample to the directionwise normalized half-bound. The broader Comparator file includes the companion ruled-set and radial-sweep approximation results.
The formalization approximates compact ruled families of line segments by finite cylinder covers with perpendicular-base area at most the integral projection cost plus any prescribed positive error. The selected results cover the stated $C^1$ hyperbolic differential condition, square-zero and nilpotent cases, physical rescalings, logarithmic and product-cell estimates, and singular cases. Compact label sets need not have regular boundary.
The differential and segment-length hypotheses remain part of each result. The aggregate Comparator file also contains the companion tetrahedron counterexamples and radial-sweep estimates.
The formalization proves that every regular tetrahedron has a finite cylinder cover whose total perpendicular-base area is strictly less than half its minimum projection area. It supplies covers with parallelogram bases and also proves the directionwise normalized cost is below one half. These are counterexamples to the two cylinder-covering bounds studied in the paper.
The linked aggregate includes the accompanying explicit angular covers and finite approximation theorems for ruled sets and radial sweeps. The affine extension of the directionwise conclusion to every nondegenerate tetrahedron is outside the selected regular-tetrahedron statements.
The formalization proves finite triangular-cylinder approximation for radially aligned segment sweeps. For every tagged partition of the parameter interval, it constructs one cylinder per interval with the prescribed radial direction, and the total perpendicular-base area converges to the weighted parameter area as the mesh tends to zero. It also covers the corresponding actual swept set under the stated geometric hypotheses.
The same aggregate includes finite cylinder covers of regular tetrahedra below half the minimum projection area. These are the radial approximation and covering consequences relevant to the paper.
AI-drafted comparisons, with no recorded human review
Cylinder-covering counterexamples and companion approximationsCylinderCovering
Unreviewed AI draft: states a paper’s theorem as the paper does. The aggregate file states the main theorems of all four accompanying papers: the explicit angular cover of the tetrahedron with ε ≤ 1/2000 and remainder at most 2ε⁴, the ruled-set approximation, the regular-tetrahedron counterexamples and the radial-sweep approximation. The extension to every nondegenerate tetrahedron is outside it.
Finite cylinder approximation for the selected ruled familiesRuledCovering
Unreviewed AI draft: states a paper’s theorem as the paper does. States the ruled-set paper’s approximation theorem: compact ruled families of segments are approximated by finite cylinder covers with base area at most the projection cost plus any error, under the stated differential and segment-length hypotheses.
Unreviewed AI draft: states a weaker form of a paper’s theorem. States the main theorem’s explicit cover with an unspecified range of ε and an unspecified constant in the ε⁴ remainder, where the paper states ε ≤ 1/2000 and a remainder of at most 2ε⁴; the strict saving below half the minimum projection area is included. The aggregate CylinderCovering states the explicit version.
Who ran the proof-verification program?
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
Cylinder-covering counterexamples and companion approximationsCylinderCovering
Two reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“CERTIFIED”
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Other people’s accounts of running proof-verification software, with links to their reports.
Pico, openai-math-counterexamples: do the counterexamples in openai/math hold when someone else computes them?, 9 October 2026. Source
The 16,000,000-cylinder construction at eps 1/2000 gives the stated area sum to within 8.4e-15, with exact coverage on 21,072 sample points and a control that finds gaps without the enlargement.
Other proofs and exact calculations
These reports examine claims in the papers using exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.
“REFUSED” The exact code did not decide it; cert-machine records this as refused, which is no evidence against the claim.
What it covers
“a finite component: A_min(K) = sqrt 2, the construction’s parameters, every polynomial identity of the coverage proof, and the exact total base area at eps = 1/2000 and tau = 1/4000 (strictly below A_min/2, inside the printed remainder bounds); COVERAGE -- the decisive geometric part -- is REFUSED (a continuum covered by 1.6e7 cylinders; ~3.2e13 sector pairs), so the row is REFUSED”
What these papers cite in the release, and what cites them
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Papers elsewhere in the release that this family’s papers cite
This family’s papers cite no paper elsewhere in the release.
Papers elsewhere in the release that cite this family’s papers
No paper elsewhere in the release cites this family’s papers.
Follow-up work by others
acprk, Remarks on proofs in OpenAI’s mathematics repository, 10 October 2026. Source
The half-area cylinder counterexample with 640 cylinders instead of 16,000,000.
References outside the release
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Explain a result, compare statements or propose a correction
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a counterexample and rates its significance, if it holds up, as “Solid publication, could lead to tenure”. The page says that nothing on it is verified.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The Lean statement treats one regime at a time and leaves the regular tetrahedron statement outside the checked theorem.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The Lean statement treats one regime at a time, so it is weaker than the paper’s theorem for fields that mix the two regimes.
Questions awaiting review
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Identify the theorem the catalogue describes
Family 100No single paper statement clearly matches OpenAI’s description by wording, and no review identifying the intended theorem is recorded.Open the form
Address a question raised in an independent assessment
Atlas records no review confirming that the two statements mean the same thing.
Independent assessment
MathVet
Their term
“full”
What their term means
The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state the headline as OpenAI wrote it.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 471 s; peak memory 6.4 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 272 s; peak memory 6.3 GiB).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
Exact calculations for finite claims, cert-machine
Their verdict
“REFUSED”
Claim tested or proved
The exact code did not decide it; cert-machine records this as refused, which is no evidence against the claim.
What it covers
“a finite component: A_min(K) = sqrt 2, the construction’s parameters, every polynomial identity of the coverage proof, and the exact total base area at eps = 1/2000 and tau = 1/4000 (strictly below A_min/2, inside the printed remainder bounds); COVERAGE -- the decisive geometric part -- is REFUSED (a continuum covered by 1.6e7 cylinders; ~3.2e13 sector pairs), so the row is REFUSED”
Exact calculations for finite claims, cert-machine
Their verdict
“NEEDS DATA”
Claim tested or proved
Cannot be decided from the release: the specific object the argument relies on is not published.
Detail
NOT PUBLISHED as a specific instance; construction in preprints/Slope-field-perturbations-of-the-two-cylinder-covering-September-27-2026/build/sections/threshold.tex and dictionary.tex with non-explicit smallness thresholds.
Exact calculations for finite claims, cert-machine
Their verdict
“NEEDS DATA”
Claim tested or proved
Cannot be decided from the release: the specific object the argument relies on is not published.
Detail
NOT PUBLISHED as a specific instance; preprints/Finite-triangular-approximation-of-radial-sweeps-September-27-2026/build/beams.tex l.292 (‘For every zeta > 0, the tetrahedron K has a finite cylinder cover ...’), coordinates.tex.
Finite cylinder approximation for the selected ruled families
Role
the release lists it as a supporting statement
Paired with
No paper theorem is paired with this Lean statement.
Who ran the proof-verification program
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Explicit triangular-cylinder cover below half area
Role
the release lists it as a supporting statement
Paired with
Theorem 1.1 (candidate pairing)
Who ran the proof-verification program
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.