Proves that the standard sine map on the two-dimensional torus has positive metric entropy with respect to area for every sufficiently large positive parameter. This establishes Sinai’s positive-parameter-measure conjecture for the original family, with the stronger conclusion of a full parameter tail. (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
In Positive Metric Entropy for the Standard Map at Large Parameters, 23 September 2026
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
There exists k_0>0 such that
Equivalently, for every such k the largest Lyapunov exponent of f_k is positive on a set of positive m-measure.
In Positive Metric Entropy for the Standard Map at Large Parameters, 23 September 2026
Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.
For each k\ge k_0 there is a measurable f_k-invariant set E=E(k) with m(E)>0 such that (E,m(E)^{-1}m|_E,f_k) is ergodic and f_k has one positive and one negative Lyapunov exponent almost everywhere on E. For some integer N=N(k,E)\ge1, there is a measurable partition E=E_0\sqcup\cdots\sqcup E_{N-1} such that f_k(E_j)=E_{j+1\bmod N} and (E_j,m(E_j)^{-1}m|_{E_j},f_k^N) is Bernoulli for every j. All invariance and partition statements are modulo m-null sets; each E_j has area m(E)/N>0.
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.
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.
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.
StandardMapComponentsThe paper states
In Positive Metric Entropy for the Standard Map at Large Parameters, 23 September 2026
For each k\ge k_0 there is a measurable f_k-invariant set E=E(k) with m(E)>0 such that (E,m(E)^{-1}m|_E,f_k) is ergodic and f_k has one positive and one negative Lyapunov exponent almost everywhere on E. For some integer N=N(k,E)\ge1, there is a measurable partition E=E_0\sqcup\cdots\sqcup E_{N-1} such that f_k(E_j)=E_{j+1\bmod N} and (E_j,m(E_j)^{-1}m|_{E_j},f_k^N) is Bernoulli for every j. All invariance and partition statements are modulo m-null sets; each E_j has area m(E)/N>0.
The words they share: hyperbolic, bernoulli, component, area, ergodic, integer, lyapunov, measurable, invariant, positive.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
StandardMapComponents.lean, the release lists it as a supporting statement.
def MainComponentsObligation : Prop := ∃ k₀ : ℝ, 0 < k₀ ∧ ∀ k : ℝ, k₀ ≤ k → HyperbolicBernoulliComponent ktheorem main_components : MainComponentsObligation := by sorryThis 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
StandardMapEntropyThe paper states
In Positive Metric Entropy for the Standard Map at Large Parameters, 23 September 2026
There exists k_0>0 such that
Equivalently, for every such k the largest Lyapunov exponent of f_k is positive on a set of positive m-measure.
The words they share: measure, metric, standard, map, entropy, largest, exponent, lyapunov, positive.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
StandardMapEntropy.lean, the release lists it as a supporting statement.
def MainObligation : Prop := ∃ k₀ : ℝ, 0 < k₀ ∧ ∀ k : ℝ, k₀ ≤ k → 0 < metricEntropy area (standardMap k)theorem main_entropy : MainObligation := by sorryThis 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
StandardMapLyapunovThe paper states
In Positive Metric Entropy for the Standard Map at Large Parameters, 23 September 2026
There exists k_0>0 such that
Equivalently, for every such k the largest Lyapunov exponent of f_k is positive on a set of positive m-measure.
The words they share: largest, lyapunov, measure, positive, metric, standard, map, entropy, exponent.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
StandardMapLyapunov.lean, the release lists it as a supporting statement.
theorem main_entropy_complete : ∃ k₀ : ℝ, 0 < k₀ ∧ ∀ k : ℝ, k₀ ≤ k → 0 < metricEntropy area (standardMap k) ∧ PositiveLargestLyapunov k ∧ (0 < metricEntropy area (standardMap k) ↔ PositiveLargestLyapunov k) := by sorryThis 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
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: main_entropy : ∃ k₀ > 0, ∀ k ≥ k₀, 0 < metricEntropy area (standardMap k) is the headline verbatim (full parameter tail); the Lyapunov and hyperbolic Bernoulli-component claims are also stated (Lyapunov, Components). Parameter is k·sin(2πx) on (ℝ/ℤ)², i.e. Chirikov K = 2πk, immaterial for ‘k large’.
Definitions the group asks readers to compare with the paper: metricEntropy μ f := ⨆ r, ⨆ p : FinitePartition r, partitionEntropy μ f p with partitionEntropy := ⨅ n, ofReal (blockEntropy μ f p (n+1)/(n+1)): custom (not in Mathlib); the inf form equals the usual limit only for measure-preserving f, which holds here (checked: the map is a composition of shears) but is not part of the statement; Two statement files (StandardMapComponents, StandardMapLyapunov) contain the meta command run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {} (clears the aux-lemma cache; not a fidelity issue, but non-standard in a Comparator statement)
“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.
cert-machine finds that the Lean statements express or imply the whole advertised result (their term: “MATCHES”).
“MATCHES”, in their words: 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.
OpenAI’s own note on what its Lean covers
The formalization proves Sinai’s positive-entropy conjecture for the standard sine map on the two-dimensional torus in the stronger form of a full positive parameter tail. For every sufficiently large parameter, normalized area has positive metric entropy, and a positive-area set has positive largest Lyapunov exponent with the stated derivative-growth limit.
It also constructs a positive-area invariant ergodic hyperbolic component. That component splits into finitely many cyclic pieces on each of which the corresponding iterate is Bernoulli. No genericity assumption on the parameter is used.
Positive-area hyperbolic Bernoulli component StandardMapComponents
Unreviewed AI draft: states a consequence of a paper’s theorem. States the paper’s corollary: a positive-area ergodic hyperbolic component splitting into finitely many cyclic Bernoulli pieces, rather than the entropy theorem itself.
Positive metric entropy for all sufficiently large parameters StandardMapEntropy
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: the standard map has positive metric entropy for every sufficiently large parameter.
Positive Lyapunov exponents and entropy StandardMapLyapunov
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem in its Lyapunov form: positive entropy and a positive-area set with positive largest Lyapunov exponent and the stated derivative growth, for all large parameters.
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.
StandardMapComponentsTwo 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. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
StandardMapEntropyTwo 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. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
StandardMapLyapunovTwo 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. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 8 October 2026 | Original report |
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.
This family’s papers cite no paper elsewhere in the release.
No paper elsewhere in the release cites this family’s papers.
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
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: StandardMapComponents, StandardMapEntropy, StandardMapLyapunovSuggest a source attributionSuggest a change
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.
Author not stated. Source
From terrytao.wordpress.com, 8 October 2026. Source
Joerg Neunhaeuserer says they spent much of their career on a problem now claimed by OpenAI (they cite the number 146; read here as the family on the standard map), is relieved not to have to do that work, and is proud their intuition about the answer was right.
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Why this passage is shown
Theorem 1.1
In Positive Metric Entropy for the Standard Map at Large Parameters, 23 September 2026
Why this passage is shown
Corollary 1.2 (Nonuniformly hyperbolic ergodic component)
In Positive Metric Entropy for the Standard Map at Large Parameters, 23 September 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, StandardMapComponents
Proof-verification report
MathVet, StandardMapComponents
Proof-verification report
cert-machine, StandardMapEntropy
Proof-verification report
MathVet, StandardMapEntropy
Proof-verification report
cert-machine, StandardMapLyapunov
Proof-verification report
MathVet, StandardMapLyapunov
Lean statement
StandardMapComponents
Lean statement
StandardMapEntropy
Lean statement
StandardMapLyapunov