Contribute
There are many ways to ccchallenge. Here are things you can do:
- Write a formalisation. Pick a paper and formalise its results in the proof assistant of your choice. We are proof-assistant agnostic (Lean, Rocq, Isabelle, Agda, etc.). You may use AI tools partially or fully (e.g. autoformalisation), but you must disclose their use and specify which model(s) you used. Once your formalisation is ready, you can mark it as "ready to be audited".
- Write an audit report. The goal of an audit report is to assess whether a formalisation faithfully captures the content of the original paper and recommend whether to accept or reject it, with argumented justification. Auditors must be different from the formalisation authors, unless the formalisation was essentially done by AI (autoformalisation). You may use AI to assist, but the human authors of the report must be 100% accountable for its content. Admins will assess the human-accountability criterion of the audit report before following its recommendations.
- Write a review. Write an informal review of a paper and link it. You can use our GitHub Discussions forum to host your review. Each paper has a Forum button that links to its discussion thread.
- Wishlist a paper. Vote on which papers should be formalised next by clicking the star button on any paper card. Papers with more votes appear higher in the list.
- Add a paper. Add papers to the database by entering their BibTeX or filling in the metadata manually. Newly added papers are included in the formalisation goal by default.
- Edit paper metadata. Help curate the bibliography by correcting titles, authors, DOIs, abstracts, and other BibTeX fields. Every paper has an Edit button.
- Link existing formalisations and reviews. If a formalisation or review already exists elsewhere, you can link it to the corresponding paper so that the community can find it.
- Suggest removing a paper from the goal. If you think a paper should not be part of the formalisation goal (e.g. duplicate, off-topic, not about the Collatz conjecture), you can suggest its exclusion and provide a reason. Admins will review and decide.
- Join the discussion. Participate in conversations on the GitHub Discussions forum and on Discord.
- Spread the word. Share the project with mathematicians, proof assistant users, and AI researchers.
Q&A
Yes. For formalisations, you may use AI tools partially or fully (e.g. autoformalisation), but you must disclose their use and specify which model(s) you used. For audit reports, you may also use AI to assist, but the human authors of the report must be 100% accountable for its content. Admins will assess this criterion before following the report's recommendations on accepting/rejecting the formalisation.
Yes.
This can be flagged by writing a review, or discovered during formalisation and/or auditing. If no results from the paper can be salvaged, it will be removed from the formalisation goal.
No. Partial formalisations are welcome. You can formalise specific theorems or lemmas.
Whichever you prefer. The project is proof-assistant agnostic.
Yes. Different formalisations, possibly in different proof assistants, can coexist.