A book on modeling mathematical objects in Lean 4 and proving their properties.