On Sunday night, after the World Cup final had ended, mathematician Levent Alpöge posted a message on X that sounded almost casual: the Jacobian conjecture was false. Beneath it sat a small block of algebra, compact enough to fit in a single post. To most readers, it looked like an indecipherable tangle of symbols. To mathematicians, it was explosive.

The problem’s modern history is usually traced to a 1939 paper by German mathematician Ott-Heinrich Keller, and it later appeared as Problem 16 on Stephen Smale’s influential list of challenges for the new century. A recent historical study found that the two-variable version goes back even further, to a flawed proof published by Ludwig Kraus in 1884. In his post, Alpöge thanked University of Chicago mathematician Akhil Mathew for raising the question and “Fable” for working on it during the final, a reference to Anthropic’s Claude Fable 5. But the bottom line was striking: an age old mathematical problem had seemingly fallen during a football match.

To understand the breakthrough, imagine a rule that moves every point in a mathematical space to a new position, like rearranging all the dots on a map. The rules involved are polynomials, formulas built from familiar operations such as addition, subtraction and multiplication. Now zoom in on any tiny patch. If nearby points remain separate and the movement can be traced backwards, that small part of the map is locally reversible.

A test called the Jacobian determinant tells mathematicians whether the transformation has flattened or collapsed any direction at a particular point. If the result is non-zero, the transformation can be reversed within a sufficiently small neighbourhood. The Jacobian conjecture claimed that if this test produces the same non-zero value everywhere, the entire polynomial transformation must also have an algebraic undo button: another polynomial formula that takes every output back to its unique starting point. Put simply, if the map is reversible everywhere close up, it should be reversible as a whole.

Alpöge’s formula exposed the flaw in that intuition. It passes the local test everywhere. Its Jacobian determinant stays fixed at minus two. The exact number is unimportant; what matters is that it never changes and never becomes zero. Yet when you step back and look at the full map, three different starting points arrive at exactly the same destination. Once several locations have been merged into one, there is no unique way to trace the journey backwards. The local undo buttons still appear to work, while the system as a whole has lost information.

That single exception defeats a claim that was supposed to hold in every case. Alpöge’s construction disproves the conjecture for polynomial maps involving three variables. By adding extra variables that are left unchanged, the same example produces counterexamples for every higher number of variables. The two-variable case, the oldest version of the problem, remains open.

OK, enough math. What happened next is the really interesting part of the story. Other mathematicians could check the two decisive claims directly: calculate the determinant and substitute the three starting points. Terence Tao noted that this verification is remarkably brief. Later that day, Paul Lezeau manually encoded the result in Lean, a proof assistant that lets a computer check a mathematical argument step by step. An independent verification in Isabelle/HOL appeared the same day. Lezeau’s contribution was reviewed and merged into Google DeepMind’s Formal Conjectures repository six days later.

The formal systems did not discover the formula. They made its decisive claims machine-checkable. The result could move rapidly from a surprising candidate to trustworthy knowledge because the evidence was precise and independently testable.

The answer was easy to verify once it was visible, while discovering it had proven elusive. Tao observed that the formula contains an extraordinary pattern of cancellations, making a naive brute-force search an implausible explanation. A counterexample is a kind of certificate: a compact object that may be difficult to find and straightforward to test once someone places it in front of you.

The loop did it

We should still be careful about taking too much about the future of human-machine collaboration from this story. The public announcement does not reveal the prompts, intermediate reasoning, tools, failed attempts or degree of human steering involved. Mathew appears to have suggested the target. Alpöge published the formula and recognised its significance. Alpöge credited Fable with working on it, while a contemporary account described Fable as having found the counterexample. The mathematics is auditable; the collaboration is not.

Trying to award the entire achievement to either a human or a machine is dangerously simplisitic. Most debates about AI and work still treat a job as an indivisible object. We ask whether mathematics belongs to humans or machines, whether strategy is human work while analysis is machine work, or whether creativity can be automated. This episode offers a more useful frame. If anything, what matters here is the learning loop between humans and machines.

