Terence Tao asks what mathematics should value when AI can do research-level work

I think the Hitchhiker's Guide had the right warning: the hard part is often asking a well-defined question, not getting an answer.

I still print short papers before reading. I understand and edit text much better on paper than on a screen.

I think avoiding AI will put people at a major career disadvantage. It can already find deep references better than I can, and the real constraint becomes choosing problems that fit a token budget, say $10k.

Tao's complaint about AI proofs applies to AI writing too. It spends lots of words on trivialities and rushes past the novel part.

That happens in ordinary proofs as well. People can explain every mechanical step without ever explaining why the proof works.

I like Tao's rule that authors should be able to give a clear, correct, properly attributed expert talk on a result. Formal verification alone does not make a proof intellectually complete for human readers.

I am not sure that rule handles computer-assisted work like the four-color theorem. Lean-verified proofs may become too long for anyone to properly explain, but discarding them seems wrong.

The incentive problem is real. If publishing a formally verified result gets the reward, nobody has much reason to spend years making it comprehensible, and digesting someone else's proof will not win tenure or a Fields Medal.

Chess engines are a useful comparison. Grandmasters can say an engine line is good without explaining why, yet people still treat it as ground truth; formally verified math may end up similarly opaque.

I think any standard that requires a human in the loop merely because they are human is anti-scientific. Science cares about results and falsifiability, not who can narrate every step.

I expect superhuman reasoning plus scalable formal verification to push much of mathematics beyond immediate human understanding within our lifetimes. We should explain the parts humans benefit from understanding, not demand explanations for all of it.

Journals already cannot keep up with review. Making journals do far more work per AI-generated paper seems impractical, though explainability might make more sense as a hiring criterion.

For programmers too, the job is still being able to answer, from memory, how the system works and why.

If someone produced a proof that P equals NP but could not explain it, I would still consider the result immensely valuable.

A counterexample that kills a conjecture also seems publication-worthy even if its derivation is opaque.

There may soon be more formally verified proofs than all mathematicians can read, let alone explain. Then mathematicians may become explainers of AI-generated results.

Tao is stating what he values as a human mathematician. As a consumer of results, I may only need confidence that a claim was proved by someone or some machine.