Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Directional zero–one laws beyond iid environments and iid ballisticity

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

On ℤd, d ≥ 3, directional escape has probability zero or one for iid strictly elliptic nearest-neighbor environments, and for stationary ergodic finite-range-dependent environments under uniform ellipticity. In iid uniformly elliptic environments with d ≥ 2, almost-sure directional transience implies a deterministic limiting velocity with positive projection in that direction, resolving the ballisticity conjecture. (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 only part of the result described above, or a narrower statement. Read the assessments

What the papers state

Theorem 1.1 (Directional transience implies ballisticity)

In Directional transience implies ballisticity, 23 September 2026

The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.

Let d\ge2 and let P=\nu^{\otimes\mathbb Z^d} be an iid law of nearest-neighbor transition rows satisfying uniform ellipticity. If \ell\in S^{d-1} and P_0(A_\ell)=1, then there exists a deterministic vector v=v(\nu)\in\mathbb R^d such that

v\cdot\ell>0, \qquad P_0\!\left(\lim_{n\to\infty}\frac{X_n}{n}=v\right)=1.

In particular, the walk is ballistic in the same direction \ell.

Corollary 1.2 (Positive-probability transience and the velocity hemisphere)

In Directional transience implies ballisticity, 23 September 2026

Possible match to OpenAI’s description, selected because it shares the most wording. No review confirming the selection is recorded.

Let d\ge3 and let P=\nu^{\otimes\mathbb Z^d} be an iid law of nearest-neighbor transition rows satisfying uniform ellipticity. For a fixed \ell\in\mathbb R^d\setminus\{0\}, set A_\ell=\{X_n\cdot\ell\longrightarrow+\infty\}. If P_0(A_\ell)>0, then there is a deterministic nonzero vector v=v(\nu) such that

v\cdot\ell>0, \qquad P_0\!\left(\lim_{n\to\infty}\frac{X_n}{n}=v\right)=1.

If such a direction exists, then the deterministic sets of directions satisfy

\{u\in S^{d-1}:P_0(A_u)=1\} =\{u\in S^{d-1}:P_0(A_u)>0\} =\{u\in S^{d-1}:v\cdot u>0\}.

In particular, P_0(A_u)=0 for each fixed u\in S^{d-1} with v\cdot u\le0, including every equator direction. The equality concerns annealed probabilities for each fixed deterministic direction, not a simultaneous pathwise assertion over all directions.

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.

Two more possible matches

  • Theorem 1.1 in A directional zero–one law under strict ellipticity, 23 September 2026.
  • Theorem 1.1 (Directional zero–one law) in A directional zero–one law for finite-range-dependent random environments, 5 October 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.
Papers and explanations
Three current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

A directional zero–one law for finite-range-dependent random environments

5 October 2026, current edition.

Read it herePDF

We prove a directional zero–one law for uniformly elliptic nearest-neighbor random walks in stationary, ergodic, finite-range-dependent environments on ℤd, d ≥ 3. For every fixed nonzero real direction, the probability of escape in that direction, averaged over the environment, is either zero or one. Finite-range dependence is imposed on the full transition rows: collections of rows at distance greater than a fixed range are independent, including collections indexed by infinite deterministic sets.

A directional zero–one law under strict ellipticity

23 September 2026, current edition.

Read it herePDF

We prove the directional zero–one conjecture for nearest-neighbor random walks in independent and identically distributed strictly elliptic environments on ℤd, d ≥ 3: the probability of escape in each fixed nonzero real direction is zero or one. Only strict positivity of the transition probabilities is required; no uniform lower bound or moment assumption is imposed.

Directional transience implies ballisticity

23 September 2026, current edition.

Read it herePDF

We prove that almost-sure transience in a fixed direction implies a deterministic limiting velocity with positive projection in that direction for nearest-neighbor random walks in independent and identically distributed uniformly elliptic environments on ℤd, d ≥ 2. This resolves the ballisticity conjecture positively.

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.

DirectionalBallisticity

The paper states

Theorem 1.1 (Directional transience implies ballisticity)

In Directional transience implies ballisticity, 23 September 2026

Let d\ge2 and let P=\nu^{\otimes\mathbb Z^d} be an iid law of nearest-neighbor transition rows satisfying uniform ellipticity. If \ell\in S^{d-1} and P_0(A_\ell)=1, then there exists a deterministic vector v=v(\nu)\in\mathbb R^d such that

v\cdot\ell>0, \qquad P_0\!\left(\lim_{n\to\infty}\frac{X_n}{n}=v\right)=1.

In particular, the walk is ballistic in the same direction \ell.

The words they share: ballisticity, implies, vector, uniform, transience, transition, rows, real, directional, direction, integer, law, nearest, neighbor, deterministic.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Directional transience implies ballisticity

DirectionalBallisticity.lean, the release lists it as a main result.

def MainStatement : Prop :=  ∀ (d : ℕ), 2 ≤ d → ∀ (ν : Measure (Row d)), IsProbabilityMeasure ν →    UniformElliptic ν → ∀ (ℓ : Vector d), dot ℓ ℓ = 1 →    DirectionallyTransient ν ℓ →    ∃ v : Vector d, 0 < dot v ℓ ∧ HasVelocity ν vtheorem directional_transience_implies_ballisticity : MainStatement := by  sorry

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.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

DirectionalWalk

The paper states

The words they share: ellipticity, transition, rows, eq, law, strict, one, zero, directional, distributed, identically, nearest, neighbor, independent.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Directional zero–one law under strict ellipticity

DirectionalWalk.lean, the release lists it as a supporting statement.

theorem directional_zero_one (d : ℕ) (hd : 3 ≤ d)    (μ : Measure (Row d)) [IsProbabilityMeasure μ]    (hell : StrictEllipticity μ) (ℓ : Fin d → ℝ) (hℓ : ℓ ≠ 0) :    annealed μ 0 (escape ℓ) = 0 ∨ annealed μ 0 (escape ℓ) = 1 := by sorry

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.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

VelocityHemisphere

The paper states

Corollary 1.2 (Positive-probability transience and the velocity hemisphere)

In Directional transience implies ballisticity, 23 September 2026

Let d\ge3 and let P=\nu^{\otimes\mathbb Z^d} be an iid law of nearest-neighbor transition rows satisfying uniform ellipticity. For a fixed \ell\in\mathbb R^d\setminus\{0\}, set A_\ell=\{X_n\cdot\ell\longrightarrow+\infty\}. If P_0(A_\ell)>0, then there is a deterministic nonzero vector v=v(\nu) such that

v\cdot\ell>0, \qquad P_0\!\left(\lim_{n\to\infty}\frac{X_n}{n}=v\right)=1.

If such a direction exists, then the deterministic sets of directions satisfy

\{u\in S^{d-1}:P_0(A_u)=1\} =\{u\in S^{d-1}:P_0(A_u)>0\} =\{u\in S^{d-1}:v\cdot u>0\}.

In particular, P_0(A_u)=0 for each fixed u\in S^{d-1} with v\cdot u\le0, including every equator direction. The equality concerns annealed probabilities for each fixed deterministic direction, not a simultaneous pathwise assertion over all directions.

The words they share: hemisphere, velocity, annealed, vector, uniform, transience, transition, rows, real, direction, probabilities, positive, integer, law, nonzero.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Positive-probability transience and the velocity hemisphere

VelocityHemisphere.lean, the release lists it as a supporting statement.

theorem positive_probability_transience_velocity_hemisphere    {d : ℕ} (hd : 3 ≤ d) (ν : Measure (Row d)) [IsProbabilityMeasure ν]    (hue : UniformElliptic ν) (ℓ : Vector d) (hℓ : ℓ ≠ 0)    (hpos : 0 < annealedLaw ν (TransientPaths ℓ)) :    ∃ v : Vector d,      v ≠ 0 ∧ 0 < dot v ℓ ∧ annealedLaw ν (VelocityPaths v) = 1 ∧      (∀ w : Vector d, annealedLaw ν (VelocityPaths w) = 1 → w = v) ∧      {u : Vector d | dot u u = 1 ∧ annealedLaw ν (TransientPaths u) = 1} =        {u : Vector d | dot u u = 1 ∧ 0 < annealedLaw ν (TransientPaths u)} ∧      {u : Vector d | dot u u = 1 ∧ 0 < annealedLaw ν (TransientPaths u)} =        {u : Vector d | dot u u = 1 ∧ 0 < dot v u} ∧      (∀ u : Vector d, dot u u = 1 → dot v u ≤ 0 →        annealedLaw ν (TransientPaths u) = 0) := by  sorry

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.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

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?

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 part of the advertised result (their term: “partial”).

Their note: Stated: directional_zero_one (d) (hd : 3 ≤ d) (hell : StrictEllipticity μ) (ℓ ≠ 0) : annealed μ 0 (escape ℓ) = 0 ∨... = 1 for IID environments (environmentLaw μ = infinitePi (fun _ => μ)), and directional_transience_implies_ballisticity (d >= 2, iid uniformly elliptic, DirectionallyTransient ν ℓ → ∃ v, 0 < dot v ℓ ∧ HasVelocity ν v), plus the velocity-hemisphere refinement. Not stated: the zero-one law for stationary ergodic finite-range-dependent environments under uniform ellipticity (the docs title says 'beyond iid environments’ but the scope and Lean are iid only).

“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.

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.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNLINKED”).

The gap they name: The directional zero–one law for stationary ergodic finite-range-dependent uniformly elliptic environments is claimed but not stated by any family-220 challenge.

“NARROWER — UNLINKED”, in their words: The challenge statements state less than the headline; the missing part comes from a paper the Lean note does not link.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

The directional zero–one conjecture asks whether a random walk’s probability of escape in a fixed direction must be zero or one. The formalization proves this for nearest-neighbor walks in independent identically distributed strictly elliptic environments on $\mathbb Z^d$, for every $d\ge3$ and every nonzero real direction. Strict ellipticity means that every allowed transition probability is positive almost surely; no uniform positive lower bound or moment condition is assumed. The probability is the annealed law from the origin.

For an i.i.d. uniformly elliptic nearest-neighbor random environment on $\mathbb Z^d$, the formalization proves that almost-sure directional transience implies convergence of $X_n/n$ to a deterministic velocity with positive projection in that direction for every $d\ge2$. For $d\ge3$, positive probability of transience in any nonzero direction already suffices. The limiting velocity is unique, and the unit directions with positive transience probability are exactly the open hemisphere having positive inner product with that velocity; transience has probability one on that hemisphere and zero on its complement. The environment is sampled once and retained along the walk, and the probabilities use the annealed law from the origin.

AI-drafted comparisons, with no recorded human review

  • Directional transience implies ballisticity DirectionalBallisticity

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: in uniformly elliptic i.i.d. environments, almost-sure directional transience implies ballisticity with a deterministic velocity, for d ≥ 2.

  • Directional zero–one law under strict ellipticity DirectionalWalk

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: the directional zero–one law for random walks in i.i.d. strictly elliptic environments on Z^d, d ≥ 3.

  • Positive-probability transience and the velocity hemisphere VelocityHemisphere

    Unreviewed AI draft: states a consequence of a paper’s theorem. States the paper’s corollary for d ≥ 3: positive probability of transience suffices, and the transient directions form the open hemisphere determined by the velocity.

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.

Directional transience implies ballisticity DirectionalBallisticity

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal 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.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Directional zero–one law under strict ellipticity DirectionalWalk

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal 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.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Positive-probability transience and the velocity hemisphere VelocityHemisphere

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal 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.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

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.

Within this family

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.

Offer to write an explanationCompare one Lean statement with its paper: DirectionalWalk, DirectionalBallisticity, VelocityHemisphereSuggest a source attributionSuggest a change

What people have said

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 “Major math journal”. The page says that nothing on it is verified.

    Author not stated. Source

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 220 The 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

Compare the proposed paper and Lean matches

  • Family 220 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form