59
$\begingroup$

Mathematics has undergone some rather nice developments recently with the adoption of new techologies, things like on-line journals, the arXiv, this website, etc. I imagine there must be many further developments that could be quite useful.

What I'm thinking of is a website where anyone can contribute formal proofs of theorems. In particular there would be many proofs of the same theorem provided the proof is different -- like a constructive proof of Brouwer's fixed point theorem, and non-constructive proof, etc.

The idea would be to build up a large web of formal proofs, one building on another so that one could eventually do searches through this space of formal proofs to find out what the most efficient proofs are, in the sense of how many ASCII characters it would take to write-up the proof using Zermelo-Frankel set theory. One hope would be to have a big, active database of verified formal proofs. Another would be to have a webpage where you could hope to discover whether or not there are simpler proofs of theorems you know, that you may have not been be aware of.

Being a web-page there would be certain useful efficiencies -- the webpage could "compile" your proof and check to see it's valid. Being a wiki would make it relatively easy for people to contribute and build on an existing infrastructure. And you'd be free to use pre-existing proofs (provided they've been verified as valid) in any subsequent proofs. One could readily check what axioms a proof needs -- for example to what extent a proof needs the axiom of choice, and so on.

Is there any efforts towards such a development? Such a tool would hopefully function like the publishing arm of some sort of modern internet-era Bourbaki.

$\endgroup$
7
  • 16
    $\begingroup$ This would be a lot like starting the arxiv before TeX - only much harder. It's not there aren't formal proof languages, it's simply that there is no good standard of one. Unlike the situation with TeX and the arxiv, what's stopping us now is not the IT. $\endgroup$ Oct 5, 2010 at 22:17
  • 11
    $\begingroup$ It would not occur to me to measure the efficiency of a proof by counting the number of bytes needed to write it up in Zermelo-Frankel set theory. $\endgroup$ Oct 6, 2010 at 1:54
  • 1
    $\begingroup$ It's of course just one measure. BUt once you have such a proof database in place you can of course contrive all kinds of other measures. For geometric topology proofs somehow I'd imagine the complexity as more of an ordinal where ZFC primitives would count as finite ordinals, and "macroscopic" theorems like the Jordan Curve Theorem would count as infinite ordinals of some sort. $\endgroup$ Oct 6, 2010 at 2:15
  • 2
    $\begingroup$ @IvanKuckir: I'm not so sure about that. Coming up with a proof is a far more complicated (algorithmically impossible) thing. But verifying proofs, and manipulating verified proofs is something that is fairly reasonable. $\endgroup$ Mar 18, 2015 at 15:29
  • 3
    $\begingroup$ what about MetaMath? $\endgroup$ Oct 8, 2015 at 12:58

9 Answers 9

33
$\begingroup$

There are lots of sites for formal proofs, but no wiki that I am aware of.

Typical examples are:

archive of formal proofs at https://www.isa-afp.org/

Mizar http://mizar.org/

Lots of proofs are contained in the distributions of various interactive theorem provers: Isabelle, Hol, hol light, Coq, acl2 etc etc

As stated in another post, there is no agreement on foundations (formulas, axioms and rules of inference). A typical split is between classical (Hol et al.) and non-classical (Coq et al.) systems, but the differences are typically much more subtle than that. As a result all these systems are effectively unable to reuse proofs from other systems. Occasionally someone writes a translator from one system to another, but the problem here is that the translation typically does not produce a readable proof in the target system; a readable proof is necessary if the translated proof is to be maintainable. If you fix on ZFC+(maybe some other axioms), then Mizar probably has the most extensive library.

Every few years, someone proposes a big database of formal proofs, but these projects invariably die for various reasons related to the issues above. An example is the QED project:

http://en.wikipedia.org/wiki/QED_manifesto

My personal view is that constructing formal proofs, and maintaining them, is currently too difficult. Having said that, in the long run this is clearly an idea whose time will come.

$\endgroup$
1
15
$\begingroup$

Such a thing does exist; check out http://www.vdash.org/ and also this talk by Cameron Freer: http://www.youtube.com/watch?v=ZDI7L4Ya9Ms.

$\endgroup$
3
  • $\begingroup$ Thanks David. That sounds like a nice project. I watched the video but I haven't tried writing up a proof on the wiki yet. Hopefully the learning curve isn't too intense. $\endgroup$ Oct 5, 2010 at 23:52
  • 3
    $\begingroup$ If only the green on black font wouldn't hurt my eyes... $\endgroup$ Oct 6, 2010 at 12:57
  • 6
    $\begingroup$ Vdash is in principle exactly what the question asks for (and what I would also like to see) but it seems to be dormant. I have looked at it occasionally for a while, and have not seen any sign of activity. $\endgroup$ Jul 7, 2011 at 11:48
5
$\begingroup$

I think the following additional links are relevant:

http://homepages.inf.ed.ac.uk/da/mathwiki/

http://prover.cs.ru.nl/wiki.php

http://www.qedeq.org/ (sort of)

However, like David Lehavi I'm skeptical about the benefit of wikis over regular proof assistant technology. For me, the entrance barrier has always been learning the language and tactics of a proof assistant, not installing the software or adding something to the standard library (that is, I have never gotten that far, but if it's a problem, then it's a social one).

I agree with Tom Ridge that the time for a big collection of formal mathematics will come. But I think we should collect definitions, theorem statements, and proofs separately. That is, if a theorem is already widely known to be true, the proof should be optional, so it can be filled in later. A collection of formalized definitions and known facts would already be very useful, and most importantly, people working on different proofs can collaborate easily, whereas the formalization of definitions and theorem statements requires coordination. Of course, with current proof assistants, it's hard to be certain that definitions and statements are correct ...

$\endgroup$
5
$\begingroup$

I have thought about this also. It is something for a much distant future.

There is already a language that most mathematicians agree on: English. A proof wiki could perhaps start with plain text proofs, but with a very strict convention, that enables a future translation to some proof system easier. For example, see D. Zeilbergers original proof of the Alternating Sign Matrix Conjecture. It is presented in plain English, but the style is in a way that each part is easy to verify.

In one distant future, perhaps it will be possible to verify proofs written in a much more "loose" style. Thus, one could gradually make proofs in the wiki closer to being computer verifiable, at the same time as proof checkers become more and more powerful. Eventually, there is some point where proofs in this wiki can be verified.

$\endgroup$
5
$\begingroup$

As part of the MathWiki project at Radboud University Nijmegen (The Netherlands), a wiki for Mizar and for Coq-CoRN wiki were built. Concerning Brouwer's fixed-point theorem, for example, see the entry BROUWER in the Mizar wiki.

$\endgroup$
2
$\begingroup$

Perhaps what would be useful are the first steps towards semi-automatic translation. There are excellent natural language parsers which almost correctly parse a complicated mathematical sentence, after applying some tricks, as one can find experimentally by looking at the online Stanford parser. Given this, it seems conceivable that there can be at least a supervised translation into Isabelle/Isar. As Isabelle can invoke powerful deduction engines, the detail in a human paper should be good enough.

$\endgroup$
1
$\begingroup$

What I'm thinking of is a website where anyone can contribute formal proofs of theorems.

I'm currently working on openmathematics.org although nothing is live yet. It will allow projects developed with the Occam proof assistant to be packaged and published in a similar vein to http://npmjs.com. The command line tool, similar to the npm tool, is called open and should be at least partially functional later this year.

In particular there would be many proofs of the same theorem provided the proof is different -- like a constructive proof of Brouwer's fixed point theorem, and non-constructive proof, etc.

There would be nothing to stop people contributing different proofs of the same theorem and nothing to stop users choosing between them. However, all would be developed with Occam, rather than divers proof assistants.

The idea would be to build up a large web of formal proofs, one building on another so that one could eventually do searches through this space of formal proofs...

One thing I've been working on with Occam is to turn all labels and references into hyperlinks. If you click on a reference, you go straight to that theorem or axiom. If you click on a label, you get a list of all the places where it's referenced. This functionality is in place in the Occam proof assistant but could surface on the openmathematics.org site at some point, too.

Being a web-page there would be certain useful efficiencies -- the webpage could "compile" your proof and check to see it's valid.

Occam will verify proofs on the fly but there could also be a step in the publishing process that verifies the project with a tool written in a language that can be trusted, rather than JavaScript. This is far in the future, however.

Being a wiki would make it relatively easy for people to contribute and build on an existing infrastructure. And you'd be free to use pre-existing proofs (provided they've been verified as valid) in any subsequent proofs. One could readily check what axioms a proof needs -- for example to what extent a proof needs the axiom of choice, and so on.

