Terence Tao at the International Congress of Mathematicians: AI is creating more proofs than mathematicians can absorb

Terence Tao at the International Congress of Mathematicians: AI is creating more proofs than mathematicians can absorb

On July 24, mathematician Terence Tao gave a lecture at the International Congress of Mathematicians on how AI is changing the way mathematicians work with proofs. He predicts that machines will increasingly be able to propose or formally verify proofs, while people will need to understand what those proofs mean and how they fit into the broader theory.

Tao divides the work involved in establishing a mathematical result into three parts. First, someone develops a chain of reasoning. Next, someone checks every step. Finally, mathematicians determine why the argument works, how it relates to other theorems, and what further problems follow from it. Tao calls this final step proof digestion.

AI accelerates the first part, while formal systems such as Lean help with the second. A mathematician writes the proof in a formal language, and the computer checks each logical inference. Other mathematicians still need to identify the central technique, understand the conditions under which it works, and connect it with established results.

In his lecture, Tao describes how this work unfolds over time. New results await verification, verified results await clear exposition, and published results await incorporation into textbooks and the research of other groups. For this final step, the author and reviewer must understand the proof well enough to use it in further work.

Tao predicts that AI will increase the flow of mathematical answers faster than people can digest them. The person who produces a long derivation is therefore not the only one creating value. Value also comes from identifying the useful technique within that derivation and explaining it to others. In a summary that he reviewed, Tao describes digestion as understanding a result, placing it in context, and explaining it.

On July 25, Tao published the lecture slides and said that he had asked AI to compile his previous public statements about AI, after which he reviewed and corrected the resulting overview himself.