Diff for "ProofInCode"

Differences between revisions 5 and 7 (spanning 2 versions)

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 .
p0 .

$/!\$ Edit conflict - other version:

p0 .

$/!\$ Edit conflict - your version:

$/!\$ 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 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
p1 .
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

-  ⇤ ← Revision 5 as of 2026-10-09 03:43:19 → 
  Size: 6258
  Editor: KeithLofstrom
  Comment:
+   ← Revision 7 as of 2026-10-09 04:34:45 → ⇥
  Size: 7719
  Editor: KeithLofstrom
  Comment:
-Deletions are marked like this.
+Additions are marked like this.
 Line 38:
- .p033 . Microsof ATPs, Zaputo, [[ https://www.researchgate.net/publication/220896279_Zap_Automated_Theorem_Proving_for_Software_Analysis | Zap ]], [[https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/ | Z3 ]]
+ .p033 . Microsoft ATPs, Zaputo, [[ https://www.researchgate.net/publication/220896279_Zap_Automated_Theorem_Proving_for_Software_Analysis | Zap ]], [[https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/ | Z3 ]]
 .p033 . [[ https://en.wikipedia.org/wiki/Satisfiability_modulo_theories#Standardization_and_the_SMT-COMP_solver_competition | SMT-COMP ]]
 .p035 . 2013, de Moura proposes new interactive theorem prover
 .p036 . [[ https://en.wikipedia.org/wiki/Ramon_Llull | Ramon Llull ]] [[ https://plato.stanford.edu/entries/llull/#FiguQuatPhasTheiFunc | Wheel of 16 divine attributes ]]
 .p037 . [[ https://en.wikipedia.org/wiki/Gottfried_Wilhelm_Leibniz | Leibniz ]] [[ https://en.wikipedia.org/wiki/Characteristica_universalis | characteristica universalis ]]
 .p037 . [[ https://en.wikipedia.org/wiki/Calculus_ratiocinator | calculus ratiocinator ]]  
 .p038 . Leibniz - Art of Discovery
 .p040 . [[ https://en.wikipedia.org/wiki/Ernst_Zermelo | Ernst Zermelo ]] [[ https://en.wikipedia.org/wiki/Abraham_Fraenkel | Abraham Fraenkel ]] formal system to express all mathematics as [[ https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory | sets ]]
 .p041 . [[ https://en.wikipedia.org/wiki/Bertrand_Russell | Russell ]] and [[ https://en.wikipedia.org/wiki/Alfred_North_Whitehead | Whitehead ]] [[ https://en.wikipedia.org/wiki/Principia_Mathematica | Principia Mathematica ]] 1910-13 [[ Ramified types and the axiom of reducibility | type theory ]] better
-Line 40:
+Line 48:
- .p035 .
 .p03  . [[  |  ]]
 .p0   . [[  |  ]]
-Line 74:
+Line 79:
+---- /!\ '''Edit conflict - other version:''' ----
-Line 75:
+Line 82:
- .p0  . [[  |  ]]
 .p0  . [[  |  ]]
 .p0  . [[  |  ]]
+---- /!\ '''Edit conflict - your version:''' ----

---- /!\ '''End of edit conflict''' ----
-Line 153:
+Line 161:
+---- /!\ '''Edit conflict - other version:''' ----
-Line 154:
+Line 163:
+---- /!\ '''Edit conflict - your version:''' ----


---- /!\ '''End of edit conflict''' ----