New preprint out!Mar 17, 2026Synthetic Differential Geometry in Lean, with Gabriella Clemente. To appear in the Annals of Formalized Mathematics.