# 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. Published: 2026-09-02 Locale: en Tags: Terence Tao, AI math, human-AI collaboration, division of labor, Lean, AlphaEvolve, decision making TL;DR: Tao's team tracks 1,000-odd Erdős problems and closed out a coin-game problem through human-AI teamwork. AI's four tasks: search literature, fill proof steps, compute tables, translate into Lean. Humans' four: pose the problem, make the conjecture, understand the proof, notice two problems were the same. One dividing line: can a machine verify the result? ![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](/covers/tao-2026-09-02-coin-game-human-ai-division-cover.png) > *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](/figures/tao-coin-game-rule-en.svg) ## 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](/figures/tao-machine-verifiable-split-en.svg) 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](/figures/tao-solution-seeks-problem-en.svg) ## 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 - AI 101 channel, "Terence Tao demonstrates how AI solves math: a coin game, and which steps humans and AI each took," uploaded 2026-08-26: [youtu.be/llGxnS34pz8](https://youtu.be/llGxnS34pz8) - Last week's piece: [Numerators Without Denominators: Tao's Slightly Drunk Genius](/en/blog/tao-2026-08-31-ai-math-drunk-genius/)