Dynamical systems and ergodic theory

The Lean Pool projects whose card's first MSC2020 code is in class 37, Dynamical systems and ergodic theory: 4 articles, one per card.

TheoremAnalytic Hamiltonian KAM on compact action domains#

Proves a nondegenerate analytic Hamiltonian KAM theorem on compact complex action domains whose real slice is the closure of a nonempty open set with null boundary. A positive perturbation threshold, chosen independently of the perturbation, yields a pairwise disjoint family of analytic invariant tori covering all but a prescribed relative measure error. Includes Fourier estimates, generating transformations, resonance measure bounds, infinite iteration, global Hamiltonian trajectories, and examples with a noninjective frequency map. The final torus interface asserts nonresonance but does not additionally assert a quantitative Diophantine bound or the Lagrangian property.

Quoted from the card LeanPool/projects/arnold-kam.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanKamProject.Arnold1963.theorem1

TheoremChaos and the Julia set of the complex exponential#

Formalizes the dynamics of z ↦ exp(z): escaping points, points with dense forward orbit, and repelling periodic points are dense in the complex plane; the map is chaotic in Devaney's sense and its Julia set is the whole plane. The development proves eventual covering of every compact set omitting zero, constructs contracting inverse branches, and rules out every locally uniform spherical subsequential limit on nonempty open sets. It includes general normal-sequence restriction lemmas, quantitative open mapping, and a two-target obstruction for arbitrary separated uniform codomains. The Lean proofs were primarily generated by AI under Lasse Rempe's direction. The initial six-lemma architecture adapts John Harrison's HOL Light formalization, credited with its retained BSD notice in the entry module.

Quoted from the card LeanPool/projects/exponential-chaos.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 7 main results, each with its informal statement quoted from the card. The scan finds 7 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanExpChaotic.devaney_chaotic · ExpChaotic.juliaSet_exp

TheoremNivat's conjecture#

Formalizes the proof of Nivat's conjecture found by GPT-6 Pro. A configuration on the integer lattice over a finite alphabet whose number of distinct patterns on some m-by-n rectangle is at most m times n has a nonzero period. Develops rational alphabet labelings, the Laurent-polynomial shift action and its annihilator ideals, the exact line ideal of a half-plane-supported difference of orbit-closure points, complexity descent to a smaller rectangle, and Szabados's two-factor theorem for finite-range configurations.

Quoted from the card LeanPool/projects/nivat-conjecture.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • Nivat.nivat (theorem; a main declaration), declared in LeanPool/Nivat/Main.lean, line 133: “For every finite alphabet A and configuration c from the integer lattice to A, if for some positive m and n the number of distinct patterns of c on the m-by-n rectangle, counted over all integer translations, is at most m times n, then there is a nonzero lattice vector h with c(z + h) = c(z) for every z.”
  • NivatSubmission.nivat (theorem; a main declaration), declared in LeanPool/Nivat/Statement.lean, line 56: “The same statement written with Mathlib vocabulary only, as registered with Palomar. The pattern set is the range of the restriction of translates of c to the product of the integer intervals [0, m) and [0, n), its natural cardinality is at most m times n, and the conclusion is a lattice vector h different from (0, 0) with c(z + h) = c(z) for all z.”
  • Nivat.nivat_rational (theorem), declared in LeanPool/Nivat/Main.lean, line 95: “A finite-range rational-valued configuration whose pattern count on some m-by-n rectangle with m, n positive is at most m times n is periodic. This is proved by strong induction on the area of the rectangle.”
  • Nivat.two_factors (theorem), declared in LeanPool/Nivat/TwoFactors/Main.lean, line 240: “If a finite-range rational configuration has pattern count at most m times n on an m-by-n rectangle with m, n positive and is annihilated by the product of two difference operators in nonzero directions h and t, then it is periodic.”
  • Nivat.Descent.exists_smaller_low_complexity_rectangle (theorem), declared in LeanPool/Nivat/Descent/ExactDescent.lean, line 328: “If two pointwise limits x and y of translates of a finite-range rational configuration c have nonzero difference whose Laurent annihilator ideal is generated by a nonzero polynomial, and c has pattern count at most m times n on an m-by-n rectangle, then applying that polynomial to c yields a configuration with pattern count at most its area on some rectangle of strictly smaller positive area.”
  • Nivat.Algebra.exact_line_in_basis (theorem), declared in LeanPool/Nivat/Algebra/ExactLine.lean, line 559: “A nonzero rational configuration that vanishes on the open lower half-plane of a lattice basis and is periodic with positive period q along the first basis direction has Laurent annihilator ideal generated by a single line-supported polynomial, obtained from a monic divisor of X^q - 1 of positive degree.”
Project
  • Authors: Boon Suan Ho.
  • Source: Pattern complexity and Nivat's conjecture by GPT-6 Pro, Boon Suan Ho.
  • The card's note on its source: “The proof and manuscript were produced by GPT-6 Pro and the Lean development by GPT-6 Astra in Codex, both prompted and directed by Boon Suan Ho, who claims no human mathematical authorship. The manuscript ships in the upstream repository as paper/nivat.tex. The Lean sources are identical to the commit archived by Palomar on 2026-09-14 (0d94547e); later upstream commits only touched the README and the paper's abstract. No human expert review is claimed upstream; Bryna Kra's guest post on Terence Tao's blog (2026-09-13) discusses the arrival of AI proofs of the conjecture. The upstream MIT copyright and permission notice is retained in every imported file.”
  • Project repository: boonsuan/nivat, at commit 84fe8396.
  • Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
  • License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
  • MSC2020: 37B10, 37B51, 68R15.
  • In Lean Pool: LeanPool/Nivat, from the card LeanPool/projects/nivat-conjecture.yaml.
Sources
LeanNivat.nivat · NivatSubmission.nivat

TheoremPointwise Birkhoff Ergodic Theorem#

Formalizes the pointwise Birkhoff ergodic theorem for integrable real-valued observables.

Quoted from the card LeanPool/projects/pointwise-birkhoff.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLeanPool.PointwiseBirkhoff.birkhoffErgodicTheorem'

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.