|
Size: 7719
Comment:
|
Size: 8308
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 46: | Line 46: |
| .p041 . ZFC: '''Z'''ermelo-'''F'''raenkel set theory with the [[ https://en.wikipedia.org/wiki/Axiom_of_choice | axiom of '''c'''hoice ]] | |
| Line 47: | Line 48: |
.p0 . [[ | ]] |
|
| Line 81: | Line 80: |
| .p0 . [[ | ]] ---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- . |
|
| Line 96: | Line 89: |
---- /!\ '''Edit conflict - your version:''' ---- .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] .p1 . [[ | ]] ---- /!\ '''End of edit conflict''' ---- |
|
| Line 117: | Line 123: |
---- /!\ '''Edit conflict - other version:''' ---- .p1 . [[ | ]] ---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- |
|
| Line 127: | Line 140: |
---- /!\ '''Edit conflict - other version:''' ---- ---- /!\ '''Edit conflict - your version:''' ---- ---- /!\ '''End of edit conflict''' ---- |
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 '''c'''hoice
p041 . Russell and Whitehead Principia Mathematica 1910-13 type theory better
![/!\](/moin_static198/modernized/img/alert.png "/!\"){kind=small}
Edit conflict - other version:
Edit conflict - your version:
End of edit conflict
Edit conflict - other version:
Edit conflict - your version:
End of edit conflict
Edit conflict - other version:
Edit conflict - your version:
End of edit conflict
Edit conflict - other version:
Edit conflict - your version:
End of edit conflict