Logic & Valid Inference

Movement I

What the syllogism was hiding

The main lesson handed you “All men are mortal” and moved on. But Aristotle’s term logic has internal architecture worth seeing, and a fault line that took two thousand years to notice.

Every classical categorical statement comes in one of four flavours, and medieval logicians labelled them with the vowels of two Latin words — affirmo (“I affirm”) and nego (“I deny”). A: All S are P (universal affirmative). E: No S are P (universal negative). I: Some S are P (particular affirmative). O: Some S are not P (particular negative). Arrange these four at the corners of a square and you get one of the oldest diagrams in Western thought, the square of opposition, which maps how the four statements support and contradict one another. The A and O corners are contradictories — exactly one is true. So are E and I. The A and E corners are contraries — they can’t both be true, but they can both be false. It is a little machine for reasoning about quantity, and for centuries it was drilled into every educated head in Europe.

Now the fault line. Look at the vertical edges, called subalternation: the classical square says that if “All S are P” is true, then “Some S are P” must be true too. From the universal, you may descend to the particular. This feels obvious — if all ravens are black, then surely some raven is black. But it smuggles in an assumption Aristotle never flagged: that there is at least one S. Watch it break. “All trespassers will be prosecuted” is something a landowner can say truthfully even if, happily, nobody ever trespasses. But subalternation would force “Some trespasser will be prosecuted” — which asserts a trespasser exists. Worse: “All unicorns are white” sounds harmlessly true, yet the classical square derives “Some unicorn is white,” conjuring a unicorn into existence by pure logic. This is the problem of existential import, and it is the precise crack that Frege’s quantifiers (from the main lesson) were built to seal.

Modern predicate logic reads “All S are P” as a careful conditional — for anything at all, if it is an S then it is a P — which is automatically true when there are no S’s to check (a “vacuously true” statement, like the promise you trivially keep by never making a relevant move). The universal no longer implies the particular. This is why “all unicorns are white” and “all unicorns are blue” can both be true at once: with zero unicorns, every universal conditional of the form “all unicorns are…” comes out vacuously true. Existential claims such as “some unicorns are white” do not. The price of Frege’s fix was surrendering some of the square’s tidy inferences — a worthwhile trade, and a beautiful case study in how formalizing an intuition reveals a hidden assumption nobody knew they were making.

How proofs are actually built

The main lesson spoke of “valid form” but never showed how a logician constructs a proof step by step. There are two great styles, and the rivalry between them shaped twentieth-century logic. Natural deduction, devised by Gerhard Gentzen in the 1930s (and independently by Stanisław Jaśkowski), tries to mimic how humans actually reason: you make temporary assumptions, derive consequences, and then “discharge” the assumptions — exactly the move in “suppose for contradiction…” Its sibling, the sequent calculus, also Gentzen’s, is more symmetric and machine-friendly, tracking what follows from what as an explicit ledger of premises and conclusions.

Gentzen then proved something deep about his own system: the cut-elimination theorem (his “Hauptsatz,” or “main theorem”). Informally, it says any proof that detours through a clever intermediate lemma can be rewritten into a direct proof that never leaves the subject matter of its premises and conclusion. Every shortcut can, in principle, be unwound into a plodding straight line. This sounds technical, but it supplies an important basis for automated proof search: cut-free proofs obey a subformula discipline that restricts which formulas need consideration. It does not make proof search uniformly manageable — first-order validity is undecidable, and eliminating cuts can make proofs enormously longer. Cut elimination also connects, through Curry–Howard from the main lesson, to how programs compute by simplification. Gentzen’s ledgers are the distant ancestor of the proof assistants we’ll return to in Movement V.

Movement II

A field guide to bad arguments

The main lesson gave you the two great formal fallacies — affirming the consequent and denying the antecedent — the ones with broken skeletons. But most of the bad reasoning you’ll actually meet in the wild is informal: the form is fine, the content cheats. These have been catalogued since antiquity (Aristotle wrote a whole treatise, the Sophistical Refutations, on argumentative dirty tricks), and knowing their names is a genuine cognitive upgrade — you cannot easily un-see a fallacy once you can label it. Here is a working field guide to the most common specimens.

A special pair deserves its own spotlight, because they are where logic meets the probability we’ll meet tomorrow on Day 4. The gambler’s fallacy is the conviction that a run of reds at the roulette wheel makes black “due” — as if the wheel had a memory and a conscience. It doesn’t; each spin is independent, and the ball owes you nothing. Its mirror image, the base-rate fallacy, is ignoring how rare something is when interpreting evidence: a test that’s “99% accurate” for a disease that afflicts one person in ten thousand will still flag mostly healthy people, because the rare truth is swamped by the common error. Both are failures of probabilistic intuition so systematic that they need formal machinery to override — which is precisely the argument tomorrow opens with.

Movement III

The sentences that broke logic

