Daniel Litt: AI will soon be superhuman at math, so the math PhD should be redefined around understanding rather than theorem output

The reconceptualization of a math PhD as becoming a world expert who can explain the topic until the examiners are satisfied is refreshing and I agree with it 100 percent. The rigorous defense is exactly where humans stay in the loop, and making the topic more open-ended and larger than a typical thesis makes sense because the old bottleneck was the researcher's own understanding.

In my country that is exactly how it is. You still need a thesis to defend, but it all comes down to the oral defense.

That is the most optimistic scenario. Access to the AI itself is a really hard problem that nobody has solved.

Why is Doctor of Philosophy the right certificate for becoming an expert in a topic? That is a radical departure from a PhD meaning you are qualified to produce new research. What you describe sounds more like a Masters.

Understanding any modern interesting piece of mathematics well enough to explain what makes it interesting, in an hour, is pretty rare. We delude ourselves about how well we understand problems and their solutions.

Another bottleneck is money. You have to pay the corporations that own the technology to do mathematics, and in that future there will never be another Ramanujan.

A rigorous defense is exactly how PhDs were awarded for hundreds of years. My BSc in Applied Physics in 1977 had a viva voce that was a substantial fraction of the final exam.

The more I read these posts about reforming math institutions because of AI, the more it looks like they need to die and start again from first principles. If math is really about spreading intuition and understanding, our institutions dropped the ball decades ago.

Agreed, the reevaluation AI is forcing on math is one the establishment could fruitfully have had a long time ago.

Great optimistic post in a sea of negativity, and it actually has suggestions. Think of the ancient Olympics: a weightlifter only won if he could lift the stone, then Archimedes builds something like an exoskeleton and any regular guy lifts twice as much as last year's athlete. Now you have to give the prize on other factors, like how well he lifts or whether he opened a gym in the city.

In coding we already cannot independently validate all AI results, and math is worse because proof validation takes months or years. Millennium problems need two years of validity after publication, which is basically infinity at AI output rates. We will end up with frontier problems articulated and proven by AI from AI results, and humans unable to understand the solution at all.

I don't think that is the real problem. Autoformalization has improved astonishingly, and every recent AI discovery came with a Lean proof. The kernel has had soundness bugs and may still have some, but it is strong evidence, and the real concern among mathematicians is that human understanding gets devalued.

AI is also great at hierarchical summarization. I do ELI5, then explain like I'm a high school student, then a bright undergrad, then a working professional in the domain, and it works. We could use that to understand AI proofs better than we understand human ones today.

With formalized math you only need to validate the problem statement. Agents have already exploited Lean compiler bugs, but those should get rare enough for blind validation of AI proofs soon.

I think it is the opposite. Lean proofs and autoformalization let you ship a proof with a certificate of its own correctness, which gives the result immediate credibility. Combining superhuman informal reasoning with superhuman autoformalization is a fundamental shakeup of the institutional order.