Timeline for Is there a database for tracking the dependencies of mathematical theorems?
Current License: CC BY-SA 3.0
24 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 23, 2018 at 12:01 | comment | added | Peter Taylor | Do you consider Metamath to meet the "present-day mathematics" criterion? I'm not sure whether you intend that to mean that you want a database of relationships between recent results, and if so what your cut-off for "recent" is. | |
| Sep 12, 2016 at 10:55 | comment | added | Derek Elkins left SE | Realms: A Structure for Consolidating Knowledge about Mathematical Theories presents an approach (geared toward formal systems) that addresses some of the concerns about multiple proofs of the same theorem and also different presentations of the same theory. | |
| Sep 11, 2016 at 6:52 | comment | added | Chill2Macht | @RossMillikan All of the proofs are valid, so all of the proofs should be in the database. Otherwise one has the false impression that the results and the possible definitions are not all equivalent, when they are. This is exactly the case with the implicit function theorem, the inverse function theorem, and the rank theorem, given one, the other two can be proved. Since they are equivalent, and hence essentially the same, what perhaps would be more meaningful would be to collapse the corresponding cycle into a single node, at least when attempting to understand the large scale structure. | |
| Sep 10, 2016 at 23:58 | comment | added | Ross Millikan | But I think it makes it harder to think about the dependencies. If my definition of $e^x$ is the Taylor series and that is what I need for the proof at hand, I don't need any of those theorems. If my definition is the $\log x$ one, I need the theorem that the Taylor series is equivalent. I think you get forced to choose one specific set of axioms and definitions for your database, though there is disparity in the community on where to start. | |
| Sep 10, 2016 at 23:50 | comment | added | Chill2Macht | @IncnisMrsi There is an arrow from result A to result B if there exists (at least one) proof using result A to show result B is true. | |
| Sep 10, 2016 at 23:50 | comment | added | Chill2Macht | @RossMillikan I think that just means that equivalent formulations lead to directed cycles, but isn't that to be expected? I mean the Axiom of Choice is equivalent to the well-ordering principle, you can choose either one and prove the other, if you're using both, without loss of generality you only assumed one of the two -- I don't see how this is or would be a problem. Same thing with supremum property of the real numbers and the intermediate value theorem, etc. | |
| Sep 10, 2016 at 23:34 | comment | added | Ross Millikan | An example that comes up on math.stackexchange is early in analysis when you want to define $e^x$. You can define $e^x=\lim_{n \to \infty}(1+\frac xn)^n$, you can define $e^x=\sum_{n=0}^\infty \frac{x^n}{n!}$, you can define $\log x = \int_1^x \frac 1y\ dy$ with $e^x$ the inverse function of $\log x$ and probably a few more. Once you choose one, the rest become theorems. Once we prove these theorems we lose track of which definition is at the root of the tree and regard all of them as established properties of $e^x$, available for use as required. What should be in the database for this? | |
| Sep 10, 2016 at 17:37 | comment | added | Incnis Mrsi | Any two statements that are true are independent. One must define precisely what does “dependence of theorems” mean, since the number of different proofs for any theorem is unbounded. | |
| S Sep 10, 2016 at 7:37 | history | suggested | Martin Sleziak |
added (online-resources) tag; I find it relevant for the question since many of answers are online resources and this is also one of the tag somebody might use when searching for this kind of question
|
|
| Sep 10, 2016 at 7:30 | review | Suggested edits | |||
| S Sep 10, 2016 at 7:37 | |||||
| Sep 9, 2016 at 0:56 | answer | added | Joseph O'Rourke | timeline score: 18 | |
| S Sep 8, 2016 at 23:30 | history | suggested | Rodrigo de Azevedo |
Added tag to this question
|
|
| Sep 8, 2016 at 22:51 | answer | added | Joel David Hamkins | timeline score: 47 | |
| Sep 8, 2016 at 22:43 | review | Suggested edits | |||
| S Sep 8, 2016 at 23:30 | |||||
| Sep 8, 2016 at 21:42 | answer | added | Pace Nielsen | timeline score: 7 | |
| Sep 8, 2016 at 20:54 | comment | added | Paul Siegel | @NateEldredge I don't think directed cycles actually cause that much of a problem. Without directed cycles the algorithm for extracting the dependencies of a given theorem would be to recursively create a set containing all predecessors, predecessors of predecessors, etc. With directed cycles one can simply modify this algorithm by stipulating that no theorem can appear in its own dependency set. | |
| Sep 8, 2016 at 20:45 | answer | added | Timothy Chow | timeline score: 34 | |
| Sep 8, 2016 at 20:36 | comment | added | Chill2Macht | i.e. imagine that U is "Theorems" and "V" is proofs -- i.sstatic.net/KZ9eG.png | |
| Sep 8, 2016 at 20:35 | comment | added | Chill2Macht | @NateEldredge I think the key would be to make each proof a separate node, and not the theorem itself. Then one could link together all proofs of the same theorem in another structure, for example by adding for each proof an outgoing edge to the node corresponding to the result which it proves. I'm not sure if the implementation would be better to make the result/theorem nodes sinks or not, but I think it might be good to have a bipartite structure -- arrows from "Proofs" enter "Thms" and arrows from "Thms" enter "Proofs", with no arrow going to a proof from a proof or to a reslt from a result | |
| Sep 8, 2016 at 20:27 | comment | added | Chill2Macht | @JoeSilverman Yes I agree, the ideal would be to codify something like that mentioned in the question so it can be searched by computer | |
| Sep 8, 2016 at 20:08 | comment | added | Nate Eldredge | It seems like it would be made tricky by the fact that theorems may have many different proofs. Suppose Theorem A has two known proofs, one from first principles and one which uses Theorem B. Theorem B also has two known proofs, one from first principles and one which uses Theorem A. How would you represent this without having a directed cycle in your graph? | |
| Sep 8, 2016 at 19:14 | comment | added | Joe Silverman | There is an earlier MO question that appears to be similar: mathoverflow.net/questions/208855/family-tree-of-theorems?rq=1 | |
| Sep 8, 2016 at 18:12 | answer | added | Paul Siegel | timeline score: 21 | |
| Sep 8, 2016 at 17:53 | history | asked | Chill2Macht | CC BY-SA 3.0 |
