From Zero to QED: An informal introduction to formality with Lean 4 December 13, 2025 by kamal Comments