In Math 2.0, Terence Tao considers a mathematical landscape in which AI and formal tools make proofs more abundant. He also stresses uneven capabilities and continuing difficulties at the research frontier. His ambition goes beyond solving problems: these tools should enrich understanding. These are the perspectives of a lecture, rather than an independent performance measurement. [1]
A proof of what?
Lean lets users construct proofs that its kernel checks against formal statements, definitions and explicit axioms. Finding a proof and checking it are distinct tasks. However, checking a formal statement does not establish that the statement faithfully expresses the question we meant to ask. [2]
That last distinction deserves attention. An answer may read convincingly; a demonstration may be correct; the result may still fail to apply to the case that interests us. Three things therefore need examination: the explanation, the proof, and the translation of our problem into mathematics. None of these stages makes the other two unnecessary. Their relationship matters as much as the correctness of each individual step.
What an average can teach us
Take an elementary example offered here, without claiming to have formalised it in Lean. A weighted mean lies between the smallest and largest values when its weights are non-negative and their sum is strictly positive. The statement feels almost too familiar to warrant examining its conditions. Its apparent obviousness is precisely what makes it a useful example.
Now remove the sign condition. With values 0 and 10, and weights −1 and 2, the mean is (−1 × 0 + 2 × 10) / (−1 + 2), which gives 20. It falls outside the interval [0, 10]. The calculation fits on one line; it explains exactly why the assumption about the weights mattered.
A correct proof of the first statement would therefore not justify using it with negative coefficients. Equally, a proof of a statement made trivial by an excessively restrictive definition would tell us little about the original problem. Before admiring an answer, we need to inspect the precise question it answers. A successful calculation is useful only within the conditions that make it relevant.
An instrument for asking questions
One promising use to explore would be to request several complementary outputs: a precise statement, an explanation, boundary cases, and counterexamples to false variants. Such requests provide no automatic guarantee. They do make the work inspectable: we can identify a hidden assumption, repeat a calculation, and locate the point at which an argument stops working. This is a practical way to expose gaps that fluent prose can otherwise conceal.
When reading an AI-assisted result, I would keep a few simple questions in view:
- Which question was actually resolved?
- Which assumptions are indispensable, and what example tests them?
- What was checked, and by whom or by which tool?
- What do we understand better after reading the proof?
The aim would not be to replace intuition with an approval stamp. It would be to connect intuition, calculation and verification more carefully. A machine can help traverse possible paths; the reader still needs to understand what makes one path fruitful. The number of proofs produced would then tell us less than the quality of the questions that have become approachable.
That is the reading of Math 2.0 proposed here: assess these tools by what they let us ask, check and explain. The example of the mean is tiny. Yet it preserves a requirement that remains as tools change: knowing exactly what we are claiming, and how far the claim reaches.