The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math (w/ Kevin Hartnett)