The three-quarter exponent for honeycomb self-avoiding walk
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Proves the diameter form of Nienhuis’s predicted three-quarter exponent: a uniformly chosen n-step self-avoiding walk on the honeycomb lattice has diameter \(n^{3/4+o(1)}\). Its local mass and covering numbers have exponent 4/3. These estimates hold at every sufficiently large fixed length, simultaneously across scales, with arbitrarily high polynomial probability. (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.
The independent assessments find that the Lean statements express a supporting step or a different result.Read the assessments
What the papers state
Theorem 1.1(Diameter tails and the second length moment)
Every sum in this statement is finite. Here f(r)=r^{a+o(1)} means that for every \varepsilon>0,r^{a-\varepsilon}\le f(r)\le
r^{a+\varepsilon} for all sufficiently large r; the one-sided notation has the analogous meaning.
No Lean statement in the release is paired with this theorem.
Theorem 1.2(Sharp boundary mass and annealed chord laws)
For every sufficiently large fixed C, normalize \mu either on R\le\operatorname{diameter}\le CR, or on \operatorname{height}\ge R and \operatorname{diameter}\le CR. Under either law, \mathbb E\ell=R^{4/3+o(1)}.
3.
Let
D_R=\{y:e_i\cdot y<R,\ i=0,1,2\},\qquad
I_R=\{v\text{ a lattice vertex}:e_i\cdot v<(1-\varepsilon)R,
\ i=0,1,2\},
where R\in\frac12+\frac32\mathbb Z and \varepsilon>0 is sufficiently small and fixed. Sum critical chord weights over the ordered pair of boundary ports and normalize on chords visiting I_R. Uniformly for v\in I_R, their visit probability is R^{-2/3+o(1)}. The expected total number of visited vertices, and the expected number in I_R, are both R^{4/3+o(1)}.
No Lean statement in the release is paired with this theorem.
The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.
26 more possible matches
Theorem 1.1(Fixed-length mass and covering exponents)in Mass and covering exponents for fixed-length honeycomb walks, 26 September 2026.
Theorem 1.2(Finite boundary and polygon estimates)in Cylinder amplitudes and logarithmic bridge-length windows on the honeycomb lattice, 26 September 2026.
Theorem 1.3(Nesting and free boundary length)in Uniform marked-polygon estimates and sharp finite bridge moments, 26 September 2026.
Theorem 1.1(Macroscopic triangle chords)in Cap-selected amplitudes and triangle chords for honeycomb walks, 26 September 2026.
Corollary 1.2(Span in every lattice normal)in Mass and covering exponents for fixed-length honeycomb walks, 26 September 2026.
Theorem 2.1(Finite bridge estimates)in Renewal and changes of law for critical honeycomb walks, 26 September 2026.
Theorem 1.1(Finite bridge estimates)in Uniform marked-polygon estimates and sharp finite bridge moments, 26 September 2026.
Theorem 1.2(Cylinder amplitude and planar nesting)in Cap-selected amplitudes and triangle chords for honeycomb walks, 26 September 2026.
Theorem 1.1(Prescribed boundary endpoints)in Critical honeycomb chords with prescribed boundary endpoints, 26 September 2026.
Corollary 1.3(Covering dimension at polynomially separated scales)in Mass and covering exponents for fixed-length honeycomb walks, 26 September 2026.
Corollary 1.4(Radius of gyration and moments)in Mass and covering exponents for fixed-length honeycomb walks, 26 September 2026.
Corollary 1.2(Length cutoffs)in Radial transfer estimates and polygon length laws for honeycomb walks, 26 September 2026.
Theorem 1.2(Finite chords and marked polygons)in Signed cylinder propagation and marked polygons on the honeycomb lattice, 26 September 2026.
Theorem 1.1(Cylinder fugacity exponent)in Cylinder loop weights and planar nesting, 26 September 2026.
Proposition 1.3(Mixed exits)in Polynomial vacuum representations and bridge mass for honeycomb walks, 26 September 2026.
Theorem 1.2(Hexagon visits)in Polynomial vacuum representations and bridge mass for honeycomb walks, 26 September 2026.
Theorem 1.1(A logarithmic bridge-length window)in Cylinder amplitudes and logarithmic bridge-length windows on the honeycomb lattice, 26 September 2026.
Theorem 1.1(Bridge mass retained in a fixed corridor)in Disk transfer representations and confined bridge mass, 26 September 2026.
Theorem 1.4(Normalized separator pairing)in Polynomial vacuum representations and bridge mass for honeycomb walks, 26 September 2026.
Theorem 2.8in Renewal and changes of law for critical honeycomb walks, 26 September 2026.
Theorem 1.1(Cylinder pressure and planar nesting)in Signed cylinder propagation and marked polygons on the honeycomb lattice, 26 September 2026.
Theorem 1.2(Two axial marks)in Uniform marked-polygon estimates and sharp finite bridge moments, 26 September 2026.
Theorem 1.1(Critical strip mass)in Critical strip-crossing mass on the honeycomb lattice, 26 September 2026.
Theorem 1.1(Squared-length polygon mass)in Marked polygon correlations and one-arc bounds, 26 September 2026.
Theorem 1.1(Strip mass and bridge length)in Polynomial vacuum representations and bridge mass for honeycomb walks, 26 September 2026.
Theorem 2.7(Infinite spatial law)in Renewal and changes of law for critical honeycomb walks, 26 September 2026.
Reported proof verification
Four Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
We prove critical diameter-tail exponents −2 for unrooted honeycomb polygons and −2/3 for length-weighted polygons, together with a truncated second-length-moment bound of exponent 2/3. Consequently, polygons conditioned to have length at least n have diameter \(n^{3/4+o(1)}\) in probability under either weight.
Critical self-avoiding walks between prescribed, macroscopically separated boundary ports of a regular honeycomb hexagon have length \(R^{4/3+o(1)}\) in probability, where R is the scale of the hexagon. We prove the corresponding statements for half-plane arches, parallel cuts and nonparallel pure cuts. The half-plane law also has mean length \(R^{4/3+o(1)}\). A separate strip argument gives endpoint mean laws on one density-one set of heights and in an aligned, critically weighted mixture of all even heights in a macroscopic interval.
We determine the growth exponent, at every fixed positive loop fugacity, of the critical honeycomb partition function for disjoint polygons separating two prescribed markers on a balanced cylinder. At fugacity two the cylinder exponent is 1/6; the corresponding planar nesting exponent and middle-strip nesting exponent are 1/12.
For uniform self-avoiding walks of every sufficiently large integer length on the honeycomb lattice, we prove diameter exponent 3/4 and simultaneous local-mass and covering exponent 4/3, with arbitrary positive exponent slack and arbitrary polynomial failure probability.
At the critical activity and loop fugacity two, we prove a 1/6 partition exponent for disjoint honeycomb polygons separating opposite marks on a balanced infinite cylinder, and a 1/12 planar nesting exponent. For ordered first-exit chords in a regular hexagon of side R, with both boundary ports summed and diameter at least \(R/10\), the finite critical partition is \(R^{3/4+o(1)}\) and the normalized mean length is \(R^{4/3+o(1)}\). A separate two-bond estimate on tilted cylinders with controlled site proportions bounds the length-square mass of planar polygons of diameter at most H, modulo translations, by \(H^{2/3+o(1)}\).
We prove a logarithmic window of critical honeycomb bridge lengths: summed through height \(2h(\log h)^{1/64}\), bridges of lengths between \(h^{4/3}(\log h)^{-1/8}\) and \(2h^{4/3}(\log h)^{1/2}\) have mass at least \(h^{3/4}(\log h)^{-C}\).
At the critical honeycomb vertex activity, the squared-length mass of simple polygons of diameter at most H, counted modulo translations, is at most \(H^{2/3+o(1)}\). We also prove a quantitative two-mark cylinder estimate and a polynomial one-arc bound uniform even for arbitrarily unequal marked intervals.
We prove that critical honeycomb bridges crossing a strip of width R have mean length \(R^{4/3+o(1)}\), with the same exponent after confinement to a fixed multiple of the strip width. The initial boundary port is fixed, the terminal port is summed, and all finite lengths receive their critical weights. The bridge mass is comparable to R−1/4; the half-plane arch kernel at endpoint separation m is comparable to m−5/4.
We prove that, under the all-length critical measure, a honeycomb bridge crossing a strip of h layers, with its initial port fixed and its terminal port free, has mean length \(h^{4/3+o(1)}\). We also obtain central visit probability \(R^{-2/3+o(1)}\) and mean length \(R^{4/3+o(1)}\) for macroscopic free-boundary chords in a regular hexagon.
For critical honeycomb self-avoiding walk, we prove spatial exponent 3/4 for the infinite irreducible-bridge law and for bridges of every sufficiently large compatible even length. We establish the corresponding thermal laws at every large discount scale, including all positive length and spatial moments. For unrestricted uniform walks, the endpoint lower law holds on a common set of lengths of natural density one. We also determine the near-critical exponential correlation scale and small-force free-energy exponent, and prove spatial local lower bounds that permit conditioning on a prescribed terminal vertex.
At the critical weight of the regular honeycomb lattice, the total weight of self-avoiding paths crossing a strip of height N is comparable to N−1/4. The first horizontal-displacement moment of return paths is comparable to N3/4.
We prove a uniform bound for critical honeycomb polygons through two axial marks on a periodic staircase. The bound retains an explicit power of the ratio between the period and the marked separation. We also prove sharp finite strip estimates: bridge mass of order h−1/4, first-length mass at most \(Ch^{13/12}\), and mass at least \(ch^{-1/4}\) on bridges with length at least \(ch^{4/3}\).
At the critical honeycomb fugacity, self-avoiding port-to-port chords in an equilateral lattice triangle of side R, summed over both boundary endpoints and restricted to diameter at least \(R/100\), have partition sum comparable to R3/4 and mean length \(R^{4/3+o(1)}\). We also determine the amplitude selected by two vacuum caps on a cylinder of circumference N and prove that it grows as \(N^{1/6+o(1)}\).
Four Lean statements in this family
Choose one to see it beside the paper theorem it is paired with. The outside readers find that the release’s Lean states a supporting or different result, so the theorem it is paired with is shown under its own heading.
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.
HoneycombBridgeMassSupport
The paper states
No paper theorem is paired with this Lean statement.
no paper statement matches the Lean text clearly enough to pair, so the closest candidates are listed below.
Statements it shares words with:
Proposition 5.1(Boundary exponent)in Polynomial vacuum representations and bridge mass for honeycomb walks, 26 September 2026.
Theorem 1.1(Strip mass and bridge length)in Polynomial vacuum representations and bridge mass for honeycomb walks, 26 September 2026.
Proposition 11.1(Finite chord length mass)in Cylinder amplitudes and logarithmic bridge-length windows on the honeycomb lattice, 26 September 2026.
Proposition 4.1(Finite calibrated input)in Renewal and changes of law for critical honeycomb walks, 26 September 2026.
Proposition 2.1(Finite boundary and length inputs)in Critical honeycomb chords with prescribed boundary endpoints, 26 September 2026.
Theorem 2.2(Boundary flux and strip mass)in Mass and covering exponents for fixed-length honeycomb walks, 26 September 2026.
Theorem 1.3(Nesting and free boundary length)in Uniform marked-polygon estimates and sharp finite bridge moments, 26 September 2026.
Proposition 7.4(Boundary occupancy)in Uniform marked-polygon estimates and sharp finite bridge moments, 26 September 2026.
HoneycombBridgeMassSupport.lean, the release lists it as a main result.
defFiniteBridgeMassEstimate : Prop := ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ h : ℕ, ENNReal.ofReal (c * (1 + (h : ℝ)) ^ (-(1 : ℝ) / 4)) ≤ bridgeMass h ∧ bridgeMass h ≤ ENNReal.ofReal (C * (1 + (h : ℝ)) ^ (-(1 : ℝ) / 4))⋮theoremfiniteBridgeMassEstimate : FiniteBridgeMassEstimate := bysorry
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.
CriticalStripMass.lean, the release lists it as a supporting statement.
defCriticalStripMass : Prop := (∀ N : ℕ, 1 ≤ N → StripSumsFinite N) ∧ (∀ N : ℕ, 1 ≤ N → c * archMass N + bridgeMass N = 1) ∧ Comparable (fun N => moment (N + 1) - moment N) bridgeMass ∧ Comparable moment (fun N => (N : ℝ) ^ (3 / 4 : ℝ)) ∧ Comparable bridgeMass (fun N => (N : ℝ) ^ (-(1 / 4) : ℝ)) ∧ (∀ N : ℕ, 1 ≤ N → bridgeMass (N + 1) ≤ bridgeMass N)⋮theoremcritical_strip_mass : CriticalStripMass := bysorry
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.
HoneycombBridgeFiniteness.lean, the release lists it as a supporting statement.
defFiniteBridgeSums : Prop := ∀ h : ℕ, 1 ≤ h → Summable (weight (h := h)) ∧ Summable (firstLengthWeight (h := h)) ∧ Summable (fun p : BridgePath h => firstLengthWeight p / bridgeMass h) ∧ Summable (fun p : ConfinedBridgePath h => weight p.val) ∧ Summable (fun p : ConfinedBridgePath h => firstLengthWeight p.val) ∧ Summable (fun p : ConfinedBridgePath h => firstLengthWeight p.val / confinedMass h)⋮theoremfinite_bridge_sums : FiniteBridgeSums := bysorry
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”.
Let D_R be convex pure lattice hexagons which, after scaling by R, converge to a regular hexagon. Let a_R,b_R be boundary ports whose scaled limits are distinct points in the relative interiors of sides. Then, for every \varepsilon>0, the critical chord law satisfies
The same conclusion holds in a full half-plane for prescribed boundary ports at distance R, in a strip of height comparable to R for one prescribed port on each of the two opposite boundary cuts, at mutual distance O(R), and in a wedge of angle \pi/3 or 2\pi/3 formed by two nonparallel pure cuts, with one prescribed port on each ray. In the wedge, each endpoint has clearance comparable to R from the other cut and distance O(R) from the apex. Constants are uniform on fixed compact sets of these nondegenerate scaled geometries. In each case the normalizing mass is at least cR^{-5/4}.
The words they share: boundary, chord, comparable, constants, critical, endpoint, fixed, height, lattice, mass, port, ports, prescribed, strip, uniform.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
HoneycombFreeEnergy.lean, the release lists it as a supporting statement.
theoremlogPartition_tendsto (o : Vertex) (e : ℂ) (s : ℝ) : Tendsto (logPartition o e s) atTop (𝓝 (freeEnergy o e s)) := bysorry
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”.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.
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 a supporting result (their term: “supporting-only”).
Their note:The four challenges are analytic inputs, not the headline: finiteness of the critical bridge sums and first-length moments at every strip height (HoneycombBridgeFiniteness), the strip estimates B_N ≍ N^{-1/4}, arch moment ≍ N^{3/4}, c*A_N+B_N=1 (CriticalStripMass, with the bridge-mass bound restated for h>=0 in HoneycombBridgeMassSupport), and existence of the force-tilted free-energy limit (HoneycombFreeEnergy). None mentions the uniform measure on n-step self-avoiding walks, their diameter, local mass or covering numbers, or any probability bound, so the headline theorem (diameter between n^{3/4-delta} and n^{3/4+delta} with probability at least 1-C n^{-k}) is not stated.
Definitions the group asks readers to compare with the paper:rho / kappa / criticalActivity: the four files use 1/sqrt(2+sqrt 2), (2cos(pi/8))^-1, (2+sqrt 2)^(-1/2) and (sqrt(2+sqrt 2))^-1, all equal to the honeycomb critical activity x_c (2cos(pi/8) = sqrt(2+sqrt 2)); a fixed concrete constant, standard; Triangle (CriticalStripMass) / Vertex (BridgeFiniteness, FreeEnergy) / Center (BridgeMassSupport): the honeycomb lattice realised as up/down triangles of the triangular tiling with the same three-neighbour adjacency up(i,j) ~ down(i,j), down(i,j-1), down(i-1,j); CriticalStripMass uses rows in N (half-plane with a bottom wall), the others rows in Z; concrete lattice, standard; CriticalStripMass.moment: sum over k >= 1 of k*K(k), a one-sided first displacement moment of arches (the paper’s m_N); an unnormalised sum over all path lengths, not the displacement of a fixed-length walk; CriticalStripMass: lambda, d, C, eta are defined but unused by the statement; tsum is 0 for non-summable families, guarded by the explicit StripSumsFinite conjunct; HoneycombBridgeFiniteness.InLogCorridor / ConfinedBridgePath: confinement |x| <= h*(log h)^2 restricts to a finite vertex set for each h, so the three confined summability conjuncts are automatic (log 1 = 0 forces x = 0 at h = 1, so no bridge is confined there); the paper’s content for the corridor (exponents unchanged) is not stated; HoneycombBridgeFiniteness.FiniteBridgeSums: purely qualitative summability for each h >= 1, no rates; the normalised conjuncts divide by bridgeMass h / confinedMass h (Lean x/0 = 0, harmless here); HoneycombBridgeMassSupport.bridgeMass: ENNReal-valued tsum with B_0 := 1 by an if; Port and Port.position are defined but unused; the theorem’s docstring says ‘Trusted reference hole only; missing necessary main obligation’; HoneycombFreeEnergy.freeEnergy: limUnder atTop (logPartition..), a junk-valued limit, so logPartition_tendsto is exactly ‘the limit exists’; e : C is not required to be a unit vector and s : R may have either sign (more general than the paper’s unit e, s >= 0)
“supporting-only”, in their words: The challenge statements state a lemma or auxiliary result, not the headline.
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.
cert-machine finds that the Lean statements express a different result (their term: “DIFFERENT”).
The gap they name:The headline (diameter n^{3/4+o(1)} and mass/covering exponent 4/3 for uniform fixed-length honeycomb SAW, the content of ‘Mass-and-covering-exponents-for-fixed-length-honeycomb-walks’) is stated by no challenge. The four challenges state ingredients from other manuscripts of the family: finiteness of critical bridge sums, existence of the forced free energy, the strip-crossing mass ≍ N^{-1/4} with displacement moment ≍ N^{3/4}, and strict-bridge mass ≍ (1+h)^{-1/4}. None implies the headline and the headline implies none of them.
“DIFFERENT”, in their words: The challenge statements state a different theorem from the headline.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
The linked formalization establishes finiteness of the critical bridge measures used in the paper. For every strip height $h\ge1$, the total weight and first length moment of self-avoiding honeycomb bridges from a fixed initial port to a free terminal port are finite. The corresponding sums are also finite when the bridge is confined to the corridor of horizontal width $h(\log h)^2$, including the normalized first-moment sums.
These are supporting summability statements. The paper’s $h^{4/3+o(1)}$ mean-length law and its central-visit and hexagonal-chord exponents are outside them.
The linked formalization proves existence of the infinite-length free energy for the critical honeycomb self-avoiding-walk partition function. For every starting vertex, force direction, and real force parameter, the logarithm of the length-$n$ partition function divided by $n$ converges to its stated free-energy limit.
This selected result supplies the limiting free energy. It does not state the paper’s small-force exponent, near-critical correlation scale, or the $3/4$ spatial and moment laws.
For critical self-avoiding walks on the honeycomb lattice, the formalization proves that the total weight of paths crossing a strip of height $N$ is comparable to $N^{-1/4}$, while the first horizontal-displacement moment of return paths is comparable to $N^{3/4}$. It also proves finiteness of the strip sums, the exact arch–bridge balance identity, comparison of successive moment increments with bridge mass, and monotonicity of bridge mass. The comparison constants are uniform in the strip height.
For the prescribed-boundary-endpoint companion, let $B_h$ be the total critical weight of strict bridges crossing a strip of integral height $h$, from one fixed bottom port to all compatible top ports, with $B_0=1$. The formalization proves
$c(1+h)^{-1/4}\le B_h\le C(1+h)^{-1/4}$
for all $h\ge0$ and fixed positive constants $c,C$. This includes finiteness of the path sum. The prescribed-endpoint length law, arch and strip mean laws, and remaining moment and renewal conclusions are outside this supporting statement.
AI-drafted comparisons, with no recorded human review
Strict honeycomb bridge mass of order $(1+h)^{-1/4}$HoneycombBridgeMassSupport
Unreviewed AI draft: states a supporting result. States the two-sided bound B_h ≍ (1 + h)^{-1/4} on strict bridge mass, an input estimate for the prescribed-endpoint paper and one of the five supporting comparisons named in the Comparator README. The theorem’s docstring in the challenge file reads “Trusted reference hole only; missing necessary main obligation.”
Critical honeycomb strip mass and displacement momentCriticalStripMass
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the strip-mass paper: strip-crossing weight comparable to N^{-1/4} and return-path displacement moment comparable to N^{3/4}, with uniform constants, finiteness and the balance identity.
Finiteness of critical bridge mass and first length momentsHoneycombBridgeFiniteness
Unreviewed AI draft: states a supporting result. States finiteness of critical bridge weights and first length moments, which the note calls supporting summability statements. The h^{4/3+o(1)} mean-length law and the other exponents of the paper are outside them.
Existence of the honeycomb free-energy limitHoneycombFreeEnergy
Unreviewed AI draft: states a supporting result. States existence of the infinite-length free energy for the critical honeycomb walk with a force parameter. The small-force exponent, correlation scale and the 3/4 spatial and moment laws are not stated.
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.
Strict honeycomb bridge mass of order $(1+h)^{-1/4}$HoneycombBridgeMassSupport
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.
Chokmah LLC, chokmah-me/fragile-proof-audit: replay audits including receipts for families 237 and 005, 9 October 2026. Source
Axiom-audit receipt: headline theorem depends only on propext, Classical.choice, Quot.sound after a clean rebuild.
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.
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 proof and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
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
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 237The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.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
“supporting-only”
What their term means
The challenge statements state a lemma or auxiliary result, not the headline.
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 a different theorem from the headline.
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
10 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 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 211 s; peak memory 6.2 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 40 s).
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.
Finiteness of critical bridge mass and first length moments
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.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.