Contribute
There are many ways to ccchallenge. Here are things you can do:
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.
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.
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 if not, to explain why. 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 in order to accept the formalisation.
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 accepting 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.
Create an account, browse the paper list, pick one that interests you, and add a formalisation link.