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 sur 1. Et avec tous les nombres qu'on a essayés jusqu'ici, aussi. It ends on 1. And so does every number tried so far.

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 » : je travaille avec l'aide d'assistants IA et, depuis juillet 2026, en collaboration ouverte avec Benjamin Macindoe.) (And I say "I": I work with the help of AI assistants and, since July 2026, in open collaboration with Benjamin Macindoe.)

Ce qu'on a fait, c'est plus modeste. What we did is more modest.

Le théorème dit : SI on accepte 3 conditions techniques, ALORS il n'y a pas d'autre « boucle » que celle qu'on connaît déjà (1 → 4 → 2 → 1). Le problème, corrigé le 2 octobre 2026 : la 3^e condition, jointe à la 2^e, dit déjà qu'il n'y a pas de très grande boucle. Ce SI-là contenait donc une partie de la réponse. The theorem says: IF we accept 3 technical conditions, THEN there's no other "loop" than the one we already know (1 → 4 → 2 → 1). The problem, corrected on 2 October 2026: the 3rd condition, together with the 2nd, already says that there is no very large loop. So that IF already contained part of the answer.

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 hypothèse de travail sur les bornes de Baker (un truc technique pas démontré, plus fort que ce qui est publié, qu'on pose comme hypothèse explicitement)A working hypothesis on Baker bounds (a technical thing not proved, stronger than what is published, which we explicitly state as a hypothesis)
2. Une vérification ordinateur (Bařina 2025, jusqu'à 2⁷¹, déjà faite et publiée)A computer verification (Barina 2025, up to 2⁷¹, already done and published)
3. Une hypothèse supposée (qu'on appelle DerivedLargeKBound — pour les très grands cycles, plus de 1322 nombres impairs). On l'avait présentée comme une dérivation : c'était faux. Elle n'est démontrée nulle part, et avec la condition 2 elle dit déjà qu'il n'y a pas de très grande boucle (erratum du 2 octobre 2026).An assumed hypothesis (called DerivedLargeKBound — for very large cycles, more than 1322 odd numbers). We had presented it as a derivation: that was wrong. It is proved nowhere, and together with condition 2 it already says there is no very large loop (erratum of 2 October 2026).

Ce qui reste démontré est petit. Et c'est vérifié par une machine, avec des réserves (voir section suivante). What remains proved is small. And it's checked by a machine, with caveats (see next section).

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

Des assistants IA ont relu la preuve : notamment Claude (Anthropic), et ponctuellement d'autres modèles pour des relectures croisées. AI assistants reviewed the proof: notably Claude (Anthropic), and occasionally other models for cross-review.

Ces relectures ne suffisent pas : la 3^e hypothèse contenait déjà une partie de la réponse, et ce n'est corrigé que depuis le 2 octobre 2026 (erratum public). These reviews are not enough: the 3rd hypothesis already contained part of the answer, and this was only corrected on 2 October 2026 (public erratum).

Et la machine Lean 4 a vérifié chaque étape du raisonnement, à partir des hypothèses. Mais elle ne juge pas ce que valent les hypothèses. Voir section suivante. And the Lean 4 machine checked every step of the reasoning, starting from the hypotheses. But it does not judge what the hypotheses are worth. 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, le raisonnement est correct à partir des hypothèses données — à condition que le vérificateur lui-même n'ait pas de bug (c'est arrivé : bug lean4#14576, juillet 2026). Il reste aussi à vérifier que les hypothèses ne contiennent pas déjà la réponse : c'est exactement l'erreur corrigée sur ce site le 2 octobre 2026. Notre théorème principal, no_nontrivial_cycle_phase59, a été accepté par Lean 4.27.0 ; ce qu'il démontre vraiment est expliqué dans l'erratum. If the machine accepts, the reasoning is correct from the given hypotheses — provided the checker itself has no bug (it happened: bug lean4#14576, July 2026). One must also check that the hypotheses do not already contain the answer: that is exactly the error corrected on this site on 2 October 2026. Our main theorem, no_nontrivial_cycle_phase59, was accepted by Lean 4.27.0; what it really proves is explained in the erratum.

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.

• Les cycles, en imagesThe cycles, in pictures — deux tours, quatre boucles, et pourquoi c'est si dur (page compagnon du gateway interactif de B. Macindoe)two towers, four loops, and why it's so hard (companion to B. Macindoe's interactive gateway)
• La FAQ détailléeThe detailed FAQ — 12 questions sur Collatz et notre travail12 questions about Collatz and our work
• L'histoireThe story — la chronologie de la conjecture, de 1937 à aujourd'huithe timeline of the conjecture, from 1937 to today
• 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 — preprint, DOI Zenodo 10.5281/zenodo.19790405 (la version v4 du dépôt Zenodo (20/10/2026, DOI 10.5281/zenodo.23496480) conserve le PDF d'origine et ajoute un erratum de 2 pages : voir l'erratum)preprint, Zenodo DOI 10.5281/zenodo.19790405 (version v4 of the Zenodo record (20 October 2026, DOI 10.5281/zenodo.23496480) keeps the original PDF and adds a 2-page erratum: see the erratum)

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.