Launching ccchallenge.org
I’m launching The Collatz Conjecture Challenge (ccchallenge.org), whose goal is to collaboratively formalise papers on the Collatz conjecture.
The literature on the Collatz conjecture is dense [1, 2] and stems from various parts of mathematics and computer science. I believe that formalising the results from this literature will help understand what is undisputedly known about the conjecture and, hopefully, serve as solid foundations towards making progress on the problem (see motivation).
The governance model is hopefully simple (ccchallenge.org/method):
- Anyone can add a paper to the formalisation goal
- Anyone can add a formalisation to a paper (proof assistant agnostic)
- Anyone can write an audit report on a formalisation (assessing if it’s faithful to the paper)
AI can be used but needs to be disclosed, and, for audit reports, we require that the human authors of the report are fully accountable for its conclusions.
See:
Feedback and contributions welcome :))!