Think of it like this: A brilliant architect designs a building with innovative structural concepts. Engineers then verify that the design won't collapse, calculating loads, stresses, and safety factors. The verification is essential, but it's not where the creative insight happens.

Kevin Han and Vishnu Hariharan from Math, Inc. emphasize that this is a collaborative achievement. Humans laid the foundational theory, identified what needed to be proven, and developed the mathematical concepts. The AI handled the mechanical process of translating informal mathematics into formal logical statements.

This matters because it points to what AI is actually good at: tasks that are well-defined, mechanical, and labor-intensive. Formal verification fits that description perfectly. Every step follows precise rules, the goal is clear, and the work is tedious but not conceptually difficult.

Where AI struggles—and likely will continue to struggle—is with mathematical creativity. Coming up with novel proof strategies, seeing unexpected connections between fields, formulating interesting conjectures. These require intuition, taste, and the kind of non-linear thinking that humans excel at.

The 8-dimensional case was formalized first, serving as a blueprint. The 24-dimensional case was more involved, requiring substantial work on properties of the Leech lattice and its uniqueness. But the AI could leverage commonalities in the foundational theory and overall architecture.

This is exactly the AI future we should want. Not AI replacing human expertise, but AI handling the parts of intellectual work that are mechanical and time-consuming, freeing humans to focus on creative problem-solving.

In mathematics, this could accelerate the field dramatically. Proof verification currently bottlenecks progress—mathematicians spend enormous time checking work, and subtle errors can go undetected for years. AI that can rapidly verify proofs means mathematicians can take more risks, try bolder ideas, and trust that verification will catch mistakes.

This applies beyond mathematics. In software engineering, AI can handle boilerplate code while engineers focus on architecture. In scientific research, AI can process data while scientists develop hypotheses. In law, AI can review documents while lawyers strategize.

The pattern is consistent: AI handles scale and tedium, humans handle creativity and judgment. That's not a future where AI replaces humans—it's a future where humans are empowered to do more ambitious work because AI handles the mechanical parts.

Maryna Viazovska's Fields Medal proof is now formally verified, thanks to AI. But she's still the one who proved it. The AI just checked her work—really, really thoroughly.

4 days ago