The main lesson mentioned Russell’s paradox in passing, as the letter that cracked Frege’s life’s work. But paradoxes are not mere curiosities in logic — they are its stress tests, the places where the machine seizes up and forces a redesign. Twice, a single self-referential sentence has brought down a foundation. Understanding why is to understand what logic is made of.

The Liar, and why it won’t sit still

Start with the oldest. Consider the sentence: “This sentence is false.” Is it true? If it’s true, then what it says holds — so it’s false. But if it’s false, then what it says fails — so it’s true. The sentence flips endlessly, true to false to true, refusing to land. This is the Liar paradox, known to the ancient Greeks (the Cretan Epimenides declaring all Cretans liars is a cousin), and it is not a party trick. It shows that the innocent-looking notion of truth, combined with a sentence’s ability to talk about itself, produces contradiction. Alfred Tarski drew the radical lesson in the 1930s: no language can consistently contain its own complete truth-predicate. To talk about the truth of sentences in a language, you must climb to a higher metalanguage — truth is always spoken from one level up. (This is also why a recurring move in this course is to separate the thing from the talk about the thing, a ladder of levels we first felt in Day 1’s internal-versus-external split.)

Russell’s paradox, in slow motion

Now the one that actually drew blood. Frege’s foundation rested on a generous assumption: any property you can state carves out a set — the set of all things with that property. Sounds unimpeachable. Russell asked about one particular property: not being a member of itself. Most sets aren’t members of themselves (the set of all teacups is not a teacup). So consider R, the set of all sets that are not members of themselves. Is R a member of R? If R is a member of itself, then by its own definition it must not be — contradiction. If R is not a member of itself, then it satisfies the membership condition, so it is — contradiction. Either way the system detonates. The barber version makes it vivid: in a village where the barber shaves exactly those who don’t shave themselves, who shaves the barber? Russell sent this to Frege in 1902, just as the second volume of his masterwork went to press. Frege’s reply is one of the most gracious admissions of disaster in the history of thought: “a scientist can hardly meet with anything more undesirable than to have the foundation give way just as the work is finished.” The foundation gave way.

The rescue, and its price

How do you save logic from a sentence? Russell’s own answer, built with Alfred North Whitehead in the monumental three-volume Principia Mathematica (1910–1913), was the theory of types: arrange objects in a strict hierarchy — individuals at the bottom, sets of individuals above them, sets of those above that — and forbid any set from referring to itself. The rules of grammar simply outlaw “R is a member of R” as meaningless, the way “the number seven is blue” is meaningless. Paradox averted by stratification. Principia was so rigorous it took hundreds of pages to reach the proof that 1 + 1 = 2 (with the wry remark, when it finally arrived, that “the above proposition is occasionally useful”). It is a monument and a warning: the cost of absolute rigour can be near-unreadable.

That hierarchy-of-types idea did not die in 1913. Stripped of its philosophical baggage and rebuilt by Per Martin-Löf in the 1970s, type theory became the logical foundation underneath Lean, Rocq, and Agda — the very proof assistants the main lesson celebrated. The defensive wall Russell built against paradox turned out, sixty years later, to be the ideal architecture for telling a computer what a proof is. Logic’s worst crisis seeded its most powerful modern tool.

When two truth-values weren’t enough

One more foundational tremor, and a charming one. The main lesson listed fuzzy and many-valued logics among the non-classical zoo, but skipped the story of where the first rigorous many-valued logic came from. In 1920, the Polish logician Jan Łukasiewicz was brooding on a problem Aristotle himself had raised: the sea battle. “There will be a sea battle tomorrow.” Is that statement true or false today? If it’s already true, the future seems fixed and free will evaporates; if already false, the battle is impossible. Aristotle squirmed. Łukasiewicz’s bold move was to deny that the statement must be either true or false right now — he introduced a third value, “possible” or “indeterminate,” for the open future. From that one philosophical itch grew the entire field of many-valued logic, the mathematical parent of the fuzzy logic running in your camera’s autofocus. A question about fate, asked for two thousand years, turned into a branch of engineering.

Movement IV

The rule that needs no rule

Here is a puzzle that looks like whimsy and turns out to touch bedrock. It was published in 1895 by Lewis Carroll — yes, the Alice author, who by day was the Oxford logician Charles Dodgson — under the title “What the Tortoise Said to Achilles.” It is four pages long, written as a dialogue, and it has unsettled logicians for over a century.

Achilles has a valid argument. From two premises — call them A (“things equal to the same thing are equal to each other”) and B (“these two things are both equal to that third thing”) — the conclusion Z (“these two things are equal to each other”) plainly follows. The Tortoise, with maddening politeness, agrees that A and B are true, and agrees the argument is valid. But he declines to accept Z. Why? Because, he says, to get from “A and B are true” to “therefore Z,” you must be relying on some further rule — call it C: “if A and B are true, then Z is true.” Fine, says Achilles, grant C as well. The Tortoise cheerfully does — and still won’t accept Z. Because now, to get from A, B, and C to Z, you need yet another rule, D: “if A and B and C are true, then Z.” And so on, forever. Every time Achilles tries to nail down the rule of inference by writing it as an explicit premise, the Tortoise demands a new rule to license that premise. The list of premises grows without end and Z is never reached.

