01Source claims
Shared formal graph · reader view
Proof Atlas
See the mathematical structure before the code. Source claims from the textbook and SampleWiki meet in shared proof roots; exact Lean declarations are the final zoom level, not the first.
02Mathematical proof nodes
Definitions, lemmas, proof techniques, and theorem interfaces. Repeated ideas are shared rather than copied into every chapter or example case.
03Exact Lean nodes
Open a theorem card only when you need the precise type, hypotheses, imports, dependencies, consumers, source location, and test evidence.
Chapter 1 shared spine
Four clusters, not one giant DAG.
Stochastic calculus
Brownian motion → adapted/progressive processes → Itô integral → stopping/localization → Itô processes.
Semigroups & inequalities
Transition kernels → semigroup → generator → reversibility/Γ → Poincaré and log-Sobolev dissipation.
Optimal transport
Couplings → transport cost → W₂ → interpolation/geodesics → geodesic convexity.
Gradient flow & algorithms
KL/Fisher dissipation and Wasserstein geometry feed convergence proofs, discretizations, complexity results, and SampleWiki cases.
Status semantics
Color the node that was actually proved.
compiled local nodeopen analytic bridgesource / reference node
A chapter is not blue because one leaf compiled. A SampleWiki row is not assimilated because a theorem-shaped Lean statement elaborates. Status follows the exact node and its verification gate.
Where did the old “Lean Foundations” packet go?
The cutoff-to-generator packet is still available through the formal library. It is now treated as one implementation example rather than the default mental model for the whole project.