Hi, I’m a software developer and I have an idea for a collaborate proof assistant using Coq that will help 100 mathematicians work on a proof at the same time.
Here is my idea showing the various pages of the website:
Home Page
There is a list of proofs which you can sort by solved/unsolved.
You can select one of the unsolved proofs or click on:
- Enter a new proposition - Here you can type your proposition to be solved in the Coq format. It will look at the proposition and automatically find any undefined terms and add them to the database. People can vote on most interesting propositions or downvote uninteresting ones.
Proofs Page
Once you click on an unsolved proof, it presents you with a list of unsolved sub-tasks. You can either click on one of the unsolved sub-tasks or click on:
- Suggest a new subtask for this proof - Here you can write lemma propositions for other people to solve.
Proof writing
You can take any unsolved proposition that someone has posted and try to solve it. You can reference lemmas that other people have posted. You can also partially solve it with unsolved lemmas. And then the lemmas will be added to the database for other people to solve.
Updating
People can take any lemma even if it is solved and try to write a shorter or nicer proof. You can only replace a part of a proof by a solved lemma. (There may be a voting system if there are competing proofs).
Proof Graph
This will display a handy graph of the progress of the proof linking various lemmas together.
Democracy
Anybody can submit proofs or partial proofs to the system so even an amateur could solve one of the proofs but there will be a filter button to filter only partial proofs submitted by your team-mates.
Solved
Once every part of the proof is solved, it will list all the people who contributed to the poof.
The whole thing would be completely automated in the cloud with nobody in overall control. The system could be used by many mathematicians to solve a large proof or also an AI could have a go at proving some of the simple lemmas.
What do you think of this idea? Any suggestions for improvements?
I am thinking of using jsCoq as the proof checker and a python implementation and SQL for the database.
Almost 10 years ago, when I was still a master student, I posted pretty much the same idea on my blog and tried to find someone who would support me to develop it as a PhD project: Getting thousands to millions of people working on a single mathematical proof - Théo Zimmermann
The same year, some other researchers had published the same idea and had started a project around it: [1404.6186] ProofPeer: Collaborative Theorem Proving
None of these projects happened, but for the wrong reasons:
-
I was told that Coq was not yet easy enough to use by mathematicians for my idea of collaborative mathematics to be realistic. I ended up doing a PhD thesis on a different topic, although closely related to collaboration around Coq.
-
The people from ProofPeer similarly thought that they needed a proof assistant that would be more suited to an audience of mathematicians, and lost themselves trying to reimplement one, instead of pursuing their idea.
Years after, the success of big collaborative mathematical libraries involving many mathematicians shows that the question was never whether current proof assistants were suited to a mathematical audience. Thus, I think it should not stop anyone from pursuing such ideas.
And indeed, now a new dimension could be to include AI in the process to prove simple intermediate goals.
That being said, I think anyone attempting this idea also needs to learn a bit about how to interface with Coq. jsCoq is a frontend meant to work in a web browser, it’s probably not what you need for a collaborative project, which will necessarily have a server too, where Coq can be run directly.
2 Likes
Good points @Zimmi48 , indeed, the CoREACT project aims for example to build something like this, and Flèche / coq-lsp / jsCoq 2.0 were designed from the scratch to support better collaborative workflows (already jsCoq 1.0 had a collaborative editor thanks to the efforts of Shachar)
But with jsCoq and Flèche development stopped, I am not sure where to point you at this.
1 Like
Thanks for your feedback. Yes, I think collaborative projects have been shown to work. Although from what I have seen they are mostly done using GitHub at present which means it’s not as fast or democratic as someone is in charge of accepting pull requests. This part of the project is not conceptually difficult to automate.
Not sure why jsCoq would be a bad choice? Can you explain more? Other than it being a bit slow to load. Although there are a few jsCoq interfaces online all with difference versions of jsCoq up to about version 0.16.0. (Is there a link to an online IDE running jsCoq 1.0?)
@MrProof , jsCoq would be an excellent choice, an in particular the main branch of jsCoq is using a new engine designed to ease your use case.
The main problem with jsCoq is that is not actively developed anymore.
1 Like
That’s a shame. It does seem to be a problem with these proof assistants that it is quite a niche subject and once the main people who have deep knowledge about how they work goes on to other things they become hard to maintain.
Yes, indeed I agree with your assessment.
It seems that the collaborative maths projects won’t be likely to happen in Coq-land, however stay tuned as the project may be re-taken soon by other proof assistants.