“And so on. You see, Achilles, we are now reaching a series of inferences that has no end.”

The Tortoise has discovered something profound: a rule of inference cannot be reduced to a premise. The step from premises to conclusion — the actual act of inferring — is not itself another premise in the argument; if you try to make it one, you trigger an infinite regress. Reasoning requires something beyond the explicit statements: a willingness to move, to actually apply the rule rather than merely contemplate a description of it. Logic, it turns out, cannot be purely a matter of more and more written-down content. At its heart there must be an act — a doing, not just a saying.

You have met this shape before. On Day 1, the Agrippan trilemma showed that every chain of justification must either regress forever, loop, or stop somewhere unjustified. Carroll’s Tortoise is the same skeleton wearing different clothes: every attempt to justify the act of inference itself regresses forever. The two puzzles rhyme because they’re about the same thing — the point where reasoning has to touch down on something that isn’t more reasoning. For justification, that floor is Day 1’s “basic beliefs” or “reliable processes.” For inference, it’s the brute capacity to apply a rule. Both tell us that a mind, or a machine, cannot run on explicit content alone. There has to be, at the bottom, a thing that simply does.

The ceiling overhead

The main lesson’s frontier — proof assistants verifying mathematics at zero tolerance — naturally invites a dream: could we someday formalize all of mathematics, reduce every truth to a mechanical check, and never be uncertain again? It is the dream Frege and Russell chased, and it is worth knowing, even now, that the dream has a proven ceiling. In 1931, a 25-year-old Austrian named Kurt Gödel demonstrated that any consistent, effectively axiomatized formal system strong enough to express basic arithmetic is incomplete: some arithmetic statements can be neither proved nor refuted within it. His second incompleteness theorem adds that, if such a system is consistent, it cannot prove its own consistency using only its own resources. There is no consistent, effectively axiomatized, complete, self-certifying formalization of arithmetic. Not because we haven’t built it yet, but because it cannot exist.

This is the great counterweight to Movement V, and we will give it the full day it deserves on Day 28. For now, hold the tension in your mind like a chord: mechanized proof is breathtakingly powerful, verifying things no human could check by hand — and there is a hard, theorem-proven limit to how much certainty any such system can deliver about itself. The proof assistant is a magnificent tool operating inside a cage whose bars Gödel measured exactly. Keep both halves. The triumph and the limit are the same subject seen from two sides — which, you may have noticed, is the recurring shape of this entire course.

Movement V

The long road to a proof no human can read

The main lesson introduced Lean and AlphaProof as if they arrived fully formed. They didn’t. There is a sixty-year backstory of machines proving things, and it contains some of the most philosophically charged moments in modern mathematics — the points where the community had to decide whether a proof nobody could fully check by hand still counted as a proof. This is the deep history the frontier was standing on.

Two theorems that license the whole enterprise

First, a piece of foundational reassurance that makes mechanized logic trustworthy at all. For standard first-order logic, two great metatheorems hold. Soundness: anything you can prove using the rules is actually true in every model — the rules never lie. Completeness (proved by the same Gödel, in 1929, a gentler theorem than his famous one): anything that is true in every model can be proven using the rules — the rules miss nothing. Together they show that, in standard first-order logic, proof rules and model-theoretic truth can be made to line up exactly. Proof assistants such as Lean rest on a related but more specific trust story: a small kernel, a type-theoretic foundation, the axioms in use, and the faithfulness of the formalization to the original problem. The crucial advantage is mechanical checking: every step must pass the kernel, so a bad step cannot slip through as rhetoric.

The colours that started a fight

The first earthquake came in 1976. The Four Colour Theorem — the claim that any map can be coloured with just four colours so that no two bordering regions share a colour — had taunted mathematicians since 1852. Kenneth Appel and Wolfgang Haken at the University of Illinois finally cracked it, but their proof did something unprecedented and, to many, deeply controversial: it reduced the problem to nearly 2,000 specific configurations and then used a computer to grind through checking every one. No human had verified, or could feasibly verify, all those cases by hand. Was it a proof? Philosophers and mathematicians erupted. A proof was supposed to be a chain of reasoning a human mind could follow and be convinced by; this was an act of faith in silicon and the program that ran on it. The University of Illinois math department, with a touch of defiance, started stamping its postage with “FOUR COLORS SUFFICE.” The discipline had crossed a threshold it could never uncross.

The doubts lingered for decades — until the proof assistants arrived. In 2005, Georges Gonthier formalized the entire Four Colour Theorem inside the Coq proof assistant, reducing the whole argument, computer-checked cases and all, to steps verified by a tiny trusted kernel. The thing that had felt like blind faith in 1976 became, in 2005, a theorem checked at zero tolerance. Mechanization didn’t just match the contested proof; it redeemed it.

