Lean 4 proof formalization for Learning Real Analysis

Notes, proofs, Nurbs, and Lean

NURBS/DDE Brownian motion pursuit simulation on the torus — C++, Vulkan, delay-differential equations.

Volume VI of Learning Real Analysis: Calculus, ODEs, Fourier analysis, geometric modeling, and computational linear algebra.

Theorem knowledge explorer — LaTeX extraction pipeline and interactive HTML graph

Volume IV of Learning Real Analysis: Abstract algebra, linear algebra, lattice theory, category theory, and algebraic structures.

Volume VII of Learning Real Analysis: Numerical analysis and approximation theory.

Volume VIII of Learning Real Analysis: Model theory, type theory, lambda calculus, and foundations of computation.

Shared LaTeX infrastructure for Learning Real Analysis (macros, preambles, bibliography, images)

Volume I of Learning Real Analysis: Logic, sets, and the foundations of proof.

Governance rules, architecture docs, sync policy, and agent instruction generators for the LRA ecosystem.

Published PDF outputs for Learning Real Analysis volumes

Volume II of Learning Real Analysis: Peano systems and rigorous construction of N, Z, Q, R, and C.

Volume III of Learning Real Analysis: Real analysis, sequences, continuity, differentiation, integration, and measure theory.

Volume V of Learning Real Analysis: Topology, metric spaces, differential geometry, and Riemannian geometry.