• 2026 Fri Oct 9 - rimuhosting flaky, editing on http://gate.kl-ic.com/ProofInCode

. http://wiki.keithl.com/ProofInCode

The Proof in the Code

How a Truth Machine Is Transforming Math and AI

• Kevin Harnett . 2026 . 510.2856 HAR . Beaverton Library (book not stamped)

• p003 . Leo de Moura started Lean project in 2013

• p004 . Kevin Buzzard Patrick Massot Johan Commelin Mario Carneiro

• p009 . Tom Hales b1958 1999 Princeton Institute for Advanced Study

• p009 . Langlands Program

• p010 . John Conway 1982 lecture at Cambridge University

• p010 . Kepler Conjecture 1611 sphere packing density around 74% for both square and hexagonal base

• p011 . Hales proves conjecture 1993-4, 300 pages in Annals of Mathematics "3GB worth of computer calculations"??

• p012 . in 1900 David Hilbert 23 most important open problems in mathematics includes Kepler Conjecture

• p014 . László Fejes Tóth Regular Figures

• p015 . Hales 1760 cases of ball arrangement, cluster of Sun workstations
• p016 . early 1998 eliminated all but fifty arrangements, 30 in spring, 19 in June, down to one by July 4

• p019 . Mathematics, Form and Function by Saunders Mac Lane (indexed "Mac Lane")

• p019 . Four years later, peer reviews barely started

• p020 . ITP Interactive Theorem Prover aka Proof Assistant

• p021 . Writing formal language ITP proof takes orders of magnitude longer than by hand

• p023 . Mechanically checkable form Flyspeck Project

• p023 . Dense Sphere Packings: A Blueprint for Formal Proofs 286 page book

• p024 . two available ITPs Isabelle and HOL Light

• p025 . Microsoft Research Leo de Moura born 1971 Rio de Janeiro

• p027 . March 1989 Pontifical Catholic University of Rio de Janeiro

• p027 . internship at Semantic Designs (est 1993? 2026 dead link) in Austin Texas
• p028 . Math objective, but problem importance is subjective

• p028 . SRI 1946 now SRI International

• p029 . LATEX, Siri
• p029 . 2001 Symbolic Analysis Laboratory . SAL
• p030 trace expressed as formula for all conditions that result in bad state???

• p030 . Yices SMT solverDr. Christian Puritz

• p030 . Automated theorem proving ATP

• p031 . Microsoft Research Thomas Ball

• p031 . Trustworthy Computing Initiative in 2002

• p032 . de Moura joins Microsoft in August 2006

• p033 . Microsoft ATPs, Zaputo, Zap, Z3

• p033 . SMT-COMP

• p035 . 2013, de Moura proposes new interactive theorem prover

• p036 . Ramon Llull Wheel of 16 divine attributes

• p037 . Leibniz characteristica universalis

• p037 . calculus ratiocinator

• p038 . Leibniz - Art of Discovery

• p040 . Ernst Zermelo Abraham Fraenkel formal system to express all mathematics as sets

• p041 . ZFC: Zermelo-Fraenkel set theory with the axiom of choice

• p041 . Russell and Whitehead Principia Mathematica 1910-13 type theory better

• p042 . satisfiability (SAT) solvers

• p043 . Satisfiability Modulo Theories (SMT)

• p047 . Interactive Theorem Provers (ITPs): Coq 1989 Agda 1999 Isabelle 1986 HOL Light 1991

• p052 . Jeremy Avigad at Carnegie Mellon University

• p055 . Grant Passmore at Imandra AI

• p058 . Rob Lewis

• p058 . Soonho Kong now at AWS

• p058 . Georges Gonthier

• p059 . Goldbach's conjecture all even numbers greater than two can be written as the sum of two primes

• p060 . law of the excluded middle

• p063 . Lean helper programs called tactics

• p065 . 2015 Lean 2

• p071 . Floris van Doorn

• p075 . Metamath proof assistant

• p075 . Norman Megill . Metamath website

• p076 . Daniel Selsam David Dill

• p076 . Josef Urban

• p078 . Adam Chlipala at MIT

• p079 . Gabriel Ebner

• p079 . Sebastian Ullrich

• p079 . Johannes Hölzl

• p080 . Kim Morrison

• p080 . Mike Freedman

• p081 . Armaël Guéneau

• p083 . Jared Roesch

• p088 . gitter instant messaging platform used by early Lean community

• p090 . Big Proof conference 2017 @ Newton Institute, Cambridge

• p091 . Vladimir Voevodsky

• p092 . teacher Dr. Christian Puritz

• p094 . Dots and Boxes game

• p095 . Michael Ciere

• p095 . Peter Scholze

• p095 . perfectoid space

• p097 . univalent foundations

• p098 . Georges Gonthier's formal proof of the odd order theorem

• p099 . Flyspeck Project 2003

• p099 . Ngô Bảo Châu

• p100 . Hoang Le Truong

• p101 . Naratajan Shankar

• p101
• p1
• p1

• p113 .

• p113 .

• p113 .

• p113 .

• p114 .

• p1 .

• p147 .

• p1 .

• p163 .

• p168 .

• p168 .

• p169 .

• p170 .

• p171 .

• p172 .

• p172 .

• p174 .

• p175 .

• p175 .

• p176 .

• p177 .

• p178 . http://wiki.keithl.com/ProofInCode

• p178 . https://en.wikipedia.org/wiki/Abraham_Fraenkel

• p179 .

• p180 .

• p181 .

• p183 .

• p184 .

• p184 .

• p185 .

• p185 .

• p185 .

• p186 .

• p187 .

• p187 .

• p188 .

• p188 .

• p188 .

• p188 .

• p189 .

• p189 .

• p190 .

• p190 .

• p191 .

• p191 .

• p192 .

• p196 .

• p198 .

• p200 .

• p200 .

• p207 .

• p209 .

• p210 .

• p211 .

• p212 .

• p213 .

• p213 .

• p214 .

• p217 .

• p217 .

• p219 .

• p220 .

• p221 .

• p221 .

• p222 .

• p222 .

• p223 .

• p223 .

• p223 .

• p225 .

• p225 .

• p229 .

• p229 .

• p229 .

• p230 .

• p231 .

• p231 .

• p232 .

• p232 .

• p235 .

• p235 .

• p236 .

• p237 .

• p238 .

• p239 .

• p240 .

• p241 .

• p241 .

• p242 .

• p242 .

• p242 .

• p243 .

• p243 .

• p243 .

• p244 .

• p244 .

• p246 .

• p247 .

• p247 .

• p248 .

• p248 .

• p249 .

• p250 .

• p250 .

• p250 .

• p251 .

• p252 .

• p252 .

• p253 .

• p254 .

• p255 .

• p257 . A Lean Proof for the Infinitude of Primes