The conjecture a machine cracked alone

Then, in 1996, a milestone the main lesson hinted at but didn’t tell: the first time an automated prover solved a famous open problem essentially by itself. The Robbins conjecture — a question, posed in the 1930s, about whether a certain simple set of algebraic equations is enough to define Boolean algebra — had defeated the field’s best for sixty years. Tarski himself had worked on it and failed. On October 10, 1996, a program called EQP, written by William McCune at Argonne National Laboratory, found a proof after about eight days of searching. It made the front page of The New York Times. McCune phoned the then-81-year-old Herbert Robbins to tell him his conjecture was finally settled — by a machine.

But here’s the twist that makes it a perfect parable. The proof EQP produced was, in the words of one logician, “a computer-generated proof that nobody understands.” It was a terse sequence of algebraic substitutions, some so unintuitive that no human would ever have dreamt of them, and it offered no insight — no story about why the theorem is true, just an unanswerable certification that it is. This is the question that has haunted machine proof ever since, and that the AI provers of 2026 sharpen to a point: if a machine hands you an airtight proof you cannot comprehend, have you gained knowledge, or merely a verdict? Mathematics has always wanted two things from a proof — certainty and understanding. The machines can now deliver the first in cases where the second is nowhere to be found. (A direct descendant of Day 1’s worry about belief that is correct without being connected to the truth in the right way.)

The proof that took a team five years to doubt

The pattern recurred, bigger, in the story of Kepler’s conjecture — the 1611 claim, made by the astronomer who also gave us planetary orbits, that the way greengrocers stack oranges (the “face-centred cubic” packing) is the densest possible arrangement of spheres. Thomas Hales proved it in 1998, but the proof was a 300-page argument leaning on enormous computer calculations. The twelve referees of the Annals of Mathematics laboured for years and finally returned a verdict no journal had ever issued: they were “99% certain” the proof was correct, but could not fully verify the computer portions. Ninety-nine percent. For a mathematical proof, whose entire promise is certainty, that one percent was a wound.

Hales’s response was to declare war on the doubt. He launched the Flyspeck project — the name a playful contraction of “Formal Proof of Kepler” — to formalize the entire thing inside proof assistants, leaving no calculation untrusted. It took a international team over a decade. In 2014 they finished, using a combination of the HOL Light and Isabelle systems, and published the official account in 2015. The orange-stacking problem, open for 400 years and only “99% certain” in 1998, became a fully machine-verified theorem. established

• 1929 · the licenceGödel’s completeness theorem. Provability and truth march in step for first-order logic — the guarantee under which every proof checker operates.
• 1976 · the controversyFour Colour Theorem (Appel & Haken). ~2,000 cases checked by computer; the first major proof no human could verify by hand. “Four colors suffice.”
• 1996 · the lone machineRobbins conjecture (McCune’s EQP). An automated prover settles a 60-year-old open problem in 8 days — with a proof “nobody understands.”
• 2005 · the redemptionFour Colour Theorem, formalized (Gonthier, in Coq). The 1976 act of faith becomes a kernel-checked theorem.
• 2014 · the 400-year finishKepler conjecture, formalized (Flyspeck, HOL Light + Isabelle). Hales’s “99% certain” proof becomes fully machine-verified.
• 2024–26 · the AI turnAlphaProof and after. Neural search inside a proof kernel — covered in the main lesson, deepened below.

How a machine actually searches for a proof

It’s worth lifting the hood on how these systems work, because the main lesson treated the proof assistant as a black box. There are really two distinct jobs, and conflating them is a common error. A proof checker (Lean, Rocq, Isabelle) merely verifies a proof you supply, step by step, against its kernel — it’s a sceptic, not an inventor. A proof searcher or automated theorem prover (like EQP, or modern tools) tries to find a proof from scratch. The hardest and most practical version of search is the humble-sounding SAT solver — a program that, given a tangle of true/false constraints, hunts for an assignment that satisfies them all. This is the Boolean satisfiability problem, and (as we’ll see on Day 29) it sits at the exact centre of the P-versus-NP question, the most important open problem in computer science. Yet despite being theoretically intractable in the worst case, modern SAT solvers routinely chew through problems with millions of variables, and they quietly power chip design, software verification, and logistics. One SAT-solver proof — of a colouring problem called the Boolean Pythagorean Triples problem, settled in 2016 — produced a certificate 200 terabytes long, at the time the largest proof ever produced. A proof you could never print, let alone read, but every line mechanically checkable. Carroll’s Tortoise would have had feelings about it.

The AI provers, with the hype filter still on

