In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far? (quantamagazine.org)

The piece argues that while formalizing proofs in systems like Lean can strengthen mathematical certainty, it may also risk shifting effort away from intuition-driven discovery and making math less flexible or elegant.