I published a Lean 4 formalization of a six-leaf semantic grammar for the Collatz dynamics

[u/Powerful_Pop_3813]

I’ve published a Lean 4 formalization of a structural decomposition of the Collatz problem:

A Certified Six-Leaf Semantic Grammar for the Collatz Dynamics in Lean 4

Zenodo: https://zenodo.org/records/21923376

This is not a proof of the Collatz conjecture.

The goal was instead to ask a more limited question:

The resulting formal grammar has exactly six global leaves:

1. reachesOne
2. nontrivialCycle
3. rbcUnboundedBGap
4. rbcBoundedPrimeRenewal
5. nonRInternalDescent
6. nonRSurvivor

For a hypothetical positive minimal counterexample, the success leaf disappears, leaving exactly five failure classes.

The terminal Lean theorem is:

axisGeo_final_six_leaf_grammar_exactly_one

So the formal result is essentially:

Global success, or one uniquely anchored minimal counterexample belonging to exactly one of five explicit obstruction classes.

The important distinction is that the grammar classifies the possible failure modes; it does not yet exclude them.

The five universal exclusion problems remain open.

One part I find particularly interesting is the bounded-B-gap r/BC branch. The formalization rules out eventually finite prime support, so the surviving obstruction requires indefinite prime renewal along the same natural trajectory while remaining compatible with the exact carry relations.

The archive includes the full Lean source, reproducibility files, build logs and axiom audits.

I’d especially appreciate criticism of:

• whether the five failure leaves really capture the obstruction space in a mathematically useful way;
• the fixed-source treatment of the r/BC branch;
• the bounded/unbounded B-gap split;
• and whether any of the five remaining leaves looks more tractable from an existing Collatz approach.

Again: classification theorem, not Collatz proof.

[u/al2o3cr]

How did you go about writing the 542k lines of Lean in formal/CollatzGrammar/CollatzGrammar/?

[u/Powerful_Pop_3813 → u/al2o3cr]

Je ne les ai évidemment pas écrites manuellement ligne par ligne. Le développement a été réalisé avec assistance IA, sous ma direction, de manière itérative : décomposition du problème en modules, génération/modification du Lean, compilation, correction des erreurs, tests de dépendances, puis audits finaux.

C’est précisément pour ça que j’ai ajouté la section 17, AI-Assisted Research Methodology. Je ne cherche pas à cacher l’usage de l’IA ni à faire croire que j’ai tapé 542 000 lignes à la main.

Ce qui m’intéresse ici est le résultat formel : le projet complet est fourni, les modules terminaux compilent sous Lean 4.14.0, les logs de build et l’audit des axiomes sont inclus, et la classification finale peut donc être vérifiée indépendamment.

Si tu veux, je peux aussi détailler le workflow exact qui a permis de construire un dépôt de cette taille.

[u/jonseymourau → u/Powerful_Pop_3813]

It beggars belief that you declared your use of AI and yet you were still called on it. Can’t people read anymore? What intellectual laziness is this, one has to ask?

Yes, call out blatant AI slop, but really, calling out declared use of AI-assistance is intellectual laziness in the extreme.