Nonlinear Dynamicsformally

A guided ascent through nonlinear dynamics

Nonlinear dynamics,
made formal.

Begin with a trajectory you can picture. Finish with mathematics you can prove and Lean code you can run. Every rung of the climb is explained.

Start the ascent Open the notebook

The learning path

Trailhead frontier

We hold your hand at sea level, then climb all the way to the research ridge.

Each stage supplies the intuition, notation, examples, and proof architecture needed by the next. Specialists can jump ahead; first-time readers always have a route upward.

  1. 01
    Trailhead

    See the motion

    Phase portraits, equilibria, recurrence, and the physical question before the symbols arrive.

    intuition
  2. 02
    Base camp

    Build the language

    Metric spaces, measures, matrices, maps, flows, and the definitions that make dynamics exact.

    foundations
  3. 03
    The ridge

    Translate into Lean

    Types, structures, hypotheses, and small reusable lemmas assembled into checked arguments.

    formal proof
  4. 04
    High camp

    Enter random dynamics

    Random matrices, Gaussian ensembles, cocycles, Lyapunov exponents, and stochastic stability.

    advanced
  5. 05
    Research frontier

    Connect to quantum chaos

    Spectral statistics, the Gaussian unitary ensemble, form factors, and invariance at the edge of the map.

    frontier
Study the textbook layer Follow the proof as it grows
Formal systemLean 4.32.0
LibraryMathlib
Current focusMatrix laws -> GUE -> stability

Choose your reading mode

Follow the construction or study the foundations.

01 / evolving record

Development Notebook

Chronological entries pairing each Lean module with the physics, derivation, proof decisions, exact commands, and honest open questions behind it.

Trace the work 02 / stable reference

Knowledge Base

A connected textbook of definitions and long-form chapters, designed to take a curious beginner to specialist-level mathematics without skipping steps.

Build the foundation

The working chain

One phenomenon, four connected views.

  1. 01
    Physical picture

    What trajectories, equilibria, forcing, and instability mean in the modeled world.

  2. 02
    Mathematical statement

    The spaces, maps, flows, assumptions, and quantifiers that make the claim exact.

  3. 03
    Lean encoding

    The definitions and reusable interfaces that expose the right proof obligations.

  4. 04
    Checked artifact

    A theorem whose dependencies, remaining assumptions, and build command are inspectable.