tech

Terence Tao's Coin Game: AI Did Four Things, Humans Did Four Things — I Checked My Own Division of Labor Against His

Terence Tao walks through a real case of humans and AI solving a math problem together: Gemini filled a missing proof step, AlphaEvolve computed up to 16 piles, Aristotle translated proofs into Lean for machine checking — while posing the problem, making the conjecture, understanding the proof, and noticing two problems were the same all came from humans. The dividing line matches the rule I use to delegate work to AI: only hand over what a machine can verify.

  • Terence Tao
  • AI math
  • human-AI collaboration
  • division of labor
  • Lean
  • AlphaEvolve
  • decision making

Neoclassical oil painting cover: a long wooden table with a row of coin stacks of uneven heights, a scholar leaning over to study them, an oil lamp lighting a few stacks, a framed diagram of grids and squares on the wall

He who learns alone, without friends, remains narrow and ill-informed.
— Book of Rites, “Record on Learning” (Warring States to Western Han period)

What this is about

Last week I wrote about Terence Tao calling AI mathematicians “slightly drunk geniuses” whose scores come with numerators but no denominators. This week the same series (AI 101 channel, uploaded 2026-08-26, about 14 minutes) dropped another episode. No metaphors this time — one real case, a coin game, with every step named: which ones humans did, which ones AI did.

The coin game

Alice splits a big pile of coins into n stacks, heights up to her. Bob takes away some stacks — but the ones he picks must run strictly upward or strictly downward in height, never zigzag. Bob picks the combination that gets him the most; Alice arranges heights to lose the least. The question: what entry fee should Alice charge Bob to make it fair?

Someone on a forum ran the small cases and made a lovely conjecture: when the number of stacks is a perfect square k², Bob can take 1/k of the total. With 16 stacks, a quarter. The conjecture sat unproven for two months.

Eight coin stacks of uneven heights; four highlighted stacks of heights 4, 8, 10, 13 rise monotonically, connected by a dashed line — Bob may only take stacks that run one way

Then, who did which step

Someone fed the conjecture to an automated prover called Aristotle — and it worked, producing a proof and translating it into Lean, a language that lets a machine check a proof line by line. Its trick: convert the coin problem into packing small squares into a big square. The video notes the move comes from an obscure 1959 paper, and the problem itself had been solved by other means in 2016 — few remembered.

When the stacks grew too many to compute, Tao switched to AlphaEvolve, ran it up to 16 piles, stared at the patterns, and made a conjecture of his own. Boris simplified it; Lawrence Wu recognized the simplified function as identical to one from a “square packing” problem solved two years earlier. The pieces snapped together.

Tao compresses the episode into two lists. AI did four things: searched literature, filled proof steps, computed tables, translated into Lean. Humans did four things: posed the problem, made the conjecture, understood the proof, noticed two problems were the same one. His words: AI by themselves are already great, but there’s far more potential in human-AI collaboration.

And the denominators I complained about last week — this episode provides some: of the 1,000-odd Erdős problems tracked, 699 remain unsolved and about 480 are solved, a large share dug out of old literature where they’d been solved decades ago and forgotten; Aristotle’s automated proving succeeds only about 1–2% of the time.

The line between the two lists

AI’s four tasks share one trait: verification can be handed to a machine. Literature checks against the source, Lean verifies line by line, tables can be recomputed, a bad translation won’t compile — garbage gets caught on the spot. The human four are the opposite: whether a problem is good, a conjecture beautiful, a proof truly understood, two problems one — the output is judgment itself, and no machine can grade it.

A dashed line splits eight tasks into two columns: left — search literature, fill proof steps, compute tables, translate to Lean, given to AI; right — pose problems, make conjectures, understand proofs, notice two problems are the same, kept by humans

That’s the same line I use when delegating to AI. Fetching data, converting files, batch rewrites — handed over without worry, because a script can check the result. Whether to buy a stock, whether an article’s conclusion holds — work whose output is the conclusion itself I don’t outsource, because nothing can check it for me. Mathematicians have Lean as referee, so they can let AI charge ahead and flail; those of us making investment judgments don’t, so we keep AI outside the judgment room. The difference isn’t how smart the AI is — it’s whether your field has a referee a machine can be.

Holding a solution, hunting for its problem

One more detail keeps growing on me. Aristotle’s move ran in the reversed order: not holding a problem and hunting for a solution, but holding an old 1959 solution and finding the new problem it fits. I have a drawer of such old solutions myself — the technical indicators I’ve collected over the years. I used to ask, “can this indicator pick winning stocks?”, and the answer kept disappointing. Now the stocks are chosen by other means, and I walk around holding the indicators, looking for the problems they actually fit — timing entries, trimming drawdowns. The indicators didn’t change; they finally met the right problem.

Two panels: on the left the arrow runs from problem to solution, the usual order; on the right it is reversed — from a solution in hand (an old paper, my indicators) to the problem it truly fits

One thing to take with you

The evening I finished the video I did one small thing, and you could try it today: write on a sticky note the last three tasks you were about to hand to AI, and ask of each — when this is done, can a machine or script tell me right from wrong? If yes, delegate freely. If no, the output is your judgment; let AI be a staff officer. One of my three failed the question, and I changed it on the spot from “ask AI to write the conclusion” to “ask AI to lay out the materials.”

Sources