What Terence Tao is telling mathematics to build

In the third week of July 2026, two conjectures were settled two days apart. Neither fell to a new theorem or a deep structural insight. Both fell to a search: a person steering a model through constructions until one of them broke the statement. Two days after the second one, Terence Tao gave a public lecture at the International Congress of Mathematicians about what the field should do about exactly this. The two events are one story told from opposite ends.

87 years

Jacobian Conjecture, 1939 to 2026

About 30 years

Dinitz–Garg–Goemans conjecture

The week itself

The first was the Jacobian Conjecture, posed in 1939. It says that a polynomial map whose Jacobian determinant is a nonzero constant must have a polynomial inverse, and over the decades it became notorious for attracting proofs that later collapsed. On July 20, Levent Alpöge posted an explicit map in three variables with a constant nonzero Jacobian that is not injective, so it has no inverse of any kind. He credited Akhil Mathew for asking the question and the model Fable for finding the construction. Checking the example is a routine computation; finding it took 87 years.

Levent Alpöge's original post on X

↗

Two days later, Dmitry Rybin posted a counterexample to the Dinitz–Garg–Goemans conjecture in graph theory, a problem he described as open for roughly thirty years. He also linked the GPT 5.6 Pro conversation in which the construction was found, so anyone could read exactly how it happened.

Dmitry Rybin's original post on X

↗

Neither result came from a model working alone. A person chose the problem, recognized which directions were worth pushing, and checked what came back, which is the division of labor mathematics has always had. What changed is the cost of the middle step. Someone who could test a handful of constructions in a week can now test thousands, including the strange ones that would never have justified the time before.

Two results in one week is two anecdotes, not a trend line. But problems this old do not usually fall at all, let alone twice in the same week by the same route, and it would be strange if that had nothing behind it. It is also worth noticing how both results arrived: as posts, with a construction inside, checked by whoever took the time to work through it. That works when it happens twice. It does not work when it happens every week.

Who Terence Tao is

If you have heard the name of one living mathematician, it is probably his. Tao was born in Adelaide in 1975, was learning calculus at seven, and won a bronze medal at the International Mathematical Olympiad at ten, the youngest competitor ever to medal there. He took silver at eleven and gold at twelve, finished his degree at Flinders University at fifteen, and started his PhD at Princeton at seventeen. He became a full professor at UCLA at twenty-four, where he still teaches.

The prizes followed. He won the Fields Medal in 2006, the closest thing mathematics has to a Nobel, and in 2014 he was one of the inaugural recipients of the Breakthrough Prize in Mathematics and its three million dollar award. With Ben Green he proved that the primes contain arithmetic progressions of every finite length, a result that had been out of reach for two centuries. With Emmanuel Candès he developed the compressed sensing results that let an MRI scanner reconstruct an image from a fraction of the measurements it used to need, which is the rare piece of pure mathematics that shortened hospital appointments.

What matters here is less the decoration than the breadth. Tao works across harmonic analysis, combinatorics, number theory, and partial differential equations, which is unusual to the point of being strange in a field this specialized. When he says something about what mathematics is for, he is speaking from an unusually large sample of it. He also co-chairs a working group on generative AI for the President's Council of Advisors on Science and Technology, so the question of what these tools are actually good for is part of his job rather than a hobby.

Quanta Magazine's profile of Tao's turn toward AI

↗

He did not watch this from the sidelines

In October 2023 Tao announced he was going to learn Lean 4, a language in which a proof is written so precisely that a program can check every step of it. His first serious attempt, formalizing Maclaurin's inequality, took about a month against an estimate of one week. That ratio is the whole problem with formal proof, and he published it rather than hiding it.

Then he did something more interesting. In November 2023 he and three coauthors posted a proof of the polynomial Freiman–Ruzsa conjecture, and four days later he opened a project to formalize it in Lean. Volunteers finished it in about three weeks. The following September he launched a larger one: take 4,694 equational laws in abstract algebra and settle all 22 million implications between them. Within a month the crowd had narrowed it to 238 open cases, by late November to 138, and by the end of March 2025 to around thirty. Along the way the project produced new mathematics nobody had asked for, including a construction its participants named magma cohomology.

The detail worth pausing on is who did that work. It was strangers, distributed, many of them not experts in the subject, contributing pieces the way people contribute to open source. That normally does not work in mathematics, because a proof is only as good as your confidence in the person who wrote it, and confidence does not scale to strangers. It worked here for one reason: Lean checked every contribution, so nobody had to vouch for anybody. Tao's description of what formalization changes about collaboration is blunt.

"you don't need to trust the people you're working with"

That is not a remark about software. It is the reason a subnet like this one can exist at all.

Tao's own running summary of his views on AI

↗

The argument he made at the ICM

On July 24, 2026, Tao gave the public lecture at the International Congress of Mathematicians, titled "Mathematics in the age of AI". He opened with an analogy. Between roughly 1900 and 1930, mathematics went through a crisis in its foundations, prompted by Russell's paradox and Gödel's incompleteness theorems. It was turbulent, and it ended with something valuable: an explicit, rigorous, standardized framework the field has trusted ever since. He thinks we are entering a second crisis of the same shape, this time in mathematical values and practices, and that it ends the same way if the community does the work.

