Sinai's positive metric entropy conjecture for the standard map
From OpenAI Aftermath
Sinai's positive metric entropy conjecture for the standard map asks whether the Chirikov standard map, an area-preserving map of the two-dimensional torus, has positive metric entropy with respect to area for a set of parameters of positive measure; equivalently, whether its largest Lyapunov exponent is positive on a set of positive area for such parameters. Hyperbolic sets of zero area, even of full Hausdorff dimension, do not suffice. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims positive metric entropy for every sufficiently large parameter, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- The standard map arose as a model of conservative instability in work of Chirikov. Duarte constructed hyperbolic basic sets and exhibited elliptic islands and tangencies for large parameters, and Gorodetski obtained transitive invariant sets of full Hausdorff dimension for a residual set of large parameters; neither hyperbolic sets nor full dimension give positive area, and residual parameter sets need not have positive measure.
- Obata proved uniqueness of the measure of maximal entropy for large parameters, and Oliveira proved positive topological entropy for every positive parameter except one value; neither identifies entropy for area. Berger and Turaev proved Herman's positive-entropy conjecture by conservative perturbations, and positive exponents are known for skew products and randomly perturbed standard maps. The manuscript cites Berger and Turaev's formulation of Sinai's conjecture and its large-parameter form recorded by Obata.
The original result
- Claim. Theorem 1.1 of Positive Metric Entropy for the Standard Map at Large Parameters states that there is a threshold k0 such that the standard sine map fk(x,y) = (x + y + k sin 2πx, y + k sin 2πx) on the torus has positive metric entropy with respect to normalized area for every k ≥ k0; equivalently, its largest Lyapunov exponent is positive on a set of positive area. The parameter set therefore contains a whole tail, and the manuscript states that this resolves Sinai's conjecture in the formulation of Berger and Turaev. A corollary gives a positive-area ergodic component on which the map is nonuniformly hyperbolic and which splits into finitely many cyclic pieces, each Bernoulli under the corresponding iterate. The manuscript states that it makes no claim of ergodicity, almost-everywhere positive exponents or a uniform lower bound on entropy.
- Method, as described: the proof tracks the expected shortfall of derivative growth from its maximal rate along orbit segments. A cancellation theorem bounds the probability that two long segments grow nearly maximally while their concatenation almost completely cancels, through a scarcity estimate for small linearized solutions. A bridge theorem gives a weighted product estimate for observations near the two ends of a rapidly growing segment, built from transverse contracting graph families. The entropy conclusion then follows from Pesin's entropy formula.
- Source (openai/math repository, commit
7ef5c0c): Positive Metric Entropy for the Standard Map at Large Parameters, dated 23 September 2026. - Formalization, as described by the repository. The scope note lean/docs/146.md states that the formalization proves positive metric entropy for every sufficiently large parameter, positive largest Lyapunov exponent on a set of positive area with the stated derivative-growth limit, and a positive-area invariant ergodic hyperbolic component splitting into finitely many Bernoulli cyclic pieces, with no genericity assumption on the parameter. The Comparator statements are
StandardMapEntropy.lean,StandardMapLyapunov.leanandStandardMapComponents.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Positive metric entropy for the standard map at large parameters, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the standard map and its invariant area, entropy and Lyapunov exponents, why large derivatives alone do not settle the problem, cancellation scarcity and fast bridges, the contradiction argument and the positive-area component, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-07 | O. Knill, Positive entropy for Standard Map by Open AI, Quantum Calculus blog | Comment | Knill, who writes that he worked on the problem for more than ten years, describes the solution, from what he had seen, as "just plain ugly". He notes that the behaviour for smaller parameters is still unknown and that the standard conjecture is the entropy lower bound log(c/2) in his normalization of the map. | Blog post of 7 October 2026, updated 10 October 2026. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the main Lean statement is the headline verbatim, a full parameter tail, and the Lyapunov and Bernoulli-component claims are also stated. It notes that metric entropy is a hand-made definition that agrees with the usual one for measure-preserving maps, which holds here, and records Comparator passes on cloud machines for the three statements on 8 October 2026. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K: StandardMapEntropy (run 38019899278), StandardMapLyapunov and StandardMapComponents (run 38040214623) | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept all three solutions, in 1364 s, 1358 s and 1892 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions lists none of the three statements, so they were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_425 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap and no minor notes. The reviewer read all sections and checked by hand the cancellation theorem and its matching and covering lemmas, the local scarcity estimates including the degenerate cases, and the bridge estimates; no code was run. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-16 | AI Proved What?, episode 146 Chaos with positive area?, remade version of 26 October 2026 | Reading (exposition) | Video explainer of the claim and its history. The episode states that the threshold k0 is never computed because the proof is by contradiction, that ergodicity, almost-everywhere positive exponents and a uniform entropy bound are not claimed, and that nothing is said about small or intermediate parameters. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 45 pages, dated September 23, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the theorem and its corollary in three statements, not run by the site. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