Actually what I decided to do is allow issues in much the vein as http://github.com. They seem to be a great way to foster communication and collaboration. The openmathematics.org site will leverage the GitHub API to allow users to create issues directly, and wash the text through KaTeX to support mathematical markup.

Is there any efforts towards such a development? Such a tool would hopefully function like the publishing arm of some sort of modern internet-era Bourbaki.

Well, yes, myself. At the moment I think I have another two years work ahead of me, it's three years and counting so far. Occam is worth a look now, but isn't verifying anything yet.

$\endgroup$
5
  • $\begingroup$ Looking forward to your work! Is there any way to get notified when the site will launch? :) $\endgroup$
    – Tadashi
    Feb 28, 2018 at 19:45
  • 1
    $\begingroup$ Thanks for the support. You might have to wait years. I was thinking of starting a mailing list, though. Would you be interested in subscribing? $\endgroup$ Feb 28, 2018 at 19:51
  • $\begingroup$ Sure! What is the mailing list address? $\endgroup$
    – Tadashi
    Mar 1, 2018 at 18:32
  • 1
    $\begingroup$ I haven't set it up yet. I will do so in the coming weeks, however. I will let you know with another comment here, if that's okay. $\endgroup$ Mar 1, 2018 at 20:20
  • 1
    $\begingroup$ Hi, @Shamisen. As promised, the mailing list is now up. You can find details on Occam's home page. I will be making an announcement about the site in the next fews days. Thanks for your interest, by the way. $\endgroup$ Mar 26, 2018 at 10:08
0
$\begingroup$

This is far from timely in any sense, but since the question just popped up again, I will mention that somewhere in 2006–2008 I heard David Harvey, while we were both in grad school, getting very excited about creating exactly this. He did a nontrivial amount of legwork to set up the verifier, as I recall, but gave it up eventually. Perhaps he remembers what he came up with.

$\endgroup$
0
$\begingroup$

Not quite on the nail but well worth a mention is Thousands of Problems for Theorem Provers.

$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.