He then did something careful. Rather than argue about how capable AI models really are, he set that question aside as a working hypothesis and asked what follows if they are reasonably capable. He was explicit that he was not asking anyone to believe the hypothesis, only to condition on it. The rest of the talk is about goals.

Suppose the goal is to solve as many unsolved problems as possible. Tao points out that we already know how that fails, and knew before AI existed: you get a large number of incorrect solutions to major problems. So the goal becomes solve as many problems as possible and verify them to be correct. That gives a pipeline — open problems, then unverified solutions, then verified solutions — and a third stage he adds after it, because a verified proof nobody can read is not yet mathematics: the results have to be communicated and understood.

He gave the evidence he trusts on capability, which is First Proof, an independent assessment that tests frontier models against batches of ten novel research-level problems under controlled conditions. In the second batch, run on May 28, 2026 against four AI harnesses and refereed by experts for both correctness and exposition, seven of the ten problems were solved at publication-level quality by at least one team.

7 of 10

Research-level problems solved at publication quality by at least one team, First Proof batch two, May 28, 2026

$10–$1,000

Compute cost per problem in that assessment

Tao's ICM 2026 slides, "Mathematics in the age of AI"

↗

His complaint about the rest of the public record is that it is not gathered under controlled conditions at all. Results get announced when they work and stay quiet when they do not, incentives are commercial, and costs frequently go undisclosed. He wants standardized, pre-disclosed benchmarks that measure reliability and efficiency per unit of work, not a stream of anecdotes.

And he pointed at the bottleneck directly. Sites collecting open problems, erdosproblems.com among them, now hold dozens of AI-generated proof submissions. Many are probably correct. No human expert has volunteered to check them, and in several cases the people who submitted them have said they are not qualified to. His term for what is coming is proof indigestion: results accumulating faster than anyone can confirm them, and a field moving from an era of proof scarcity to one of proof abundance it is not yet organized for.

Why this subnet is built the way it is

Conjectures.io is one answer to the middle stage of that pipeline, and every design decision in it maps onto something in the argument above.

The statement is pinned before anyone attacks it. Each task carries the complete Lean statement taken from one published revision of a public corpus, with a fingerprint proving every validator checked the same problem. Nobody can quietly weaken a hypothesis or strengthen a conclusion to make a proof go through, which is the oldest way a wrong result gets accepted. It also matches the division of labor Tao recommends for projects like this: humans write the statements, machines supply the proofs.

The check is the filter. A submission runs without network access, against a verifier that rejects the known shortcuts, inspects which axioms and dependencies the proof actually used, and asks the Lean kernel for a verdict. Tao's description of the situation is that traditional mathematics was a slow tap of clean water and AI is a firehose, and that the entire job is building filters. This is a filter. It has no opinion about who you are or which model you used.

Because trust is not required, the door can stay open. This is the part that the polynomial Freiman–Ruzsa project and the equational theories project already demonstrated: once a machine checks every contribution, a crowd of strangers becomes an asset rather than a liability. Tao's term for the version of this he wants is big mathematics, with room in it for undergraduates and amateurs contributing modular pieces. A subnet adds the thing those volunteer projects did not have, which is a reason to show up other than goodwill.

Every attempt is recorded against a fixed target. One shared verifier, tasks that do not move, submissions committed and then revealed, and a result anyone can rerun. That is close to the controlled, pre-disclosed measurement Tao says the public record lacks, and it has a property the current record badly needs: attempts that fail are still attempts, counted rather than forgotten. A catalog like this reports its own denominator.

The catalog is a population, not a trophy. The pool holds exact tasks, each pinned to a published source revision, and the point is the sweep rather than any single entry. Tao has been explicit that the real near-term value is in what he calls the attention-starved long tail, the enormous number of problems that are tractable but that nobody has time to look at, and that surveying thousands of problems at once is a genuinely new instrument rather than a faster version of an old one.

What this is and is not

Verification is not discovery. Lean checks a proof; it does not go looking for one. This subnet does not make anyone better at mathematics, and it is not trying to. It decides which claimed results are real, which is a narrower job and a necessary one.

It is also one stage of a longer process. A proof that clears the verifier is certified correct and not yet explained, and turning a checked result into mathematics other people can learn from stays human work. Machine checking clears the queue in front of that work. It does not do it, and nothing here pretends otherwise.

The near-term expectation is the long tail: tractable problems that have gone unattacked because nobody had the time, rather than the marquee names. Counterexample handling is still in development as well, since a counterexample needs its own formal statement and review path before the network can return a verdict on it.

The bet

The two counterexamples in July arrived as posts on X, with a construction inside, and were checked by whoever felt like working through them. That is a fine way to handle two results. It is not a way to handle two hundred. Verification becomes a queue, priority becomes an argument in the replies, and the person who found the result has nothing to show for it beyond credit in a thread.

Tao's answer to the whole situation is that broad participation and scale are a net win specifically because formal verification lets us filter the untrustworthy inputs and keep the good ones. Take that seriously and it describes a piece of infrastructure: a fixed set of important statements, an open door, a mechanical check, and a reason to bother. That is what this is. If more weeks like the third week of July are coming, the infrastructure should exist before they arrive.