The paradigm of mathematical proof is shifting from solitary genius to collaborative software engineering. AI and formalization are turning proofs into blueprints that can be crowdsourced.
Podcast: A 4-hour Interview with Carina Hong: AI for Math, Lean, Proofs from The Book, and Intuition
The romantic image of math is a lonely genius solving a centuries-old problem at a chalkboard for 10 years.
But today, that image is quietly being replaced.
Modern proofs are increasingly broken down into massive, formalized projects. Terence Tao and Alex Kontorovich have started decomposing big theorems into "blueprints" that cut the proof into hundreds of smaller, well-defined tasks that anyone in the world can pick up and contribute to.
Carina Hong says proof now resembles collaborative software engineering more than solitary insight.
This is powered by formal verification languages like Lean. Through the Curry-Howard correspondence, every mathematical proof can be mapped to a computer program.
Furthermore, AI approaches math proofs through a completely different philosophy. In a recent Putnam-style problem, a human solved a geometry question with a single elegant drawing. The AI produced thousands of lines of brute-force enumeration. Same answer, but completely different method.
Therefore, the future role of the mathematician will likely rely less on mechanical labor and more on elite intuition about which conjectures to pursue and where to direct the AI's computing power.