#formal verification

David Bessis argues that the traditional theorem-proving economy is declining as automated proof assistants and formalization shift mathematics toward intuition and visualization. This essay critiques the system's obsession with theorem-proving priority while real progress often occurs outside that loop. This matters because it signals a transformation in how mathematics is practiced and valued, with AI and formal tools challenging the core incentive structure of academic mathematics. It could reshape priorities toward insight and understanding rather than pure theorem production. Bessis highlights that AI-written proofs in systems like Lean often fail to convey useful human insights, yet they are increasingly used. He contends that the intuitions gained from proving are more valuable than the proof itself.