Timeline for A complete formalization of EGA in Lean
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 8, 2019 at 21:31 | history | edited | David Loeffler | CC BY-SA 4.0 |
deleted 4 characters in body
|
| Jun 8, 2019 at 19:37 | comment | added | arsmath | I follow the advances in machine learning and formal theorem proving, and I think there is no chance of this project succeeding unless somebody invested literally a billion dollars in it. | |
| Jun 8, 2019 at 18:07 | comment | added | Piotr Achinger | @AsuraPath not really, no. | |
| Jun 8, 2019 at 16:00 | comment | added | user141498 | @PiotrAchinger just out of curiosity, Dr. Achinger, I think you are an arithmetic geometer with some interests outside of that area. Have you been following the recent advances in machine learning, automation and formal theorem proving closely? I find it very hard to imagine somebody could come across this paper when not thinking specifically about the question in the OP. | |
| Jun 8, 2019 at 15:55 | history | edited | David Loeffler | CC BY-SA 4.0 |
added 207 characters in body
|
| Jun 8, 2019 at 15:49 | history | edited | David Loeffler | CC BY-SA 4.0 |
added 207 characters in body
|
| Jun 8, 2019 at 15:38 | comment | added | Piotr Achinger | This answer is misleading. Last time I checked, they haven’t made meaningful progress after writing this very bold “outline of a program”. | |
| Jun 8, 2019 at 15:06 | comment | added | user141498 | Well, when I said accessible I meant accesible to computers (as can be inferred from the second paragraph of the question). I do not think that right know computers know how to read so Stacks project is going to be problematic in this regard. It is pretty accessible to first-year grad students, on the other hand, so in that sense I agree. | |
| Jun 8, 2019 at 15:05 | comment | added | David Loeffler | Why not? "The Stacks project is an ever growing open source textbook and reference work on algebraic stacks and the algebraic geometry needed to define them. [...] he aim is to build algebraic geometry and use this in laying the foundations for algebraic stacks. The theory of commutative algebra, schemes, varieties, and algebraic spaces forms an integral part of the Stacks project." They're really starting from the ground up; I refer you to e.g. stacks.math.columbia.edu/tag/006S (the definition of a sheaf on a topological space). | |
| Jun 8, 2019 at 15:00 | comment | added | user141498 | it also appears that we are using the phrase "large chunks of algebraic geometry presented in an accessible form" in different ways (Stacks project definitely not match my usage of this phrase). So I am not sure whom you are quoting. | |
| Jun 8, 2019 at 14:59 | comment | added | user141498 | it appears they are even going further: "We outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry." They automate something we are struggling to do by hand in a single case! | |
| Jun 8, 2019 at 14:57 | history | answered | David Loeffler | CC BY-SA 4.0 |