AI Proved What?

AX04 (outside OpenAI’s math catalogue), October 2026

Collatz: at least 1 in 2^2^2^163 numbers reach 1 fast?

Kenny Lau, with AxiomProver, makes Lech Mazur’s positive-proportion theorem explicit. Not a proof of the Collatz conjecture.

Play AX04: an explicit positive density for Collatz. The constant 2^2^2^163 and the orbit of 17.

7:15. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:24The claim
  3. 4:08How the proof goes
  4. 5:39Where it stands

The claim, in plain words

This is AX04. Take a positive whole number. If it is even, halve it; if it is odd, triple it and add one. Starting from 17, the paper’s example goes to 52, 26, 13, forty, and on down to one, in twelve steps. The Collatz conjecture says that every starting number reaches one. First, what this episode is not about: it is not a proof of the Collatz conjecture, and neither paper claims one. It is a theorem about a proportion of starting numbers, with a constant so small that it takes a tower of powers to write down.

This episode covers a preprint on the Hexagon server by Kenny Lau, of Axiom Math: Explicit positive lower density for the Collatz Conjecture, 71 pages, version two of October 21. Its Corollary 1.2: let D_A be 2^2^2^163. Then, for every N, at least the floor of N over D_A odd starting values below N reach one within 10.46 log n ordinary steps, and within 3.4881 log n accelerated steps, which jump from odd number to odd number. Theorem 1.3 does the same for any target t not divisible by three, with a smaller constant. The abstract says AxiomProver was used to obtain and formalize this result in Lean. The paper’s AI declaration says AxiomProver autonomously produced the mathematics and formalized it, and that Lau is accountable for the introduction and wrote the summary in Section 2.

The paper calls itself a quantitative refinement of Mazur’s construction. It says Mazur’s constants are not explicitly specified, and bounds them by a tower of seven twos topped by 173; Mazur’s own abstract says his constants are specified by finite arithmetic expressions. Axiom’s tower has three twos. Now, how small is one over D_A? Our arithmetic. 2^163 has 50 digits. Two to that power has about 3.5 × 10^48 digits; printed at a billion digits a second, that takes about 10^32 years. D_A is two to the power of that. So for every N below D_A, which means every N anyone could write out in digits, the guarantee is zero. The paper says so: below D_A times t, the count is zero. Our computer count, and a count is not a proof: about 54% of the numbers below a million reach one within the step budget.

What it doesn’t claim

What is not claimed. Not the Collatz conjecture. Not that every number reaches one within 10.46 log n steps: in our count, 27 takes 111 steps, against a budget of 34. Not a usable proportion: Mazur’s paper says no practical numerical range is claimed for his constants, and this tower is far beyond any range we can test. And not a first: the positive proportion is Mazur’s theorem; this is a quantitative refinement, with its own Lean proof. The paper’s Corollary 1.6 is only conditional: if almost all numbers reach one, then all do; Mazur’s companion paper already has a criterion of the same kind.

Where it stands

Preprint on Hexagon
Version 1, October 14, 2026 (constant 2^2^2^87640); version 2, October 21, 2026 (2^2^2^163). Hexagon’s declarations: “A mix of human-written and AI-generated”; “Some parts of this contribution, but not all, have been checked and understood by a human.”
Independent expert review
None named in our sources.
Peer reviewed
No
Lean proof, by Axiom
AxiomMath/CollatzPositiveDensity: metadata says the Lean files were generated by AxiomProver apart from the human-written challenge file; scope Theorem 1.3, Remark 1.4 and Corollary 1.2 (not Corollary 1.6); sorry count 0; only Lean’s three standard axioms; review “author-verified” (Kenny Lau); README “locally verified with the comparator”; GitHub build check passed on all 8 commits. Not built or run by us.

Last checked October 27, 2026. Where it stands. Axiom’s repository was created on October 9; the paper followed on October 14, version two on October 21, and the last commit on October 23. The top of the tower fell from 140,214, to 87,640, to 163. Hexagon’s declaration says the text is a mix of human-written and AI-generated, and that some parts, but not all, have been checked and understood by a human. No source names an independent expert review, and it is not peer reviewed. The Lean metadata says that, apart from the human-written challenge file, AxiomProver generated the Lean files. It covers Theorem 1.3, its remark and Corollary 1.2, with no sorry and only Lean’s three standard axioms; its review is author-verified, by Lau. The README says it was locally verified with the comparator, and GitHub’s build check passed on all eight commits. Our keyword scan of its 1,050 Lean files finds sorry only in the four challenge statements. We did not build or run it.

