Diff for "ProofInCode"

Differences between revisions 22 and 33 (spanning 11 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 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
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

-  ⇤ ← Revision 22 as of 2026-10-09 21:30:14 → 
  Size: 9630
  Editor: KeithLofstrom
  Comment:
+   ← Revision 33 as of 2026-10-09 23:07:14 → ⇥
  Size: 12013
  Editor: KeithLofstrom
  Comment:
-Deletions are marked like this.
+Additions are marked like this.
 Line 7:
- .p004 . [[ https://en.wikipedia.org/wiki/Kevin_Buzzard | Kevin Buzzard ]] [[ https://leanprover-community.github.io/sphere-eversion/ | Patrick Massot ]] [[ https://math.commelin.net/ | Johan Commelin ]] [[ https://digama0.github.io/ | Mario Carneiro ]]
+ .p004 . [[ https://en.wikipedia.org/wiki/Kevin_Buzzard | Kevin Buzzard ]] [[ https://leanprover-community.github.io/sphehttps://en.wikipedia.org/wiki/Abraham_Fraenkelre-eversion/ | Patrick Massot ]] [[ https://math.commelin.net/ | Johan Commelin ]] [[ https://digama0.github.io/ | Mario Carneiro ]]
 Line 24:
- .p025  . [[ https://en.wikipedia.org/wiki/Microsoft_Research | Microsoft Research ]] [[ https://en.wikipedia.org/wiki/Leonardo_de_Moura | Leo de Moura ]] born 1971 Rio de Janeiro
 .p027 . March 1989 [[ https://en.wikipedia.org/wiki/Pontifical_Catholic_University_of_Rio_de_Janeiro | Pontifical Catholic University of Rio de Janeiro ]]
+ .p025  . [[ https://en.wikipedia.org/wiki/Microsoft_Research | Microsoft Research ]] [[ https://en.wikipedia.org/wihttps://www.newton.ac.uk/event/bprw01/ki/Leonardo_de_Moura | Leo de Moura ]] born 1971 Rio de Janeiro
 .p027 . March 1989 [[ https://en.wikihttps://en.wikipedia.org/wiki/Perfectoid_spacepedia.org/wiki/Pontifical_Catholic_University_of_Rio_de_Janeiro | Pontifical Catholic University of Rio de Janeiro ]]
 Line 33:
- .p030 . [[ https://yices.csl.sri.com/ | Yices ]] [[ https://en.wikipedia.org/wiki/Satisfiability_modulo_theories | SMT solver ]]
+ .p030 . [[ https://yices.csl.sri.com/ | Yices ]] [[ https://en.wikipedia.org/wiki/Satisfiability_modulo_theories | SMT solver ]]Dr. Christian Puritz
 Line 47:
- .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
+ .p041 . [[ https://en.whttps://en.wikipedia.org/wiki/Abraham_Fraenkelikipedia.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 53:
+ .p058 . [[ https://fordham.academia.edu/RobertLewis | Rob Lewis ]]
 .p058 . [[ https://soonhokong.github.io/ | Soonho Kong ]] now at AWS
 .p058 . [[ https://en.wikipedia.org/wiki/Georges_Gonthier | Georges Gonthier ]]
-Line 57:
+Line 60:
- .p075 - [[ https://en.wikipedia.org/wiki/Metamath | Metamath ]] proof assistabt
+ .p071 . [[ https://florisvandoorn.comhttps://en.wikipedia.org/wiki/Perfectoid_space/ | Floris van Doorn ]]
 .p075 . [[ https://en.wikipedia.org/wiki/Metamath | Metamath ]] proof assistant
 .p075 . [[ https://www.legacy.com/us/obituaries/bostonglobe/name/norman-megill-obituary?id=31842140 | Norman Megill ]] . [[ https://us.metamath.org/ | Metamath website ]]
-Line 60:
+Line 65:
+ .p078 . [[ https://adam.chlipala.net/ | Adam Chlipala ]] at MIT
-Line 61:
+Line 67:
- .p080 . [[  |  ]]
 .p088 . [[  |  ]]
 .p095 . [[  |  ]]

 .p0  . [[  |  ]]
+ .p079 . [[ https://www.convergentresearch.org/team/sebastian-ullrich | Sebastian Ullrich ]]
 .p079 . [[ https://www.cs.vu.nl/~jhl890/ | Johannes Hölzl ]]
 .p080 . [[ https://tqft.net/ | Kim Morrison ]]
 .p080 . [[ https://en.wikipedia.org/wiki/Michael_Freedman | Mike Freedman ]]
 .p081 . [[ https://armael.deuxfleurs.page/ | Armaël Guéneau ]]
 .p083 . [[ https://www.linkedin.com/in/jaredroesch/?isSelfProfile=false | Jared Roesch ]]
 .p088 . [[ https://gitter.im/ | gitter ]] instant messaging platform used by early Lean community
 .p090 . [[ https://www.newton.ac.uk/event/bprw01/ | Big Proof conference 2017 ]] @ Newton Institute, Cambridge
 .p091 . [[ https://en.wikipedia.org/wiki/Vladimir_Voevodsky | Vladimir Voevodsky ]]
 .p092 . teacher Dr. Christian Puritz
 .p094 . [[ https://en.wikipedia.org/wiki/Dots_and_boxes | Dots and Boxes ]] game
 .p095 . [[ https://www.ciere.com/ | Michael Ciere ]]
 .p095 . [[ https://en.wikipedia.org/wiki/Peter_Scholze | Peter Scholze ]]
 .p095 . [[ https://en.wikipedia.org/wiki/Perfectoid_space | perfectoid space ]]
 .p097 . [[ https://en.wikipedia.org/wiki/Univalent_foundations | univalent foundations ]]
 .p098 . Georges Gonthier's formal proof of the [[ https://www.researchgate.net/publication/257285461_A_Machine-Checked_Proof_of_the_Odd_Order_Theorem | odd order theorem ]]
 .p099 . [[ https://github.com/flyspeck/flyspeck | Flyspeck Project ]] 2003
 .p099 . [[ https://en.wikipedia.org/wiki/Ng%C3%B4_B%E1%BA%A3o_Ch%C3%A2u | Ngô Bảo Châu ]]
 .p100 . [[ https://sites.google.com/math.ac.vn/hoang-le-truong/home?authuser=0&pli=1 | Hoang Le Truong ]]
 .p101
 .p101
 .p1
 .p1
-Line 70:
+Line 92:
  .p113 . [[  |  ]]
-Line 94:
+Line 116:
- .p178 . [[  |  ]]
+ .p178 . [[  |  ]]https://en.wikipedia.org/wiki/Abraham_Fraenkel