Terence Tao: A few weeks ago, AI crossed the critical threshold of mathematical formalization

The "most powerful brains" in the mathematical community are being inundated with proofs generated by AI.

Terence Tao, a Fields Medalist, shared his latest experience in the IEANTN project (Integrated Explicit Analytic Number Theory Network):

AI can generate correct proofs at an incredibly fast pace, but the proofs are so verbose that humans simply don't have the time to review them.

Formalization tasks that used to take volunteers weeks to complete a few weeks ago can now be finished by AI in just a few hours.

A phenomenon that was noticed by the 17th - century mathematician Pascal is now plaguing contemporary mathematics in a brand - new way:

It is easier to generate a long, correct proof than a short, correct one.

Terence Tao calls this phenomenon "impedance mismatch," and AI has taken this contradiction to the extreme.

From weeks to hours

The IEANTN project led by Terence Tao aims to formalize a large number of technical papers in explicit analytic number theory and build a living, dynamically updatable network of number - theoretic estimates in the Lean proof assistant.

This work involves a large amount of tedious numerical verification and parameter matching.

In Terence Tao's own words, this kind of work takes up at least 70% of his time when thinking about analytic number theory problems.

Using the traditional method, he would break down individual lemmas into independent tasks and post them, then wait for volunteers to claim them - usually for several weeks.

Due to the difficulty of manual formalization, volunteers naturally pursue short, efficient, and natural proofs, and the submitted code is easy to review.

But in recent weeks, the automatic formalization technology has suddenly crossed a certain critical point.

Almost every formalization task posted by Terence Tao can be completed by AI tools within a few hours.

The queue of unresolved issues waiting to be claimed in the project has been basically cleared.

AI can do local optimization but not global reconstruction

The leap in speed has brought unexpected side effects.

The formalized proofs generated by AI are often hundreds of lines longer than those written by humans, containing a large number of redundant steps, and many lemmas are not stated at an appropriate level of abstraction.

Looking at any single proof, it doesn't seem to be a big problem, because these proofs are not meant to be read by humans.

But each verbose proof adds dozens of seconds to the total project build time, and the cumulative effect cannot be ignored.

Terence Tao calls this "impedance mismatch": the speed gap between the three stages of proof generation, proof verification, and proof digestion is widening.

The generation end has been accelerated by several orders of magnitude by AI, but the verification and digestion ends still rely on human cognitive bandwidth.

In practice, transforming a medium - sized Lean document containing thousands of lines of code (partially generated by AI) into an elegantly structured version suitable for submission to the Mathlib mathematical library has become a challenging task.

Terence Tao has discovered a clear boundary for current AI tools.

AI can handle local "code golf" (code reduction) and can compress the size of the proof to some extent.

But global reconstruction decisions are completely beyond the capabilities of existing AI tools.

For example, if a certain argument appears repeatedly in a document, it can be abstracted into an independent lemma, and this lemma may have broader applications outside the current file.

Terence Tao points out that he can explain such a reconstruction scheme to AI, and AI can then execute it, but AI cannot spontaneously discover such reconstruction opportunities.

AI is good at handling local, atomized tasks but lacks an understanding of the global structure of the project. In the context of the IEANTN project, this means that AI can quickly generate proofs for individual lemmas but cannot determine how these lemmas should be embedded in the architecture of the entire number - theoretic estimation network.

The project is progressing much faster than expected.

But Terence Tao said that he now needs to spend more time planning the scope of formalization tasks in advance. Since he anticipates that AI will quickly return a proof, he needs to consider how to make the results easier to review and more compatible with the global structure of the project when posting tasks.

In other words, the bottleneck has shifted from "waiting for people to do the proofs" to "designing tasks so that the output of AI can be effectively integrated." The role of mathematicians is shifting from performing proofs themselves to becoming architects of proof engineering.

To achieve this vision, every piece of the puzzle must exist in the system at the correct level of abstraction and with the correct interface standards. AI can produce puzzle pieces at an amazing speed, but only humans can currently judge whether the shape of these puzzle pieces matches the overall blueprint.

Reference links:

[1]https://mathstodon.xyz/@tao/116789374373843141

[2]https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/

This article is from the WeChat official account "QbitAI". Author: Meng Chen. Republished by 36Kr with permission.