Terence Tao Discusses AI's Role in Expanding Mathematical Collaboration and Problem Solving

Mathematician and Fields Medalist Terence Tao stated that new technologies are disrupting traditional mathematical working methods, emphasizing that formal verification, rather than artificial intelligence alone, is key to this transformation. Speaking at the SAIR Foundation's "AI for Science: Kickoff 2026" event in February 2026, Tao highlighted how these advancements are enabling large-scale collaboration and addressing a vast number of mathematical problems previously beyond human capacity.

Six blackboards filled with complex mathematical equations in a sunlit office.

Tao, who maintains six blackboards in his office, recently led a project involving 50 individuals that solved 22 million mathematical problems using AI and code. He underscored that while mathematics has historically been a conservative discipline, new tools are fostering unprecedented levels of collaboration.

Mathematics' Conservative Nature and Collaboration Barriers

Tao began his lecture by referencing an 1826 mathematics textbook by Cauchy, noting its continued usability despite its age and French language. This continuity, he explained, demonstrates the enduring strength of mathematics but also its inherent conservatism. Mathematicians, he observed, are among the last academics to rely on blackboards and chalk, a detail captured in Jessica Wynne's photography collection, "Do Not Erase," which features blackboards from over 100 mathematicians, including Tao's.

Split image showing historical and modern mathematicians at blackboards, symbolizing continuity and change.

He presented data showing that while other scientific fields have seen an explosion in the average number of authors per paper, mathematics has only slowly increased from 1.5 to 2.5 collaborators. Tao attributed this not to a lack of social interaction among mathematicians, but to three structural barriers:

• High Barrier to Entry: Understanding complex mathematical problems often requires a Ph.D.

• Extreme Correctness Requirement: A single error in a crowdsourced proof can invalidate the entire result.

• Non-Scalable Workflow: Traditional methods, such as two or three people discussing at a blackboard, do not scale to large online collaborations.

Formal Verification as a "Secret Weapon"

Tao described a shift from a "case study" mode of research, where mathematicians tackle one problem at a time, to a "large-scale survey" mode that addresses hundreds or thousands of problems simultaneously. This new approach, he noted, also broadens participation, allowing for "citizen mathematics" akin to citizen science in other disciplines.

The "secret weapon" enabling this transformation, according to Tao, is formal verification. This computer language automatically checks the correctness of mathematical arguments, effectively "filtering out a lot of garbage." This capability directly addresses the issue of errors in collaborative proofs, as it removes the need to trust individual contributors and instead relies on the verification system. The proof assistant language Lean, developed by Microsoft Research, is a prominent tool in this area, offering real-time feedback during proof writing.

Abstract visualization of formal verification, showing data passing through a digital filter.

The Equational Theories Project: 22 Million Problems Solved

Tao detailed the Equational Theories Project, which he initiated at UCLA with 50 collaborators, many of whom he had not met previously. The project aimed to programmatically generate and solve 22 million algebraic implication problems. These problems involved determining if one algebraic property could be deduced from another.

The project, which launched on GitHub in September 2024 and saw its final paper uploaded to arXiv in December 2025, involved 22,028,942 pairs of implication relations between 4694 equational laws of magmas. While a single problem might take a graduate student an hour to solve, the project completed all 22 million problems, each with a proof or counterexample, in three months.

Key to its success were:

• Modularity: Problems were broken into subtasks, allowing participants to contribute without needing to understand the entire project.

• Clear Metrics: A visible count of unsolved problems motivated participants.

• Formal Verification: All proofs were formalized in Lean and stored on GitHub, allowing for automatic verification. This enabled contributions from strangers and anonymous participants, as correctness was machine-checked.

• Atomic-Level Discussion: Formal verification facilitated precise discussions, pinpointing errors at specific steps in a proof.

Diverse team collaborating on a large digital screen displaying mathematical problems and a '22 Million Solved' metric.

Tao noted that while automated theorem provers were used, basic collaboration platforms like GitHub and Zulip were "incredibly useful and essential."

AI's Role: Augmentation, Not Replacement

Tao also addressed the capabilities of large language models (LLMs) in mathematics. While LLMs can solve complex problems, including some mathematical Olympiad questions, they often make basic arithmetic errors. He demonstrated an instance where an LLM incorrectly calculated a simple sum.

He explained that combining LLM output with a verifier—where the LLM generates content, the verifier checks it, and feedback is provided for correction—can be effective. Tao is collaborating with Google DeepMind on AlphaEvolve, a tool that combines LLM generation with evolutionary algorithms. AlphaEvolve has shown promise in solving optimization problems, even breaking human records in hexagon packing problems.

Tao concluded that AI's greatest value to mathematics is not in replacing mathematicians in solving the hardest problems but in handling the "long tail of medium-difficulty problems." He stated that AI should "not compete with the pie of work that humans already do, but to enlarge the pie and create more tasks." He emphasized that AI tools require careful application and integration into broader collaborative systems to be most effective.