Mathematicians are debating the value and risks of formalizing all of mathematics using the proof assistant Lean, which has already verified over 260,000 theorems. Drawing on historical parallels — from the rigorization of calculus by Cauchy and Weierstrass to the austere Bourbaki movement — the piece explores how formalization can both strengthen and constrain mathematical progress. Lean's modular, verifiable approach offers benefits like catching errors and enabling AI integration, but critics worry it could homogenize mathematical culture, favor certain subfields over others, and subtly shift what questions mathematicians pursue. The historical lesson is that formalization works best when it arises organically to solve specific problems, not as a top-down mandate.
Sort: