From Zero to QED: An informal introduction to formality in Lean 4