Advanced knowledge work consists of a sequence of cognitive events: choosing a worthwhile question, defining what a valid answer would look like, searching a large space of possibilities, producing a candidate, checking it, interpreting its meaning, deciding what follows and learning from the outcome.

Those cognitive events can be distributed across different forms of intelligence. In my new book on digital labor, I describe this as cognitive routing: deliberately directing each cognitive task to the form of intelligence best suited to perform it. A human expert may recognize which questions are worth asking. A generative model may explore possibilities beyond the limits of human time and patience. A deterministic or formal system may test whether a candidate satisfies precise constraints. Other experts may interpret the result, challenge its assumptions and decide how much authority it deserves.

The allocation will keep changing. The design challenge is to connect these capabilities into a reliable learning system.

Proof-carrying work

This suggests a powerful rule for enterprise AI: autonomy should scale with verifiability. AI-assisted discovery will advance fastest where searching for an answer is expensive, while checking a proposed answer is fast, independent and cheap.

The enterprise equivalent is proof-carrying work. An AI output should arrive with the evidence needed for another system or accountable person to accept, reject or escalate it. In software, agent-generated code can arrive with passing tests and security scans. In supply chains, an AI-generated schedule can be checked against capacity, inventory and service commitments. In finance, a recommendation can carry exposure calculations, policy checks and scenario results. In engineering, a proposed design can be tested through simulation before it reaches the physical world.

Trust comes from the verification architecture surrounding each output.

Formal verification is an unusually rigorous version of that architecture, and it also has limits. Lean can confirm that a formula satisfies a precisely stated mathematical claim. It cannot decide whether the claim captures the right question, whether the question is worth pursuing or what the result means. Enterprises face the same problem. A system can perfectly follow an incomplete policy, optimise a metric that damages the wider business, or verify an answer to a badly framed question. Human judgment remains essential around purpose, trade-offs, consequences and accountability.

As intelligence becomes abundant, evaluation becomes strategic infrastructure. This extends well beyond what AI teams commonly call evals. Evals generally measure how well a model or application performs against predefined tasks, rubrics and failure cases. Enterprises must also evaluate each output in context, at the moment it may influence a real decision. Is the evidence sufficient? Does policy permit the action? Are legal, financial and operational constraints satisfied? When should the system act, and when should it escalate?

Answering those questions requires a broader evaluation architecture: proprietary tests, simulations, policy engines, source verification, outcome data, exception histories, human review and escalation paths. These systems determine whether an output is trustworthy enough to inform a decision, bind a workflow or trigger an action.

They also track what happened afterwards. Did the recommendation produce the expected result? Where did the system fail? Which exceptions required human judgment? That evidence feeds the next cycle of evaluation and improvement. A durable advantage may therefore lie in the verification and learning system around the model. It determines how much authority a machine can receive, where human judgment should enter and how quickly the whole organization can improve.

Accelerating discovery

Meanwhile, back in the world of advanced mathematics, the learning loop around the disproved conjecture was already accelerating. The next day, Tao published a geometric explanation that made the apparently miraculous formula more intelligible. The announcement also prompted new counterexamples to the Gaussian Moments Conjecture, while another team built directly from Alpöge’s map to refute a related Hessian conjecture. These follow-on results were still preprints, but the speed of the sequence was revealing.

The cycle moved from question selection to AI-assisted search, independent checking, formal verification, human interpretation and a new round of questions. A process that might once have unfolded over months or years began turning in days.

The deeper lesson reaches far beyond mathematics. Discovery accelerates when different kinds of intelligence are connected around results that can be challenged and checked. The future of knowledge work will be organized around these learning loops, rather than a border with humans on one side and machines on the other.

Organizations that learn to ask sharper questions, search more widely, verify more rigorously and feed every result into the next cycle will gain a compounding advantage. The real race is to build systems in which every answer sharpens the next question, every decision produces new evidence, and the loop becomes more intelligent each time it turns.