Which brings us back to the present, and to the deeper version of the main lesson’s AI story. The genuine frontier of 2024–2026 is the marriage of two things that were always meant for each other: the neural network’s gift for guessing which step to try, and the proof kernel’s refusal to accept a step outside its formal rules. Several research threads are worth knowing by name. Autoformalization — automatically translating mathematics written in ordinary English into formal statements a machine can check — is the bottleneck everyone is racing to widen, because the world’s mathematical knowledge is almost all in prose, and a machine can only verify what’s been formalized. Tools like LeanDojo opened the proof assistant up as a training environment for AI. And the AlphaProof system the main lesson described works precisely by auto-formalizing about a million problems into Lean and training against the kernel’s verdicts, so that, in DeepMind’s phrase, there are “no hallucinations to worry about” in the checked derivation — an invalid formal step simply fails to compile.

The scorecard, sharpened from the main lesson:

• What’s real established: AI has reached medal-level competition performance; AI-assisted formalization is genuinely accelerating; and in May 2026 an internal OpenAI model generated a counterexample to the Erdős unit-distance conjecture that human mathematicians checked and digested. A kernel-checked system will not accept a derivation that violates its formal rules. Passing verification therefore establishes the theorem relative to the formal statement, axioms, and kernel; whether the formalization faithfully captures the intended informal claim remains a separate question. That scoped guarantee is the deep point — machine-learning’s creativity can now be paired with mechanical proof checking.
• What’s emerging promising hint: 2025–26 preprints describe AI agents solving some previously open (if narrow and specialized) problems in Lean, while the unit-distance result shows that autonomous mathematical discovery can sometimes reach accepted research. Fresh, important, still uneven. Watch this space without swallowing the pitch.
• What’s hype contested/hype: any claim that AI has “solved mathematics” or made mathematicians obsolete. One landmark counterexample is not a general mathematical mind, and contest problems are still a narrow slice with known-to-exist short answers. Recall from the main lesson that even at the 2025 “gold” level, dozens of human teenagers still scored higher.

The thread running through all sixty years — from Appel and Haken’s contested map, through the Robbins proof nobody understands, to AlphaProof searching inside Lean’s unforgiving kernel — is a single quiet idea, the one the main lesson closed on. Aristotle wanted a chain of reasoning that could not be doubted. We have finally built a machine that enforces a formal version of that standard, line by line, relative to a specified kernel and axioms. What we are still discovering is the strange new questions that machine raises: whether a proof we cannot read is a proof we have understood, and whether formally checked certainty, delivered without insight, is the thing mathematicians were really after all along.

Dispatch I

The provers grew up — and went open

The main lesson left the AI-proving story at AlphaProof: a closed system, behind a corporate wall, requiring days of computation per problem. Since then the field has done something the larger AI world rarely does — it has gone open, and it has gotten startlingly good. In 2025, anyone with a decent graphics card could download a model that solves olympiad-level mathematics in formal, machine-checked Lean. That is the quiet earthquake.

To follow it you need to understand the scoreboard. Machine provers are ranked on shared benchmarks — fixed sets of problems used to compare systems. Three matter. miniF2F (introduced 2022) is a few hundred olympiad-style problems and was, until recently, the gold standard; it is now nearly saturated, with the best systems scoring near the ceiling. PutnamBench (2024) is harder — problems from the legendarily brutal Putnam undergraduate competition, where the median human score is famously zero. FrontierMath (2024) spans tiers from challenging university-level work to research-level problems that may take experts days. Its scores depend on the tier, dataset version, and evaluation protocol, so no single percentage characterizes the benchmark. As one benchmark saturates, the field builds a taller one.

Now the systems doing the climbing. Two open-weights provers reset expectations in 2025, and a third pushed into olympiad-gold territory.

Two things deserve emphasis, one exciting and one limiting. The exciting one: a 32-billion-parameter model — small enough to run on hardware a serious hobbyist could own — now matches systems that, a year earlier, needed a data centre. Capability is collapsing in size and cost, fast. The limiting detail hides inside the phrase Pass@k. When a paper reports “88.9% on miniF2F,” it often means the model was allowed thousands of attempts per problem, and succeeded at least once. “The machine solved it” can quietly mean “one of eight thousand tries compiled.” That’s not cheating — for formal proof, a single compiling proof is a proof, no matter how many failures preceded it — but it is a very different thing from a human who gets it on the first attempt because they understood it. Hold both facts: the provers are genuinely, rapidly better, and the headline percentages flatter them.

Dispatch II

The machine that found something nobody had found

Proving a known theorem is one thing. Discovering a new mathematical object — a construction no human had ever written down — is another, and in 2023 a machine did exactly that, in a way worth understanding precisely because it is so easy to mis-tell.

The system was FunSearch, from Google DeepMind, published in Nature in December 2023. The setup is elegant and a little humbling. Take a hard mathematical problem where you want the best possible example of something. Have a large language model write little programs that generate candidate examples. Score each program by how good its output is. Keep the winners, feed them back to the model to mutate and improve, and loop — an evolutionary search where the LLM is the source of mutations and a fast, dumb scorer is the judge. The target was the cap set problem, a notorious question in combinatorics that the Fields Medalist Terence Tao has called one of his favourites. FunSearch found a cap set in dimension 8 of size 512 — larger than the best previously known, which had stood at 496 — and nudged a long-stuck lower bound upward for the first time in twenty years.

