Pour les non-mathématiciens For everyone

1. C'est quoi cette histoire de Collatz ? 1. What is this Collatz story?

Imagine un jeu très simple. Tu prends n'importe quel nombre. Vraiment n'importe lequel. 7. 23. 1872. Peu importe. Imagine a very simple game. You take any number. Really any one. 7. 23. 1872. Doesn't matter.

La règle est en deux temps : The rule has two cases:

• Si ton nombre est PAIR → tu le divises par 2.If your number is EVEN → you divide it by 2.
• Si ton nombre est IMPAIR → tu le multiplies par 3, et tu ajoutes 1.If your number is ODD → you multiply by 3, and add 1.

Et tu recommences. Encore et encore. And you repeat. Again and again.

Exemple avec 6 : Example with 6:

6 (pair) → 3 (impair) → 10 (pair) → 5 (impair) → 16 → 8 → 4 → 2 → 1

On finit toujours sur 1. Toujours. It always ends on 1. Always.

La conjecture de Collatz, c'est juste une question : est-ce que ça marche pour TOUS les nombres ? The Collatz conjecture is just a question: does this work for ALL numbers?

Personne ne sait. Nobody knows.

2. Pourquoi c'est célèbre ? 2. Why is it famous?

Parce que c'est facile à comprendre, mais personne au monde n'arrive à le démontrer. Depuis presque 100 ans. Because it's easy to understand, but nobody in the world can prove it. For almost 100 years.

(Précisons.) On a vérifié sur ordinateur des nombres de plus en plus grands. Aujourd'hui, on a testé tous les nombres jusqu'à 2⁷¹ — c'est plus que le nombre d'étoiles dans la galaxie. (Let me be precise.) Computers have checked larger and larger numbers. Today we've tested all integers up to 2⁷¹ — that's more than the number of stars in our galaxy.

Et toujours, ils retombent sur 1. And they always fall back to 1.

Mais « vérifier des nombres » n'est pas « prouver que TOUS retombent ». Les maths demandent une vraie démonstration. On en a pas. Pas encore. But "checking numbers" is not "proving that ALL of them fall back". Math demands a real demonstration. We don't have one. Not yet.

Paul Erdős, un grand mathématicien hongrois, disait : « Les mathématiques ne sont pas prêtes pour ce problème. » Paul Erdős, a great Hungarian mathematician, said: "Mathematics is not yet ripe for such questions."

3. Qu'est-ce qu'on a fait ici ? 3. What did we do here?

(Et je dis « j'ai » mais c'est un travail d'équipe avec des IA et des mathématiciens — je ne marche pas seul.) (And I say "I" but it's a team effort with AIs and mathematicians — I don't walk alone.)

Ce qu'on a fait, c'est plus modeste. Mais c'est solide. What we did is more modest. But it's solid.

On a montré que SI on accepte 3 conditions techniques, ALORS on est sûr d'une chose : il n'y a pas d'autre « boucle » que celle qu'on connaît déjà (1 → 4 → 2 → 1). We showed that IF we accept 3 technical conditions, THEN we're sure of one thing: there's no other "loop" than the one we already know (1 → 4 → 2 → 1).

C'est un théorème conditionnel. Avec un grand SI au début. It's a conditional theorem. With a big IF at the start.

Les 3 conditions, en très très simplifié : The 3 conditions, very simplified:

1. Une conjecture de travail sur les bornes de Baker (un truc technique pas démontré, qu'on pose comme hypothèse explicitement)A working conjecture on Baker bounds (a technical thing not proved, which we explicitly state as a hypothesis)
2. Une vérification ordinateur (Barina 2025, jusqu'à 2⁷¹, déjà faite et reproductible)A computer verification (Barina 2025, up to 2⁷¹, already done and reproducible)
3. Un théorème publié (Hercher 2023, déjà accepté par d'autres mathématiciens)A published theorem (Hercher 2023, already accepted by other mathematicians)

C'est petit. Mais c'est carré. Et c'est vérifié par une machine (voir section suivante). It's small. But it's clean. And it's verified by a machine (see next section).

Comment on a vérifié ? How did we verify?

Trois IA différentes ont relu la preuve indépendamment : Claude (Anthropic), ChatGPT (OpenAI) et Gemini (Google). Trois cerveaux différents, trois pédigrées différents. Three different AIs read the proof independently: Claude (Anthropic), ChatGPT (OpenAI), and Gemini (Google). Three different brains, three different pedigrees.

C'est comme demander à 3 experts différents de relire un texte pour ne rien manquer. Chacun voit ce que les autres ratent. On a appelé ça la méthode Three-Key. It's like asking 3 different experts to proofread a text so nothing slips through. Each one catches what the others miss. We called this the Three-Key method.

Et pour boucler la boucle : la machine Lean 4 a tout revérifié, à la virgule près. Voir section suivante. And to close the loop: the Lean 4 machine rechecked everything, down to the comma. See next section.

4. C'est quoi Lean 4 ? 4. What is Lean 4?

Lean 4, c'est une machine ultra-pointilleuse. Imagine un correcteur d'orthographe, mais pour les preuves mathématiques. Lean 4 is an ultra-picky machine. Imagine a spellchecker, but for mathematical proofs.

Tu lui donnes ta démonstration ligne par ligne. Si une seule ligne a une erreur logique, il refuse. Tout est rouge. Tu corriges, tu recommences. You give it your proof line by line. If just one line has a logical error, it refuses. Everything turns red. You fix, you restart.

Si la machine accepte, ta preuve est correcte. À 100%. Pas « l'arbitre humain est probablement d'accord ». À 100%. If the machine accepts, your proof is correct. 100%. Not "the human reviewer probably agrees". 100%.

C'est plus fiable qu'un peer review humain (où tout le monde peut louper un détail). It's more reliable than human peer review (where everyone can miss a detail).

Notre théorème principal, no_nontrivial_cycle_phase59, a été accepté par Lean 4. C'est solide. Our main theorem, no_nontrivial_cycle_phase59, was accepted by Lean 4. It's solid.

5. Pour aller plus loin 5. Going further

Si tu veux plonger un peu plus : If you want to dive deeper:

Les liens sont rangés du plus accessible au plus technique. Tu peux t'arrêter au premier qui te parle. Links are ordered from most accessible to most technical. You can stop at the first one that speaks to you.

• La FAQ détailléeThe detailed FAQ — 12 questions sur Collatz et notre travail12 questions about Collatz and our work
• L'histoireThe story — le récit personnel du chemin parcouruthe personal narrative of the journey
• La page SyracuseThe Syracuse page — définition complète et alias internationaux du problèmefull definition and international aliases of the problem
• La preuve étape par étapeThe step-by-step proof — l'architecture détailléethe detailed architecture
• Le paper formelThe formal paper — 28 pages, soumis au Journal of Automated Reasoning (en review)28 pages, submitted to Journal of Automated Reasoning (under review)

Une dernière chose. Ce site est un document vivant. Si tu trouves une erreur, une formulation maladroite, ou si tu as une question — écris-moi sur GitHub ou via la page Équipe. One last thing. This site is a living document. If you find an error, an awkward phrasing, or have a question — write me on GitHub or via the Team page.