Proof Jenga
a game for “Math 2.0”

Proof Jenga

Here are six proofs that there are infinitely many primes, each one checked by the Lean proof assistant. They stand on a tower of ideas from Lean's math library, Mathlib. Pull an idea out and watch which proofs fall.

The tower

Tap a block to pull it out
logic

The proofs

What the tower shows

    Why play this

    In October 2026 Terence Tao gave a public lecture at Caltech called “Math 2.0”. His argument is that AI has made proofs cheap. Mathematics used to run on proof scarcity, and now it has proof abundance. When proofs are cheap, a solved problem is no longer the prize. What matters is understanding: why a proof works, what it really needs, and what else it could prove.

    One of the experiments he suggested is exactly this game. A student of his took a proof, blocked one of the results it used, and asked for a new proof. Then two results. Then a weaker model.

    “Now that proofs are cheap, we don’t need to stop at one proof of theorem. We can have many.”Terence Tao, Math 2.0, AIM Public Lecture, Caltech, 9 Oct 2026, at 44:00 (auto-captions)

    Proof Jenga does the bookkeeping half of that experiment for one of the oldest theorems there is. Each proof's dependencies are not hand-labelled. They are read out of the proof terms Lean actually checked, so when a proof falls, it really did use that block, and the chain of lemmas that shows why is one tap away.

    “The primary bottleneck to achieving ‘Math 2.0’ is not technology, or even institutional culture. It is imagination.”Terence Tao, Math 2.0 slides, slide 29

    How it works, and what it can't tell you

    What “uses” means. For each proof, a short Lean program walks the checked proof term and collects every definition and lemma it mentions, then every one those mention, all the way down. A proof falls when the block you pulled is anywhere in that collection. The tower is a hand-picked list of named Mathlib declarations, chosen to stand for recognisable ideas.

    “Uses” is not “needs”. A proof falls if the library's version of it happens to touch a block, even when the mathematics doesn't need it. That gap is the interesting part. Finding 2 above is an example: the gap was real, so we closed it with a rebuilt proof. A fallen proof here means “this route, as written, goes through that idea”, not “no route exists”.

    Versions. Lean 4.35.0 and Mathlib v4.35.0. The counts change as Mathlib changes, and the build recomputes them.

    Add a proof

    The tower gets more interesting with every route that avoids a block. Two open challenges:

    1. Dirichlet without Euclid. Dirichlet's theorem falls with Euclid through the same smooth-numbers lemma, further down. Proving that lemma's forward direction on its own inside Mathlib would make both the Mathlib Erdős proof and Dirichlet stand. We checked that no other route connects them to Euclid.
    2. Any proof without the axiom of choice. Euclid's argument is constructive, but every proof here reaches the axiom through some library lemma.

    The proofs live in jenga/Jenga/Proofs/. Each file proves the same statement. Add one, list it in scripts/Deps.lean and scripts/build_site.py, rebuild, and the page updates.