Timeline for A global mathematics library
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 17, 2020 at 2:21 | comment | added | Alexander Woo | Some old theorems generalized to (at least some of) the new class of objects by doing the 'obvious' translation to the new language; some generalized but required genuinely new proofs; some remained true only for the 'classical' objects (redefined). In which cases do we have the "same theorem"? | |
| Jul 17, 2020 at 2:20 | comment | added | Alexander Woo | "Same theorem" is much more of a problem than you think. Let me point out one particularly problematic situation. The foundations of algebraic geometry were completely redone in the 1960s by Grothedieck and others, to the extent that modern algebraic geometers find it very hard to read the standard text of Hodge and Pedoe from the 1950s. A much broader class of objects was introduced, and the objects previously studied were redefined in a different way. (continued) | |
| Jul 16, 2020 at 19:57 | answer | added | Daniel Shapero | timeline score: 3 | |
| Jul 16, 2020 at 8:27 | comment | added | Valentin | First one needs a good strategy how to store statements. One this is defined the aggregating process and linking by ML and the user friendly search engine frontend can be independent and more and more improved over the years. | |
| Jul 16, 2020 at 8:25 | comment | added | Valentin | I am aware that there is sometimes no unique formulation of a theorem. That is not a problem. A perfect system/database would try to just capture exactly in a machine-readable form how a textbook states a theorem. Using some ML one then aggregates similar statements (the "same") theorems and displays them in a frontend view. Maybe listing the most stated version first and referring to other formulations etc. | |
| Jul 16, 2020 at 1:37 | history | became hot network question | |||
| Jul 16, 2020 at 0:18 | comment | added | Jochen Glueck | I'm not sure whether I understand point 3 correctly: If I get it right, you would like to have a database which contains theorems, definitions, etc., and which links to articles books, etc, where they are used. I am, however, under the impression that this idea underestimates the diversity of mathematical literature, even within very specific sub-areas: For instance: What precisely is the statement of Banach's fixed point theorem? What is "the" Perron-Frobenius theorem in matrix analysis? What does the existence and uniqueness theorem for ODEs say? And these are only rather mild examples... | |
| Jul 15, 2020 at 21:20 | history | edited | David White | CC BY-SA 4.0 |
added 36 characters in body
|
| Jul 15, 2020 at 20:18 | comment | added | darij grinberg | There is slow progress towards point 5 (see various libraries that have grown around systems like Coq and Mizar), but at the moment nothing too high can grow on this field since most proof languages are too unstable and don't feel like "the right thing" (so any work done now will probably have to be painstakingly adapted in 10 years if not earlier). Most of the time, these libraries are written by humans, typically inspired by existing literature but in no way just straightforwardly translating it. Maybe AI could do this in 20 years, but even that's far from a given. | |
| Jul 15, 2020 at 19:53 | answer | added | Alexandre Eremenko | timeline score: 11 | |
| Jul 15, 2020 at 18:40 | answer | added | David White | timeline score: 25 | |
| Jul 15, 2020 at 18:10 | comment | added | Gerhard Paseman | IMU is international Mathematics Union. WDML is World Digital Mathematics Library. I think you can find the links as well or better than I can. Gerhard "Ingrid Posted About It Here" Paseman, 2020.07.15. | |
| Jul 15, 2020 at 18:05 | history | edited | Valentin | CC BY-SA 4.0 |
typo
|
| Jul 15, 2020 at 18:03 | comment | added | Valentin | So far I just found articles either analyzing existing systems or abstractly sophisticating about properties that a perfect library should have. Do you know about a recent concrete effort of building a perfect system? And can you give me a link for that IMU effort? Sounds interesting. | |
| Jul 15, 2020 at 17:43 | comment | added | Gerhard Paseman | You might look at the IMU and their efforts on WDML. Part of the idea is to archive sites like MathOverflow which show the (relatively informalized) development of mathematics in this century. Gerhard "Says 'Informalized' Is A Word" Paseman, 2020.07.15. | |
| Jul 15, 2020 at 17:33 | history | asked | Valentin | CC BY-SA 4.0 |