In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far?
Summary
The article surveys the long arc of mathematical rigor, from Euclid to Bourbaki, and examines the push to formalize proofs in computer language Lean. It discusses the benefits and risks of digitizing proofs, including potential gains in reliability and new discoveries, but also concerns about homogenization and the possible impact on mathematical creativity. The piece highlights real-world efforts, funding, and examples where AI-assisted formalization could play a growing role, while arguing for a balanced, plural approach to proof and discovery.