That is a real, verifiable, new mathematical result, and it earns an established. But now read the fine print, because the fine print is the whole lesson. First, it was rare: only four of a hundred and forty experimental runs found the size-512 set at all — the machine got lucky a handful of times out of many. Second, and stranger: the language model was never told what problem it was working on. It saw only an abstract scoring function and a request to write better programs. It had no concept of “cap set,” no understanding of the mathematics, no idea it was making history. The insight, such as it was, lived in the loop — the marriage of the model’s blind generative fluency with a scorer that could tell better from worse — not in any moment of machine comprehension. The computer scientist Ernest Davis, reviewing the result, stressed exactly this: the genuinely interesting thing is the human–AI feedback structure, not autonomous AI insight. A human mathematician, Jordan Ellenberg, then looked at what FunSearch had produced, noticed a symmetry the program had stumbled into, and used that human observation to push the bound further. The machine found the brick; the human saw the cathedral.

The pattern has since scaled up. AlphaEvolve (DeepMind, 2025) generalized the FunSearch idea into a broader “evolutionary coding agent,” and a November 2025 paper — Mathematical exploration and discovery at scale, with Tao himself among the authors — turned it loose on sixty-seven problems across analysis, combinatorics, geometry, and number theory, rediscovering known optima and improving a handful. established The authors’ own framing is the key takeaway of this entire dispatch: these systems are doing search and optimization, brilliantly, at superhuman scale and speed. They are not doing proof, and they are not doing understanding. They are a new and powerful kind of mathematical telescope — and a telescope discovers nothing on its own; it just lets a mathematician see farther.

Dispatch III

The Erdős affair: a case study in how to read a headline

If you want a single story that teaches the entire skill this curriculum is built around — separating a true claim from a true-sounding one — it is the saga of AI and the Erdős problems, which played out in public over the winter of 2025–2026. It has a hype spike, a sharp correction, and then a quieter, genuinely interesting truth. Watch all three beats.

The backdrop: Paul Erdős, the wandering Hungarian who posed more problems than perhaps anyone in history, left behind hundreds of open questions, now catalogued at a public database maintained by the mathematician Thomas Bloom. They make an irresistible target for an AI lab wanting to claim a scalp.

Beat one — the spike

In October 2025, figures at OpenAI announced, with considerable fanfare, that GPT-5 had “found solutions to 10 (!) previously unsolved Erdős problems” and made progress on others. The number flew around the internet. It sounded like the moment the machines started doing real research mathematics. hype

Beat two — the correction

It came fast, and from the person best placed to deliver it. Thomas Bloom, who runs the database, called the claim “a dramatic misrepresentation.” The problems had not been solved by GPT-5. They had been solved years earlier, by humans, in papers Bloom simply hadn’t yet logged — and the model had done the genuinely useful but utterly different job of finding those existing papers. “Open,” on his database, only ever meant “I personally am not aware of a paper solving this.” The origin case, problem #339, had been settled roughly twenty years before. What GPT-5 had demonstrated was superb literature search, not mathematical discovery. Even Demis Hassabis, head of a rival lab, called the episode “embarrassing.” OpenAI’s own subsequent paper quietly reframed the results as exactly what they were: retrieval, not proof.

The machine had not answered the question. It had found where someone else already had — and a press release turned a librarian into a mathematician.

Beat three — the quieter, real thing

And yet. Strip away the hype, wait a few months, and something genuine emerges from the same effort — which is what makes this a great story rather than a simple debunking. By January 2026, Terence Tao was reporting, carefully, that a small number of Erdős problems had been solved in a way that did appear new. Problem #728, he wrote, “was solved more or less autonomously by AI (after some feedback…), in the spirit of the problem…, with the result (to the best of our knowledge) not replicated in existing literature.” A couple more followed, including some formalized and checked in Lean via a system called Aristotle, and accepted by Tao himself. promising

But notice how Tao — a working mathematician, not a marketing department — frames it, because his framing is the model of calibrated thinking this course is trying to install in you. These, he stresses, are the “lowest-hanging fruit.” Erdős problems “vary widely in difficulty, by several orders of magnitude”; an “open” label “is always provisional”; and the reporting is badly biased, because the failures never get announced — the tool had already been “quietly applied to a significant fraction of the currently open Erdős problems, without notable success.” The successes are real and worth celebrating. They are also the easiest problems in the pile, solved with human feedback in the loop, with closely related results already sitting in the literature. The machine is, in Tao’s lovely phrase, “clearing out the lowest-hanging fruit and isolating the problems which are genuinely difficult.”

