What is Lean?
A formalization states definitions and theorems in the dependent type theory of Lean 4 and gives their proofs as terms of that theory. Whether such a term is a proof is decided by a small kernel that rechecks every step, and the axioms a finished proof relies on can be listed exactly. Mathlib, the community library, supplies the underlying analysis, linear algebra and topology basics, and is extended over time.
Projects on GitHub
A blueprint is a readable account of the mathematics with links into the Lean code,
and its dependency graph shows which results rest on which.
s-Numbers of operators (Lean-SNumbers)
Blueprint (as pdf)·Dependency graph
Pietsch's axiomatic theory of s-numbers, which takes the place of the singular values on Banach spaces, where no spectral theorem is at hand. The development covers the axioms, the five classical sequences (the approximation numbers \(a_n\), the Bernstein, Gelfand and Kolmogorov numbers, and the Hilbert numbers \(h_n\)) and the inequalities between them. Its main result is the maximal difference theorem \(a_n(S)\le e(n+1)\,h_n(S)\). Since \(a_n\) is the largest s-number sequence and \(h_n\) the smallest, this single factor bounds the gap between any two of them, and its growth in \(n\) is order-optimal.
Getting there called for a good deal of general functional analysis that Mathlib does not yet carry: Auerbach's lemma, John's ellipsoid together with the decomposition of the identity, the singular value decomposition of a compact operator, the Eckart–Young theorem, and the projection theorems of Kadets–Snobar and Garling–Gordon.
About 17,500 lines against Lean 4.33.0, with no sorry left in the library. A blueprint pairs every Lean declaration with its mathematical statement and draws the dependency graph.
Palomar-registered results
Palomar is a public registry of Lean formalizations. It re-runs the proof itself at one pinned commit of the repository and records the outcome, down to the axioms the proof rests on.
The maximal difference theorem for s-numbers
SNumbers.approximationNumber_le_mul_hilbertNumber\(a_n(S)\le \frac{(n+1)^{n+1}}{n^{n}}\,h_n(S)\)SNumbers.approximationNumber_le_e_mul_hilbertNumber\(a_n(S)\le e\,(n+1)\,h_n(S)\)