Теренс Тао о будущем ИИ в математике | Теренс Тао и Лекс Фридман

Summary

Lean and formal proof

• Lean is both a programming language and a proof assistant. Unlike ordinary code, which mainly performs actions or computes answers, Lean can produce a machine-checkable proof showing why a statement follows.
• A proof is built from earlier statements in small steps. Lean checks that each step is justified, relying on a compact trusted core rather than asking an AI model to decide whether a proof is valid.
• Formalizing mathematics is demanding: Lean requires details that mathematicians often leave implicit on paper, such as the type of an object or why a particular step is valid. Automation helps, and AI-based autocomplete can sometimes suggest the right lemma or next step, though it is often wrong.
• The library Mathlib contains a large collection of formalized mathematical results. Finding the right existing lemma is a common challenge; search tools and language models can help.
• Tao estimates that formalizing a proof currently takes substantially longer than writing it informally. But formalization can make later revisions easier: when a theorem’s constant or assumptions change, Lean identifies which steps break instead of requiring the entire proof to be checked manually.
• Formal proofs can also be easier to navigate and collaborate on. Lean exposes the context behind a line of proof, and collaborators can discuss a precise, failing step. Its checks provide a strong guarantee that a contribution is mathematically valid.

Collaboration and large-scale mathematics

• Tao describes mathematical research as beginning with brainstorming and exploration, not simply dividing up a known implementation task. Researchers test ambitious or imperfect ideas, adjust assumptions, and look for smaller subproblems that can be solved.
• Successful collaboration often depends on matching complementary expertise and negotiating assumptions that are both provable and useful. Tao illustrates this with his work with Ben Green on what became the Green–Tao theorem.
• Lean could eventually let large teams work on separate, independently checkable parts of a proof. For now, formalization is more often used to verify mathematics already established informally, since papers may omit details Lean requires.
• Tao describes a large project examining roughly 22 million pairs of possible algebraic laws derived from about 4,000 candidate laws. For each pair, participants determine whether one law follows from another, supplying either a proof or a counterexample. Lean makes it feasible to combine and verify work at this scale; the project was close to completion, with two tasks still remaining at the time of the conversation.
• Project records can help document contributions, but Tao cautions against treating line counts or other crude metrics as measures of research value. The project instead uses participant-reported contributions across a set of categories. He also notes that metrics can distort behavior when people are rewarded for optimizing them—a version of Goodhart’s law.
• Large collaborative projects need fair recognition. Tao contrasts an earlier crowdsourced project published under the collective pseudonym “D. J. Polymath,” which made it difficult for contributors to claim authorship, with the newer approach of listing all coauthors and documenting their roles.

What AI can—and cannot—do in mathematics

• AI systems have demonstrated impressive results on difficult school-level problems, but Tao warns that these results do not yet scale reliably. Proof search becomes harder as the number of steps grows, and even a modest chance of error at each step makes a long proof unlikely to be correct end to end.
• Translating ordinary mathematical language into formal code is also difficult. Informal writing tolerates ambiguity and small errors; formal systems do not, and translation between different proof languages remains challenging.
• AI is especially promising for well-defined tasks with clear outcomes, such as numerical answers or routine calculations. Long proofs are harder to evaluate automatically: reinforcement-learning systems need reliable feedback, and checking mathematical proofs at scale can be expensive.
• Tao’s central distinction is between producing plausible-looking work and having mathematical judgment. AI can generate arguments that appear polished but contain subtle, serious errors. Human mathematicians are better at recognizing when an approach is promising, when a problem has been made harder rather than simpler, and when something has the “smell” of bad mathematics.
• He sees a productive future in human–AI collaboration: AI could help with calculations, coding, literature searches, proof suggestions, and exploring alternatives, while people assess the ideas and verify the results. Current systems can be useful but unreliable enough that supervising and correcting them may take more effort than doing the work oneself.
• Better formalization tools and dependable literature search could trigger a major change. If writing formal proofs becomes nearly as convenient as writing informal ones, papers could include machine-verified proofs, potentially easing some burdens on peer review.
• Tao predicts that AI-assisted mathematical research could produce genuine coauthored scientific work in the near future, even if the AI contributes only part of the calculations, testing, or exploration. He also suggests that, within this decade, AI may be able to propose a significant and plausible mathematical hypothesis connecting ideas that are not obviously related.
• A major obstacle to training better research systems is missing data. Mathematics records successful results, but rarely preserves promising-looking hypotheses that failed, the mistakes researchers made, or how they learned to repair those ideas. Tao argues that AI would benefit from something like the full experience of graduate education—including unsuccessful attempts, feedback, and correction.

Speakers and sources featured

Speakers

• Terence Tao — mathematician and guest.
• Lex Fridman — interviewer.

Systems, projects, and references discussed

• Lean and Mathlib — proof assistant and mathematical library.
• GitHub Copilot — cited as an example of AI-assisted proof autocomplete.
• AlphaProof and AlphaZero — discussed in connection with AI proof solving and strategic intuition.
• Green–Tao theorem and Szemerédi’s theorem — referenced in Tao’s account of collaboration with Ben Green.
• Polymath / “D. J. Polymath” — an example of crowdsourced mathematics and collective authorship.
• LaTeX — cited as an example of a tool that became widely adopted after reaching a usability tipping point.
• Tim Gowers — mentioned for an earlier vision of interactive mathematical assistants.