• Oct 2025 · the spike”GPT-5 solved 10 unsolved Erdős problems.” Announced by OpenAI figures; widely shared as a research breakthrough. hype
• Oct 2025 · the correction”A dramatic misrepresentation” — Thomas Bloom. The problems were solved years ago by humans; the AI found the existing papers. Hassabis: “embarrassing.”
• Jan 2026 · the real thingErdős #728 solved “more or less autonomously,” not in existing literature. A few more follow, some Lean-verified and accepted by Tao — but the “lowest-hanging fruit.” promising

The lesson is not “AI math is fake” — beat three is real, and may well be the leading edge of something large. The lesson is that the same underlying events produced a wildly false headline in October and a carefully true statement in January, and the only way to tell them apart was to ask who was speaking, what “solved” and “open” actually meant, and whether the result had been checked. That is the hype filter, working exactly as designed, on a live story. Hold onto the method; you’ll need it long after the specific problem numbers are forgotten.

Dispatch IV

Is any of it actually reasoning?

Underneath the benchmark scores and the headlines sits a question that is not yet answered, and that careful researchers on both sides treat as unsettled: when a model produces a chain of plausible-looking steps and lands on a correct answer, is it reasoning — or performing an extraordinarily sophisticated imitation of reasoning, pattern-matched from billions of examples? This is the modern, mechanized form of the Day 1 question about whether a system that outputs a true claim actually knows anything. And in 2024–2025 it produced one of the sharpest empirical fights in the field.

The case for “it’s pattern-matching”

The flashpoint was a pair of papers from Apple’s machine-learning group. The first, GSM-Symbolic (presented at the 2025 ICLR conference), ran a beautifully simple experiment. Take grade-school math word problems that models ace. Now change only the numbers and names — nothing about the underlying reasoning — and watch scores wobble, which they shouldn’t if the model truly understood the method. Then do something crueller: add a single sentence that is topically relevant but logically irrelevant to the problem. Performance collapsed — by up to 65%. The strongest model they tested fell from 94.9% to 63.0% the moment an innocuous red-herring clause was dropped in. The authors’ conclusion was blunt: the models “cannot perform genuine logical reasoning”; they “replicate reasoning steps from their training data.” The second paper, The Illusion of Thinking (June 2025), pushed further, reporting that on controlled puzzles like the Tower of Hanoi, the latest “reasoning” models show “complete accuracy collapse” past a certain complexity — and, eerily, start trying less as problems get harder.

The case for “not so fast”

The rebuttals were swift and, in part, fair. A widely-circulated reply — half-jokingly credited to an AI co-author — argued the Apple results were partly experimental artifacts: some “failures” were just the model running into an output-length limit mid-answer, and some puzzle instances scored as failures were mathematically unsolvable to begin with, so no system could have gotten them “right.” A neutral replication by a Spanish research group (published September 2025) landed, satisfyingly, in the middle: yes, some of the dramatic collapse was an artifact of output limits — but no, not all of it; the models genuinely did stumble as complexity rose even modestly, around the eight-disk mark. The truth, as so often on this page, is neither headline.

The twist that should worry you most

There is a third finding, less famous than the Apple fight but arguably more important, and it cuts at the foundation of trusting machine reasoning at all. When a model shows its work — the now-ubiquitous “chain of thought,” where it narrates its steps before answering — we naturally assume that narration is its reasoning. Research from Anthropic’s alignment team (2025) suggests it often isn’t. They measured how often a model’s stated reasoning actually reflected the factors driving its answer, and found faithfulness shockingly low: around 25% for one leading model, 39% for another. When the researchers slipped models a hint and the model used it, the model frequently didn’t mention having done so — constructing a plausible after-the-fact rationalization instead. The chain of thought, in other words, is not a reliable window into the machine’s actual process. It is sometimes a story the model tells about an answer it reached by other means.

Sit with what that implies for an AI “proof.” If a system hands you a step-by-step argument and the steps are not faithful to how it actually got there, then the explanation is decorative — and you are back, exactly, to the Day 1 Gettier worry: a conclusion that may be correct while its stated justification has nothing to do with why it’s correct. This is the deepest reason the Lean-verified provers of Dispatch I matter so much. They are the one corner of this whole landscape where the question “but is the reasoning real?” can be sidestepped entirely — because the kernel doesn’t read the story, it checks the proof. When you cannot trust the explanation, you verify the result. The entire frontier keeps arriving back at that single sentence.

Dispatch V

Benchmark scores need version labels

Every claim on this page ultimately rests on benchmark results, but a benchmark name alone does not identify a stable test. A usable claim should name the dataset version and tier, the model release or snapshot, the tools and scaffolding, the inference or attempt budget, and the scoring protocol. FrontierMath shows why.

In December 2024, OpenAI reported 25.2% for the then-unreleased o3 on FrontierMath_11-26-24, a version containing 180 questions. Epoch’s current model page lists the released o3 at 18.7% ± 2.3% on FrontierMath Tiers 1–3 (v1, old) and 2.1% ± 2.1% on Tier 4 (v1, old). These are not repetitions of the same experiment: the model release and problem sets differ, and the available reports do not establish identical scaffolding, reasoning settings, attempt budgets, or scoring protocols. The later figures therefore neither reproduce nor refute the 25.2% announcement. protocol-dependent

