.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 ==== . [[ https://kevinstenhartnett.com/ | Kevin Harnett ]] . 2026 . 510.2856 HAR . Beaverton Library (book not stamped) ---- .p003 . [[ https://en.wikipedia.org/wiki/Leonardo_de_Moura | Leo de Moura ]] started [[ https://en.wikipedia.org/wiki/Lean_(proof_assistant) | Lean ]] project in 2013 .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 ]] .p009 . [[ https://en.wikipedia.org/wiki/Thomas_Callister_Hales | Tom Hales b1958 ]] 1999 [[ https://en.wikipedia.org/wiki/Institute_for_Advanced_Study | Princeton Institute for Advanced Study ]] .p009 . [[ https://en.wikipedia.org/wiki/Langlands_program | Langlands Program ]] .p010 . [[ https://en.wikipedia.org/wiki/John_Horton_Conway | John Conway ]] 1982 lecture at Cambridge University .p010 . [[ https://en.wikipedia.org/wiki/Kepler_conjecture | Kepler Conjecture ]] 1611 sphere packing density around 74% for both square and hexagonal base .p011 . Hales proves conjecture 1993-4, 300 pages in [[ https://en.wikipedia.org/wiki/Annals_of_Mathematics | Annals of Mathematics ]] "3GB worth of computer calculations"?? .p012 . in 1900 [[ https://en.wikipedia.org/wiki/Hilbert's_problems | David Hilbert 23 most important open problems in mathematics ]] includes Kepler Conjecture .p014 . [[ https://en.wikipedia.org/wiki/L%C3%A1szl%C3%B3_Fejes_T%C3%B3th | László Fejes Tóth ]] [[ https://en.wikipedia.org/wiki/Regular_Figures | 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 . [[ https://en.wikipedia.org/wiki/Mathematics,_Form_and_Function | Mathematics, Form and Function ]] by [[ https://en.wikipedia.org/wiki/Saunders_Mac_Lane | Saunders Mac Lane ]] (indexed "Mac Lane") .p019 . Four years later, peer reviews barely started .p020 . [[ https://en.wikipedia.org/wiki/Proof_assistant | 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 [[ http://www.proof-technologies.com/flyspeck/ | Flyspeck Project ]] .p023 . [[ https://books.google.com/books/about/Dense_Sphere_Packings.html?id=ROQYof3dOrYC | Dense Sphere Packings: A Blueprint for Formal Proofs ]] 286 page book .p024 . two available ITPs [[ https://sketis.net/isabelle | Isabelle ]] and [[ https://en.wikipedia.org/wiki/HOL_Light | HOL Light ]] .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 ]] .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 [[ https://en.wikipedia.org/wiki/SRI_International | 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 . [[ https://yices.csl.sri.com/ | Yices ]] [[ https://en.wikipedia.org/wiki/Satisfiability_modulo_theories | SMT solver ]]Dr. Christian Puritz .p030 . [[ https://en.wikipedia.org/wiki/Automated_theorem_proving | Automated theorem proving ]] ATP .p031 . [[ https://www.microsoft.com/en-us/research/ | Microsoft Research ]] Thomas Ball .p031 . [[ https://en.wikipedia.org/wiki/Trustworthy_computing | Trustworthy Computing Initiative in 2002 ]] .p032 . de Moura joins Microsoft in August 2006 .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 . ZFC: '''Z'''ermelo-'''F'''raenkel set theory with the [[ https://en.wikipedia.org/wiki/Axiom_of_choice | axiom ]] of '''ch'''oice .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 .p042 . [[ https://en.wikipedia.org/wiki/Satisfiability | satisfiability (SAT) ]] solvers .p043 . [[ https://en.wikipedia.org/wiki/Satisfiability_modulo_theories | Satisfiability Modulo Theories (SMT) ]] .p047 . Interactive Theorem Provers (ITPs): [[ https://en.wikipedia.org/wiki/Rocq | Coq 1989 ]] [[ https://en.wikipedia.org/wiki/Agda_(programming_language) | Agda 1999 ]] [[ https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) | Isabelle 1986 ]] [[ https://en.wikipedia.org/wiki/HOL_Light | HOL Light 1991 ]] .p052 . [[ https://en.wikipedia.org/wiki/Jeremy_Avigad | Jeremy Avigad ]] at [[ https://en.wikipedia.org/wiki/Carnegie_Mellon_University | Carnegie Mellon University ]] .p055 . Grant Passmore at [[ https://www.imandra.ai/about | Imandra AI ]] .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 ]] .p059 . [[ https://en.wikipedia.org/wiki/Goldbach%27s_conjecture | Goldbach's conjecture ]] all even numbers greater than two can be written as the sum of two primes .p060 . [[ https://en.wikipedia.org/wiki/Law_of_excluded_middle | law of the excluded middle ]] .p063 . [[ https://en.wikipedia.org/wiki/Lean_(proof_assistant) | Lean ]] helper programs called tactics .p065 . 2015 Lean 2 .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 ]] .p076 . [[ https://scholar.google.com/citations?user=yaSqFaEAAAAJ&hl=en | Daniel Selsam ]] [[ https://en.wikipedia.org/wiki/David_L._Dill | David Dill ]] .p076 . [[ https://people.ciirc.cvut.cz/~urbanjo3/ | Josef Urban ]] .p078 . [[ https://adam.chlipala.net/ | Adam Chlipala ]] at MIT .p079 . [[ https://gebner.org/ | Gabriel Ebner ]] .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 . [[ | 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