|
Size: 4546
Comment:
|
Size: 4571
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 4: | Line 4: |
| . [[ | Kevin Harnett ]] . 2026 . 510.2856 HAR . Beaverton Library (book not stamped) | . [[ https://kevinstenhartnett.com/ | Kevin Harnett ]] . 2026 . 510.2856 HAR . Beaverton Library (book not stamped) |
| Line 162: | Line 162: |
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
- p028 . Math objective, but problem importance is subjective
- p035