∑math20

Dynamical systems and ergodic theory · Result 146

Positive metric entropy for the standard map

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Positive Metric Entropy for the Standard Map at Large Parameters

Positive Metric Entropy for the Standard Map at Large Parameters

OpenAI · September 23, 2026

We prove that the standard sine map of the two-dimensional torus has positive metric entropy with respect to normalized area for every sufficiently large positive parameter. This gives a full parameter tail, and hence answers Sinai's positive-parameter-measure conjecture affirmatively.

Read PDF Download Source

Cite
@misc{OAI:Positive-Metric-Entropy-for-the-Standard-Map-at-Large-Parameters-September-23-2026,
  author = {{OpenAI}},
  title = {{Positive Metric Entropy for the Standard Map at Large Parameters}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Positive-Metric-Entropy-for-the-Standard-Map-at-Large-Parameters-September-23-2026/paper.pdf}{OAI:Positive-Metric-Entropy-for-the-Standard-Map-at-Large-Parameters-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

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.

Comparator links

ResultComparator statement
Positive-area hyperbolic Bernoulli componentStandardMapComponents.lean
Positive metric entropy for all sufficiently large parametersStandardMapEntropy.lean
Positive Lyapunov exponents and entropyStandardMapLyapunov.lean

Scope note on GitHub →