|
Size: 9214
Comment:
|
Size: 10661
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 53: | 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 55: | Line 58: |
| .p061 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] |
.p063 . [[ https://en.wikipedia.org/wiki/Lean_(proof_assistant) | Lean ]] helper programs called tactics .p065 . 2015 Lean 2 .p071 . [[ https://florisvandoorn.com/ | 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 .p095 . [[ | ]] |
| Line 79: | Line 79: |
| ---- /!\ '''Edit conflict - other version:''' ---- .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] |
.p113 . [[ | ]] .p113 . [[ | ]] .p113 . [[ | ]] .p113 . [[ | ]] .p114 . [[ | ]] |
| Line 90: | Line 88: |
| ---- /!\ '''Edit conflict - your version:''' ---- .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] |
.p147 . [[ | ]] |
| Line 101: | Line 92: |
| ---- /!\ '''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 . [[ | ]] |
.p163 . [[ | ]] .p168 . [[ | ]] .p168 . [[ | ]] .p169 . [[ | ]] .p170 . [[ | ]] .p171 . [[ | ]] .p172 . [[ | ]] .p172 . [[ | ]] .p174 . [[ | ]] .p175 . [[ | ]] .p175 . [[ | ]] .p176 . [[ | ]] .p177 . [[ | ]] .p178 . [[ http://wiki.keithl.com/ProofInCode| ]] .p178 . [[ | ]] .p179 . [[ | ]] .p180 . [[ | ]] .p181 . [[ | ]] |
| Line 124: | Line 111: |
| ---- /!\ '''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 . [[ | ]] |
.p183 . [[ | ]] .p184 . [[ | ]] .p184 . [[ | ]] .p185 . [[ | ]] .p185 . [[ | ]] .p185 . [[ | ]] .p186 . [[ | ]] .p187 . [[ | ]] .p187 . [[ | ]] .p188 . [[ | ]] .p188 . [[ | ]] .p188 . [[ | ]] .p188 . [[ | ]] .p189 . [[ | ]] .p189 . [[ | ]] .p190 . [[ | ]] .p190 . [[ | ]] .p191 . [[ | ]] .p191 . [[ | ]] .p192 . [[ | ]] .p196 . [[ | ]] .p198 . [[ | ]] |
| Line 173: | Line 135: |
---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- |
.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 |
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
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
- p032 . de Moura joins Microsoft in August 2006
p033 . SMT-COMP
- p035 . 2013, de Moura proposes new interactive theorem prover
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
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
- p257 . A Lean Proof for the Infinitude of Primes