Lean formalizations

Results of my articles formalized in Lean 4 with Mathlib and checked by the proof assistant. Each formalization has a page with the article’s statements, the browsable Lean code with its proof states, the axioms it uses, and the complete Lean project to verify it locally.

Density of polynomials whose Aron–Berner extensions attain their norms Verified A machine-checked proof, in Lean 4 with Mathlib, of the polynomial Lindenstrauss theorem: for every real or complex Banach space X and every n ≥ 1, the n-homogeneous polynomials whose Aron–Berner extensions attain their norms are dense, for scalar and for vector values. Density of polynomials whose Aron–Berner extensions attain their norms · arXiv:2610.18117v1 · v1 · 25 Oct 2026 · Lean 4 · Mathlib