There is a separate data-governance concern. OpenAI commissioned Epoch to produce 300 core questions and 50 Tier 4 questions. Epoch says OpenAI owns the commissioned questions and had access to all statements and solutions through FrontierMath_12-04-24. Later versions added explicit holdouts: 53 core solutions in FrontierMath_02-28-25, and 20 of the 50 Tier 4 problems. Epoch announced the partnership before the o3 announcement, but says it did not clearly explain the ownership and data-access terms at that point; many contributors were unaware of those details. That asymmetry is a reason to require prominent disclosure and independently held-out evaluation. It is not, by itself, evidence that the reported score was fabricated.

Versioning matters for another reason. On June 12, 2026, Epoch released FrontierMath v2 after addressing errors in 42% of the problems. Correcting a benchmark is healthy maintenance, but it also means that v1 and v2 scores cannot be compared without qualification. The defensible conclusion is narrow: 25.2% was a reported result for one model snapshot on one dated version under one evaluation. Claims about o3’s broader or current performance need a version-matched evaluation with documented conditions.

Dispatch VI

The quieter revolutions

The AI-proving story has sucked up most of the oxygen, but four other frontiers have moved meaningfully since 2020, with less noise and — in some cases — more solidity. They round out the picture, and a couple may matter more in the long run than this year’s leaderboard.

The Continuum Hypothesis is back in play

The deepest foundational question in mathematics — Cantor’s Continuum Hypothesis, whether there is any size of infinity strictly between the integers and the real numbers — was shown by Gödel and Cohen to be independent of the standard axioms: you can neither prove it nor disprove it. For decades that looked like the end of the conversation. But W. Hugh Woodin has spent years building a candidate for a new, canonical foundation he calls Ultimate L, and in a striking reversal, recent work (with collaborators, 2024) suggests that if his central conjecture holds, the natural axiom it licenses would make the Continuum Hypothesis come out true — overturning his own earlier lean toward it being false. established as serious mathematics, but the key conjectures remain open, and others (notably Joel David Hamkins) argue the question has no single answer at all — that there is a multiverse of equally legitimate set theories. A two-thousand-year-old question about infinity is, astonishingly, still live.

A foundation where proofs compute themselves

An alternative to building mathematics on sets is to build it on types and spaces — the program of homotopy type theory (HoTT) and its “univalent foundations,” which treats equality itself as a kind of path and so brings geometry into the bedrock. Its newest incarnation, cubical type theory, finally gave this program something it long lacked: the ability to actually compute. The proof-of-concept landed in 2023, when researchers using Cubical Agda formally established a deep fact about the homotopy groups of spheres and, in the process, made the computer calculate a specific number (the so-called Brunerie number) that had resisted hand computation for years. established Still a niche relative to Lean’s set-theoretic mainstream, but a genuine glimpse of a different, more computational way to ground all of mathematics.

Turning logic back on the AI

If neural networks are going to fly planes and read scans, we would like proofs about how they behave — and a whole subfield, neural-network verification, now exists to provide them. Using techniques descended from the very formal methods that verified seL4 and CompCert (from the main lesson), tools with names like α,β-CROWN can prove mathematical guarantees about a trained network — for instance, that small perturbations to an input cannot flip its output. There is an annual competition to push these tools, and they are maturing fast. established It is a neat inversion of this whole appendix: having spent six dispatches asking whether AI can do logic, here logic is deployed to police the AI. And the dominant successful paradigm everywhere on this page — neural creativity bolted to a symbolic checker — has a name, neurosymbolic AI, and is increasingly seen as the route to systems you can actually trust.

The question that outlasts all the others

Finally, a frontier that is philosophical rather than technical, and that this whole page has been circling. A small but serious literature — Jeremy Avigad’s “Mathematics and the formal turn” (2024), work by Eamon Duede and others on knowledge “in an era of computational opacity” — asks what happens to mathematical understanding when proofs become things only machines can check. Mathematics has always wanted two goods from a proof: certainty that a thing is true, and understanding of why. The machines are now superb at delivering the first. The mathematician Alex Kontorovich has named the nightmare version: a million-line, machine-verified proof of a famous conjecture like the Riemann Hypothesis that is certainly correct and completely incomprehensible — true knowledge that explains nothing, the ultimate descendant of Day 1’s belief that is right without being understood. Whether that is a triumph or a hollowing-out of the subject is not a question any benchmark can settle. open question It is the one this dispatch leaves you holding.

Now you try

The hype filter, hands on

You’ve watched the filter applied six times. Now apply it yourself. Each card below is a real claim from the 2023–2026 frontier, drawn from the dispatches above. Decide where it lands — established, promising, or hype — then reveal the verdict and the reasoning. The aim is not a perfect score. It’s to feel the weighing become automatic.