Event

Harvard Science Book Talks — Kevin Hartnett, The Proof in the Code

Hosts

Harvard Book Store, Harvard University Division of Science, Harvard Library

When

Tuesday, 2026-12-01, 18:00 ET

Where

Hall B, Harvard Science Center, 1 Oxford Street, Cambridge, MA 02138

Admission

RSVP required. Free, or a "Book-Included" ticket. The book is picked up at the venue that night only, not at the store beforehand; unclaimed copies are held at Harvard Book Store for 30 days after.

After

book signing

Link

Event page

Title

The Proof in the Code: How a Truth Machine Is Transforming Math and AI

Publisher

Quanta Books (Simons Foundation with Farrar, Straus and Giroux); the imprint's first book

Published

2026-06-09, hardcover, 288 pp.

ISBN

978-0-374-62005-9

From the publisher and listing descriptions only. Lean started as a program at Microsoft Research, written by Leo de Moura. Mathematicians took it up as a way to have every step of a proof checked by machine; it later drew in Peter Scholze and Terence Tao, and Google DeepMind, Meta AI and others now use it for machine reasoning. The book is about how that changes the way mathematicians work, collaborate and decide what is true, and where it sits in the push toward machine intelligence. The Simons release adds Jeremy Avigad, Kevin Buzzard, Johan Commelin and Patrick Massot to the cast, and describes the truth machine of the subtitle as a guarantee that a proof is entirely correct.

• Math and technology writer: Quanta Magazine, The Atlantic, The Boston Globe, WIRED, Nautilus, Scientific American.
• Formerly Quanta's senior writer for mathematics and computer science; now listed there as a contributing writer.
• Collected in several volumes of Princeton's Best Writing on Mathematics.
• Wrote the Globe's weekly "Brainiac" column (Ideas section), 2013–2016.
• Lives in Yarmouth, Maine.

1. What does the kernel trust, and what does it not? Tactics, simp, decide and the automation are untrusted search; only the elaborated term goes through the kernel. Does the book draw that line for a general reader, and does "100 percent" survive axiom, native_decide and the compiler in the trusted base? The codec proofs here state two String lemmas as axioms — checked, conditionally.
2. How is mathlib kept correct as it grows? Its build is pinned to a Lean toolchain and takes long enough that the FreeBSD 15 note fetches the cache instead. Who reviews definitions, as opposed to proofs, and what happens when a definition is wrong but everything above it still checks?
3. AI provers: when DeepMind or Meta report a Lean proof, what exactly was checked — the statement as a human wrote it, or one the model also produced? The parity differential note tried a proof generated by AxiomProver; it is sorry-free, but the useful question was whether problem.lean says what the paper says.
4. Formalising a statement is itself a translation. Who checks it, and has Lean caught a published error in a theorem's statement rather than its proof?
5. Lean versus the lighter tools: Alloy and TLA+ find counterexamples in bounded models and never prove anything. Where does Hartnett think working programmers meet Lean — proofs about software, or only about mathematics?

Lean, run here:

• Lean 4 on FreeBSD 14 — Lean 4.23.0 fails until procfs is mounted.
• Lean 4 on FreeBSD 15 — validation on 15.0-RELEASE, with mathlib as an option.
• Lean 4.26.0 on FreeBSD 15.0-RELEASE: Parity Differential Proof — building an AI-generated proof (arXiv:2602.03722).
• Lean 4 Codec Proofs — roundtrip, injectivity and involution, with the axioms named.

Other formal methods:

• Alloy Specification Language — relational logic and a SAT solver, compared with TLA+ and Lean 4.
• TLA+ for Build Pipeline Verification — Make targets as state machines.
• Logic for Programmers: a tools comparison — nine tools on the ability-guarantee axis.

Previous Harvard Book Store event: David Weinberger, Beautiful Particulars (2026-11-10). Same bookstore as organiser; that one was an in-store author talk, not a Harvard Science Book Talk, and not at the Science Center.