Timeline for Does formalizing math require search and creativity, or is it near-mechanical?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 13 at 15:30 | comment | added | Timothy Chow | Here's a better link for Gonthier's paper: A computer-checked proof of the Four Color Theorem. | |
| May 15, 2014 at 23:35 | history | made wiki | Post Made Community Wiki by Todd Trimble | ||
| May 15, 2014 at 17:19 | comment | added | Timothy Chow | The issue of background material is very important. In Gonthier's formalization of the four-color theorem, for example, the Jordan Curve Theorem was a major issue. Formalizing the full JCT would have been a major "digression" as it were. It required considerable creativity to figure out how to work around it. See Gonthier's paper for more information. research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf Similarly, when Avigad formalized the prime number theorem, creativity was needed to find the version of the proof that would be the easiest to formalize. | |
| May 15, 2014 at 14:35 | history | edited | Jason Rute | CC BY-SA 3.0 |
added 15 characters in body
|
| May 15, 2014 at 13:17 | history | answered | Jason Rute | CC BY-SA 3.0 |