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 solver

• 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 . Russell and Whitehead Principia Mathematica 1910-13 type theory better

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

• p0 .

Edit conflict - other version:

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

Edit conflict - your version:

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

End of edit conflict

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

Edit conflict - other version:

• p1 .

Edit conflict - your version:

End of edit conflict

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

• p1 .

Edit conflict - other version:

Edit conflict - your version:

End of edit conflict

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

• p2 .

Edit conflict - other version:

Edit conflict - your version:

End of edit conflict