Timeline for Is there a database for tracking the dependencies of mathematical theorems?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 17, 2017 at 10:32 | comment | added | Chill2Macht | Regarding my earlier comment about Baby Rudin, it seems that Wolfram Research recently did something similar with Munkres's Topology : blog.wolfram.com/2016/12/22/… Normally I don't read the e-mails they send me but it seems like this time it was somewhat worthwhile. | |
| Sep 11, 2016 at 18:27 | comment | added | Timothy Chow | @IncnisMrsi : Rather than try to elaborate here, I think the best thing is for me to point you to the literature on reverse mathematics (which is so named precisely because of the "reversed polarity" that you noted). The standard textbook is Simpson's "Subsystems of Second-Order Arithmetic". And of course Wikipedia is a good entry point too. | |
| Sep 11, 2016 at 15:10 | comment | added | Incnis Mrsi | You formulated the “Theorem T depends on Axiom A if T is actually unprovable in the absence of A” condition ambiguously. Do you mean that, for certain class of theories, any theory obtaining T must have A as a theorem or an axiom? This indicates T ⇒ A — but it’s a “dependence” of reversed polarity, possibly equivalence (that is much stronger relation). Practically, if T ⇏ A, then we always can specially tailor such a set of axioms that T becomes a theorem while A doesn’t. | |
| Sep 9, 2016 at 0:46 | comment | added | Timothy Chow | People in the formal theorem-proving community are working on it. One estimate I have heard is that it takes about one week (40 person-hours) to formalize a page of advanced mathematics. See for example Freek Wiedijk's slides here: cse.chalmers.se/research/group/logic/TypesSS05/Extra/… The labor involved should decrease with time as people build better formalization tools, but until it is easy enough for all mathematicians to do it themselves, formalization will always lag well behind the published mathematical literature. | |
| Sep 9, 2016 at 0:42 | comment | added | Chill2Macht | @AndrásSalamon Thank you for the link -- I didn't even know this existed! Skimming over some of the pages it is now clearer to me why this is much more difficult than I previously thought | |
| Sep 8, 2016 at 22:08 | comment | added | András Salamon | @William see for instance isa-afp.org/topics.shtml for one such project. | |
| Sep 8, 2016 at 20:53 | comment | added | Chill2Macht | I would say this answers my question, because I had the latter type of dependency in mind. Why is "formalizing at least one proof of every mathematical theorem" "at least decades away"? Are people working on it at least? Would it be possible, today, to formalize one given book into such a system, say Baby Rudin for example? | |
| Sep 8, 2016 at 20:45 | history | answered | Timothy Chow | CC BY-SA 3.0 |