OpenAI’s math catalogue has no Collatz result. If it holds, for every N, at least the floor of N over D_A numbers below N reach one within 10.46 log n steps: Mazur’s theorem, refined to a tower of three twos by AxiomProver with Kenny Lau, with a Lean proof we did not run, a constant far too large to test, and the conjecture itself still open.

How the proof goes

  1. History. History, as the papers tell it. Krasikov and Lagarias proved that, for large X, at least X^0.84 numbers below X reach one. Tao proved that, for any function that tends to infinity, almost every orbit, in the sense of logarithmic density, eventually falls below it; Mazur’s paper notes that this alone does not give convergence to one. Then, on September 6, twenty 26, Lech Mazur announced a positive proportion: for every large enough X, at least cX numbers below X reach one within 10.46 log n steps. His paper’s disclosure says that generative AI, OpenAI’s GPT models through Codex, contributed substantially, and that the theorem comes with a Lean formalization.
  2. Walking backwards. How the proof goes, in the paper’s outline. Walk backwards. An odd number n has odd predecessors, (2^a·n − 1)/3, whenever that is a whole number: for seven they are nine, 37, 149, and so on. A path back from the target is a word of exponents. The word four, three, two, one leads from one back to eleven. Each word gets a weight, three to its length over two to its total, which is roughly the target divided by the source. Now treat each letter as random, equal to a with chance 2^−a. The average letter is two, so each odd step multiplies a number by about three quarters, and the model predicts about 10.428 log n steps.
  3. Mixing and the seed. The key tool is a mixing lemma, in the sense of Tao: the spread of these words over residues modulo three to a large power is, on average, close to its spread at a much smaller power. With it, the proof grows a family of words, generation by generation, and shows that the errors from generation 9,853 onward add up to less than six sevenths. The method needs a seed in one residue class modulo 3^d0, where d0 is 5·2^160. The seed reaches the target in one odd step, but the paper bounds it by 2^(5·3^d0) times t, which is below D_A times t. The count shrinks as the seed grows, so the tower comes from the seed.

The numbers in the video

  • Ours: the orbit of 17 takes 12 steps (budget ⌊10.46 ln 17⌋ = 29); 27 takes 111 steps (budget 34).
  • Ours: the predecessors of 7 are 9, 37, 149, 597, 2389; the word (4, 3, 2, 1) leads from 1 back to 11, and 2^10/3^4 ≈ 12.642.
  • Ours: 1/ln(4/3) ≈ 3.476 and 3/ln(4/3) ≈ 10.428, the random model’s step counts.
  • Ours: 2^163 = 11692013098647223345629478661730264157247460343808 (50 digits); 2^(2^163) has about 3.5 × 10^48 digits; printing them at a billion digits a second would take about 10^32 years; D_A is 2 to that power, so ⌊N/D_A⌋ = 0 for every N below D_A.
  • Ours (a count, not a proof): the share of positive n below 10^2, 10^3, 10^4, 10^5, 10^6 that reach 1 within ⌊10.46 ln n⌋ steps is 83.8%, 64.4%, 56.3%, 55.3%, 54.2%.
  • Ours: the paper’s integer comparisons 3^200 < 2^317 and 4 + (317/200)·d0 < 2^163 for d0 = 5·2^160 hold; d0·log₂3 ≈ 0.99·2^163.
  • Ours (keyword scan, not an audit): Axiom’s repository has 1,050 Lean files (149,926 lines); sorry appears only in the 4 challenge statements.

Read the source

AI Proved What? is independent and not affiliated with Axiom Math, OpenAI or Lech Mazur.

Transcript

Read the full script

0:00The question

This is AX04. Take a positive whole number. If it is even, halve it; if it is odd, triple it and add one. Starting from 17, the paper’s example goes to 52, 26, 13, forty, and on down to one, in twelve steps. The Collatz conjecture says that every starting number reaches one. First, what this episode is not about: it is not a proof of the Collatz conjecture, and neither paper claims one. It is a theorem about a proportion of starting numbers, with a constant so small that it takes a tower of powers to write down. History, as the papers tell it. Krasikov and Lagarias proved that, for large X, at least X^0.84 numbers below X reach one. Tao proved that, for any function that tends to infinity, almost every orbit, in the sense of logarithmic density, eventually falls below it; Mazur’s paper notes that this alone does not give convergence to one. Then, on September 6, twenty 26, Lech Mazur announced a positive proportion: for every large enough X, at least cX numbers below X reach one within 10.46 log n steps. His paper’s disclosure says that generative AI, OpenAI’s GPT models through Codex, contributed substantially, and that the theorem comes with a Lean formalization.

