OpenAI claim summary for Math-336

Sinai's Positive Metric Entropy Conjecture for the Chirikov Standard Map

OpenAI's claim

For every sufficiently large positive parameter, the torus standard sine map is claimed to have positive entropy for normalized area, giving a full parameter tail. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

On $\mathbb T^2=\mathbb R^2/\mathbb Z^2$ with normalized Lebesgue area $m$, define the standard map \[ f_k(x,y)=(x+y+k\sin(2\pi x),\ y+k\sin(2\pi x))\pmod{\mathbb Z^2}. \] OpenAI claims some $k_0>0$ with $h_m(f_k)>0$ for every real $k\ge k_0$. The entropy is Kolmogorov--Sinai entropy for the fixed invariant area measure; equivalently the largest Lyapunov exponent takes positive values on a subset with area greater than zero. This is not only a topological-entropy or zero-area hyperbolic-set assertion.

Outline of the argument

Manuscript 1 (family 146, 2026-09-23): Logarithmic matrix-product growth is treated as a stationary time semimetric whose expected shortfall is monitored across scales. Transverse graph families from finite Dirichlet problems give a weighted product estimate across fast bridges without assuming independent orbit segments; the multiscale argument forces positive average derivative growth.

Formal verification

For family 146, the scope page documents the following selections. Selections include positive entropy throughout a sufficiently large parameter tail, positive Lyapunov growth on positive area, and a hyperbolic ergodic component with finitely many cyclic Bernoulli pieces. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: StandardMapComponents.lean, StandardMapEntropy.lean, StandardMapLyapunov.lean. Declarations: OAI.StandardMapEntropy.main_components, OAI.StandardMapEntropy.main_entropy, OAI.StandardMapEntropy.main_entropy_complete.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

• OpenAI, Positive Metric Entropy for the Standard Map at Large Parameters, 2026-09-23; citation key OAI:Positive-Metric-Entropy-for-the-Standard-Map-at-Large-Parameters-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: main:entropy.
• Family 146: Lean scope.
• Comparator StandardMapComponents.json.
• Comparator StandardMapComponents.lean.
• Comparator StandardMapEntropy.json.
• Comparator StandardMapEntropy.lean.
• Comparator StandardMapLyapunov.json.
• Comparator StandardMapLyapunov.lean.
• OpenAI catalogue entry.