A wiki for mathematical theorems
(No Ratings Yet)
Loading ...A dream I’ve had for some time is to build a wiki for mathematical proofs. It would be sort of like Stack Exchange / Quora – people would post conjectures, and the answers would be in the form of a formal proof, automatically verified by the site.
You could link to proven theorems as lemmas in your proof. A conjecture could have several different proofs. The conjectures/theorems and proofs would all be voted on, tagged, and have English text explaining the steps in addition to the logical formulation.
This site would essentially be the Wikipedia of mathematics. If successful, it will become a place where anyone can find important theorems in a specific field, or build new theorems formally from smaller building blocks, validating their correctness.
I won’t have time to build it in the very near future, but I’m juggling the idea in my head nonetheless. A few open questions:
- Do you think such a site would be useful?
- Does something like this already exists?
- Is it even practical?
- Where would you start?
- What programming language / framework would you use for this?
- Any other helpful ideas?
- And finally … do you want to collaborate with me on this?
Update – Please see also this cross-post I did to Quora. It seems the problem is a lot more complicated than I had first imagined. I wonder if it fits as a doctorate thesis…
In any case, it requires a lot of research, not just coding. Perhaps someday.
Yonatan:
There are some attempts in this direction, of course none containing the automated proof verification part. There’s mathoverflow.net which is a stack exchange-like site for research-level mathematics discussion (mathstackexchange is similar but geared towards students). For research-level discussion on theoretical computer science there’s cstheory.stackexchange.com.
There has been other attempts at (massively) collaborative mathematics, the most famous of which is probably the polymath projects – polymathprojects.org, where a math conjecture/problem is posed and anyone who wants can try and assist in proving/solving it.
Another venture, which can probably be declared dead, is the tricki – http://www.tricki.org which is a wiki that was supposed to hold a repository of mathematical arguments and techniques.
One obvious problem if you want to add the automatic verification component, is that writing the proofs in the formal language would be hard for cutting-edge mathematics, especially considering you would have to implement a lot of previous theorems and lemmas, and would probably deter users from contributing proofs. Despite what I’ve just wrote, I think that it might be interesting to suggest this idea to the polymath community.
6/10/11, 12:41ripper234:
Thanks for the pointers @Yonathan, I’ved emailed some of the Polymath admins to see where this can be posted.
I know this idea has a long way to go, even if the platform was already finished. Bootstrapping it would take some serious time … but the vision is having a really convenient tool for writing high level proofs bottom up.
I believe it can be achieved, with time, and that if wildly adopted it could boost mathematics a notch or two upwards. Imagine the possibility of formulating a proof and knowing you’ve 100% proven it, avoiding incidents like incorrect proofs for P != NP or Fermat’s Last Theorem.
Every journey starts somewhere.
6/10/11, 13:12Prime Mover:
An ambitious project, for which I wish you all the best. You might want to take a look on proofwiki in the community portal for a list of lots of math proof wikis already in existence – proofwiki is just one of many, and all are different. One of those is a meta-mathwiki dedicated as it is to math wikis – this has become the subject of several academic papers, plenty of which are in progress.
My particular dream is that proofs can be written in human-readable and editable LaTeX which would be a direct interface to a formal theorem prover. It requires that there is a certain amount of rigorous structuring of each page, and from what I can tell, very few editors want to be constrained in this. Getting an editor even to bother to read the house style rules is like plaiting diarrhoea.
6/10/11, 19:32ripper234:
@Prime – I believe that if a website would be realy intuitive and convenient, along with a lot of pre-built tools (a tome of previously proven theorems and lemmas, automatic syntax corrections/suggestions, fast auto-complete when possible, voting, …), then some researches could see the ultimate advantage of working with such a system.
Bootstrapping will, of course, take a *long time*. I’m thinking of doing this after I get “rich enough so I don’t have to work”, because I know it will take a huge amount of effort to do right, and I don’t think I could dedicate enough time for it while I still need to work for a living – and this project, being a non-profit project almost by definition, can’t really pay the bills.
6/10/11, 19:41ripper234:
BTW, I forgot to mention this, but of course every proof, statement and proof step would have a parallel, human readable text. This will not become just a huge collection of symbols! It will be a collection of pairs, each composed of a verifiable piece of logic/math, and a human readable alternate.
Together, they form proofs that are both humanly readable from top to bottom, and completely verifiable.
6/10/11, 19:44ripper234:
From @Meni:
The proofwiki community portal indeed has good links. A few highlights are http://us.metamath.org/ , which has some 16K proofs in computer-verifiable format; and the “Formalized Mathematical Proofs” systems, some (or all) of which are capable of generating proofs, not just verifying them. I think the point with such systems is that the mathematician defines some “key frames” in the proof and the software fills in the grunt details.
If you ever get something new started I’ll be happy to collaborate on it, though I doubt I’ll be able to put much time in.
11/10/11, 0:51M. A. Hanin:
Hey Ron,
The project sounds very interesting, but I can see right away the resemblance to the attempt made by the great David Hilbert at the beginning of the previous century, where mathematicians attempted to reconstruct the entire body of knowledge on the basis of axioms. Perhaps the final nail in the coffin was the work of Kurt Gödel (the incompleteness theorems), proving that any finite set of axioms is incomplete (there will always be undecidable statements, which cannot be proven nor disproven), and that every complete set of axioms is infinite. This is where we’re walking the line between mathematics, logic, and philosophy, and I find the subject very interesting.
This is why I figured the most interesting aspect of this project is modeling the domain.
I’d love to collaborate around such a project, it sounds very interesting an fun to try, but sadly it’ll be mostly for entertainment purposes rather than trying to achieve a working solution… when walking towards an unreachable destination, one might as well enjoy the journey 😉
Email or catch me at the upcoming ALT.NET tools night if you wanna discuss this further.
29/12/11, 18:17