|
Size: 4571
Comment:
|
Size: 5280
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 21: | Line 21: |
| .p02 [[ | ]] .p02 [[ | ]] .p02 [[ | ]] .p02 [[ | ]] .p02 [[ | ]] |
.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 |
| Line 160: | Line 160: |
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
- 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 in Austin Texas
- p028 . Math objective, but problem importance is subjective
- p035