After the morning's talks about proof abundance and formalization strategy, Alex Kontorovich (Rutgers University) takes the room through something more literal: he opens Lean on his own laptop and proves a theorem in front of everyone, live. His stated goal is modest and useful — "give a little demonstration of what Lean actually is, so that we can all know what we're talking about in practice." What follows is a single small proof, built up interactively, glitches and all.
Why pair a stochastic model with a deterministic checker
Kontorovich opens with the framing that motivates the whole Lean-plus-LLM conversation running through the meeting. Large language models are stochastic — they choose next tokens out of a distribution — and they're remarkable at generating text. But mathematical certainty is deterministic: we build towers of reasoning on top of fixed logical foundations. Lean, he says, is the latest in a lineage of interactive theorem provers — his slide lists Lean's peers: Rocq, Isabelle, HOL Light, and others. (Rocq is the current name for the prover formerly called Coq, which its developers renamed "The Rocq Prover.") Lean's job is to be the "deterministic pair" to the LLM's stochastic generation — anchoring it in logical reality.
He then breaks character for a second, noting drily that what he'd just said sounded LLM-generated even though he swears he wrote it himself.
Two practical notes before the demo starts. First, Lean itself doesn't invent arguments — it only checks, line by line, whether an argument you (or an LLM) supply is logically sound and gapless. Coming up with the argument is what LLMs are good at; that's the whole reason the pairing works. Second, Lean proofs lean heavily on Mathlib, a large reusable library, so that you don't have to hand-prove "really annoying basic facts." He adds that LLMs, left alone, don't mind doing those annoying facts anyway — and will happily bloat a proof by 10,000 lines for no reason if you let them.
The limit that won't go away: semantic alignment
Before touching the keyboard, Kontorovich flags a warning tied to an earlier audience question he attributes to "Dima's question" — Dimitri Shlyakhtenko (UCLA). Even with LLMs and Lean working together, math is not "solved." Lean can certify that a supplied proof logically closes the gap (the "sorry") in a given formal statement — but it cannot tell you whether that formal statement actually means what you intended. Did you misstate a definition? Misstate the theorem itself? That gap — semantic alignment between formal statement and mathematical intent — will never be solved purely in software, in his view. You can throw LLM judges or human judges at it, but both are fallible, so pressing a button never fully closes the loop.
Picking a non-technical example
Kontorovich wanted an example accessible to non-mathematicians in the room, and he's candid about how he found it: he asked an AI for suggestions, got ten, didn't like any of them, asked for ten more, and picked one from that second batch. The result is a well-known logic puzzle, chosen because he thinks solving it formally in Lean is about as close as he can get to a non-technical illustration of what modern formal mathematics feels like day to day.
The puzzle: you're at a party. Some people shake hands, some don't. Every person has some handshake count — in his example, he shook five people's hands (five is odd), someone else shook ten (even). Claim: you can't say anything in general about how many people shook an even number of hands, but the number of people who shook an odd number of hands always turns out to be even. Right after posing it, he calls it a little parity puzzle — a natural pun on the party setting he's just laid out, since the whole argument turns on parity (odd versus even). He's explicit that the puzzle itself is easy — "frontier LLMs will solve it immediately, and small children will solve this immediately" — the difficulty is not the point; the illustration is.
He walks the natural-language proof first. Define T as the total handshake count summed across every person at the party. The key idea is that T is always even, because every individual handshake between two people increments T by exactly 2. Split people into group E (even handshake count) and group O (odd handshake count). The total contribution to T from group E must be even (sum of even numbers). Since T overall is even, the contribution from group O must also be even — but a sum of odd numbers is itself odd unless there's an even number of them being summed. So group O must contain an even number of people.
The live build: "Lean in Scratch"
With the natural-language proof in hand, Kontorovich turns to the actual demo: formalizing this in a prototype tool he describes as being developed with Jason Reed at "the Lean FRO" — confirmed by his title slide, which credits "Jason Reed of the Lean FRO," the Lean Focused Research Organization. The premise, in his words: he watches his own kids learn to code in Scratch, so the idea is to do Lean in a Scratch-like block interface. He's explicit that "this does not yet exist" as a public tool — it's running locally on his own machine for this demo.
He narrates the screen layout: the right-hand pane shows the current goal state — the theorem being proved, which starts with a "sorry" placeholder, stating that the number of odd handshakes is even. The objects in play: a "person" is left undefined (he notes that, as in any formal system, you need some undefined primitive terms, just as you need axioms); a "party" is a finite set of people; a "handshake" is a symmetric, two-argument relation on people telling you yes/no whether they shook hands; and "handshake count" is a function from each person to a natural number, defined as the cardinality of the set of people they shook hands with. "Number of odd handshakes" is then the cardinality of the set of people in the party whose handshake count is odd, and the goal is to show that quantity is even.
The only two properties recorded about the handshake relation are symmetry (if X shook Y's hand, Y shook X's) and irreflexivity — you don't shake your own hand, stated in the tool as "the handshake of X and X is false" and abbreviated on screen to `Handshake_irref`.
From there he builds the proof interactively, matching the natural-language argument step for step:
- He introduces T as a new natural number, defined as the sum over all people X in the party of their handshake count, and "pops" it into the goal state — the info pane visibly updates to include this new object.
- He states a new hypothesis — that T is even — which creates a second, separate sub-goal (its own "sorry") alongside the original one. - He pulls up a library theorem that appears on screen as `even_sum_relation_counts` — stated generally as: given a finite set and a relation on it that's symmetric and irreflexive, the sum of that relation's associated function over the set is even. He fills in the required facts — that the party is the finite set, that the handshake relation is symmetric ("handshake sym"), and that it's irreflexive via the axiom already given — and tries to apply the theorem. - The first attempt visibly fails on screen. "This is what happens when you play with technology," he says, and calls out his collaborator directly — "Jason, we got some work to do" — before noting "it has worked in the past" and moving on, leaving that sub-goal as an open "sorry" to return to.
- He defines group E as a finite subset of people (a `Finset` on type person) for whom handshake count is even, hits a second small glitch (he traces it to using a comma where something else was expected), fixes it, and confirms the tool now understands the definition. - He duplicates the same construction to define group O (odd handshake count).
- He defines TE as the sum of handshake counts over people in group E, and TO as the same sum over group O, and confirms both appear correctly in the goal/info view. - He states a new hypothesis, that T equals TE plus TO, pops it in, and now has three open sub-goals stacked up: T is even (the first, unresolved one from earlier), T = TE + TO, and the eventual main goal.
- For the T = TE + TO sub-goal, he pulls a second library theorem — named on screen `sum_eq_sum_even_add_sum_odd` — that given a party and any function on it (here, handshake count), a sum over the whole party can be broken into a sum over the even-valued elements plus a sum over the odd-valued elements. Rather than "apply," he tries "convert," and this time it works cleanly: the goal disappears and a checkmark appears.
He ties this back to an audience question — attributed to "Dan's question," from Daniel Spielman (Yale University) — about whether the process really is line-by-line: yes, he confirms, and notes that even the "specialized" library theorems he's invoking are themselves ultimately just line-by-line statements underneath, which is why leaning on Mathlib saves so much manual work.
Where it stops
Kontorovich doesn't close every sub-goal live. The final screen shows "Proof incomplete" with two goals still open (the state panel reads "2 goals," including the "T is even" step left over from the earlier glitch), and with time running short before lunch, he wraps the demonstration there: "I think in the interest of getting everyone to lunch, maybe I'll stop there."
What the session actually demonstrates, concretely, is less about the specific handshake theorem and more about the texture of interactive proof: a goal state that updates live as you introduce new objects and hypotheses, sub-goals that stack up and get resolved (or don't) one at a time, library theorems that get pulled in by name and applied to fill gaps, and — not incidentally, for a live demo — the ordinary friction of a prototype tool misbehaving in front of an audience and being worked around in real time.