Internal Projectivity of the Sequence Space in Lean

Abstract: The theory of condensed mathematics has been well-explored in formalized mathematics. In my master thesis, I proved that the sequence space, a condensed Abelian group describing null-sequences, is internally projective in the category of light condensed abelian groups. I will discuss the proof, and what it is like for a relative beginner to prove a non-trivial theorem in Lean.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2026