|
Size: 5280
Comment:
|
Size: 6258
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 6: | Line 6: |
| .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/sphere-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/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 ]] .p027 internship at [[ | Semantic Designs ]] in Austin Texas |
.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/sphere-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/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 ]] .p027 . internship at Semantic Designs (est 1993? 2026 dead link) in Austin Texas |
| Line 29: | Line 29: |
| .p03 [[ | ]] .p033 [[ | ]] |
.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 ]] .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 . 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 ]] |
| Line 32: | Line 40: |
| .p035 .p03 [[ | ]] .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 [[ | ]] .p0 [[ | ]] .p0 [[ | ]] .p0 [[ | ]] .p0 [[ | ]] .p0 [[ | ]] |
.p035 . .p03 . [[ | ]] .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 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] .p0 . [[ | ]] . .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 . [[ | ]] |
| Line 71: | Line 120: |
| .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 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] .p2 [[ | ]] |
.p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] .p2 . [[ | ]] |
| Line 159: | Line 154: |
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
- p035 .
.