Glitnir notebooks.
Lean notebooks on circuits, dynamical systems and partial differential equations.
Examples using Lean, Mathlib, Forseti and Asgard. Read the mathematics and follow the proofs.
Start here
Small models introduce claims, saved evidence and refutations.
Circuits
Composition, contracts, rewrites and discrete dynamics.
Dynamical systems
Continuous trajectories and their bounds.
Finance
A hedged book bounded under every shock in a band, and bounds on the odds of its stop under random shocks, all as theorems.
Galerkin models
Finite-dimensional fluid models, energy and enstrophy.
- A 12-mode truncation of Navier–Stokes: the energy stays in its ball
- A 5-mode truncation of Navier–Stokes: the energy stays in its ball, then below its laminar level
- A 3-mode truncation of Navier–Stokes at small forcing: the laminar line attracts
- A 3-mode truncation of Navier–Stokes: the energy stays in its ball
Partial differential equations
Stream contracts, formal expansions and analytic certificates.
- Burgers: from a unique formal stream to a certified front
- Two more Burgers fronts: certificates, counterexamples and open requests
- The Euler equations of a frictionless fluid, solved exactly as a power series in time: one solution, a certified radius, and how far it is from sharp
- Navier–Stokes through a typed mild circuit