1:24The claim

This episode covers a preprint on the Hexagon server by Kenny Lau, of Axiom Math: Explicit positive lower density for the Collatz Conjecture, 71 pages, version two of October 21. Its Corollary 1.2: let D_A be 2^2^2^163. Then, for every N, at least the floor of N over D_A odd starting values below N reach one within 10.46 log n ordinary steps, and within 3.4881 log n accelerated steps, which jump from odd number to odd number. Theorem 1.3 does the same for any target t not divisible by three, with a smaller constant. The abstract says AxiomProver was used to obtain and formalize this result in Lean. The paper’s AI declaration says AxiomProver autonomously produced the mathematics and formalized it, and that Lau is accountable for the introduction and wrote the summary in Section 2. The paper calls itself a quantitative refinement of Mazur’s construction. It says Mazur’s constants are not explicitly specified, and bounds them by a tower of seven twos topped by 173; Mazur’s own abstract says his constants are specified by finite arithmetic expressions. Axiom’s tower has three twos. Now, how small is one over D_A? Our arithmetic. 2^163 has 50 digits. Two to that power has about 3.5 × 10^48 digits; printed at a billion digits a second, that takes about 10^32 years. D_A is two to the power of that. So for every N below D_A, which means every N anyone could write out in digits, the guarantee is zero. The paper says so: below D_A times t, the count is zero. Our computer count, and a count is not a proof: about 54% of the numbers below a million reach one within the step budget. What is not claimed. Not the Collatz conjecture. Not that every number reaches one within 10.46 log n steps: in our count, 27 takes 111 steps, against a budget of 34. Not a usable proportion: Mazur’s paper says no practical numerical range is claimed for his constants, and this tower is far beyond any range we can test. And not a first: the positive proportion is Mazur’s theorem; this is a quantitative refinement, with its own Lean proof. The paper’s Corollary 1.6 is only conditional: if almost all numbers reach one, then all do; Mazur’s companion paper already has a criterion of the same kind.

4:08How the proof goes

How the proof goes, in the paper’s outline. Walk backwards. An odd number n has odd predecessors, (2^a·n − 1)/3, whenever that is a whole number: for seven they are nine, 37, 149, and so on. A path back from the target is a word of exponents. The word four, three, two, one leads from one back to eleven. Each word gets a weight, three to its length over two to its total, which is roughly the target divided by the source. Now treat each letter as random, equal to a with chance 2^−a. The average letter is two, so each odd step multiplies a number by about three quarters, and the model predicts about 10.428 log n steps. The key tool is a mixing lemma, in the sense of Tao: the spread of these words over residues modulo three to a large power is, on average, close to its spread at a much smaller power. With it, the proof grows a family of words, generation by generation, and shows that the errors from generation 9,853 onward add up to less than six sevenths. The method needs a seed in one residue class modulo 3^d0, where d0 is 5·2^160. The seed reaches the target in one odd step, but the paper bounds it by 2^(5·3^d0) times t, which is below D_A times t. The count shrinks as the seed grows, so the tower comes from the seed.

5:39Where it stands

Where it stands. Axiom’s repository was created on October 9; the paper followed on October 14, version two on October 21, and the last commit on October 23. The top of the tower fell from 140,214, to 87,640, to 163. Hexagon’s declaration says the text is a mix of human-written and AI-generated, and that some parts, but not all, have been checked and understood by a human. No source names an independent expert review, and it is not peer reviewed. The Lean metadata says that, apart from the human-written challenge file, AxiomProver generated the Lean files. It covers Theorem 1.3, its remark and Corollary 1.2, with no sorry and only Lean’s three standard axioms; its review is author-verified, by Lau. The README says it was locally verified with the comparator, and GitHub’s build check passed on all eight commits. Our keyword scan of its 1,050 Lean files finds sorry only in the four challenge statements. We did not build or run it. OpenAI’s math catalogue has no Collatz result. If it holds, for every N, at least the floor of N over D_A numbers below N reach one within 10.46 log n steps: Mazur’s theorem, refined to a tower of three twos by AxiomProver with Kenny Lau, with a Lean proof we did not run, a constant far too large to test, and the conjecture itself still open.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.