Starting ccchallenge.org

General
1

Hello everyone,

Iā€™m launching The Collatz Conjecture Challenge whose goal is to formalise results of the Collatz literature :slight_smile:

As a start, I used Opus 4.6 to formalise BohmSontacchi1978, and this formalisation needs to be audited (currently doing it but alternative audits are welcome of course!).

The following links explain the method and ways to contribute: method and contribute

Feebdack & contributions welcome :slight_smile:

(Also, I reference Collatz World in the story related link section :slight_smile: )

3 Likes
2

Fantastic! A great topic for formalized math, and great timing with the rapidly rising intelligence of proof assistants!

1 Like