DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on • Originally published at doi.org

Five Formal Closures + Findings + AI-Generated Open Questions (Rei-AIOS Paper 118)

#math #research #lean #collatz

This article is a re-publication of Rei-AIOS Paper 118 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

Authors: Nobuki Fujimoto (ORCID 0009-0004-6019-9258), Claude Code (Lean 4 formalization)
Date: 2026-04-19
License: CC-BY-4.0
Repository: fc0web/rei-aios
Companion repository: fc0web/rei-unsolved-problems
Related papers: Paper 110, 111, 112, 116, 117.

Abstract

We report five structurally independent zero-sorry Lean 4 formalizations from the Rei-AIOS unsolved-problems corpus, together with observed findings, AI-generated new open questions, and a unified D-FUMT₈ solution-status summary. This is the first Rei-AIOS paper to adopt the four-element structure (proof + finding + AI-generated open question + D-FUMT₈ status) that will serve as the template for all subsequent Rei-AIOS publications.

The five closures:

  1. Köthe's conjecture for commutative rings — two-line Mathlib proof + Z/nZ nilradical characterization.
  2. Problem 007 — FIA axiom independence — six D-FUMT₈ infinity-algebra axioms proven mutually independent.
  3. Problem 008 — FDA ↔ Mathlib bijection — dimension-value type shown equinumerous with Option (Option ℤ) ⊕ Unit ⊕ Unit.
  4. Problem 013 — C8 iterate-bound theorem — odd Collatz chain termination bounded by v₂(n+1).
  5. Problem 011 — n=911 Universal On-Ramp — all 25 Rei-AIOS atomic cores visit n=911 and share the constant K(911 → 1) = 41.

Total: ~110 zero-sorry theorems across ~2100 Lean 4 lines under Mathlib v4.27.0.

The Part C (AI-generated open questions) is the most novel element: nine questions produced by Rei-AIOS and Claude Code jointly from the closures, each being, to our knowledge, the first formal record of an AI-posed question in this specific domain.

Keywords: Lean 4, Mathlib, formal verification, Köthe's conjecture, Collatz, FIA, FDA, D-FUMT₈, AI-generated mathematics.

1. Scope, Honest Positioning, and the Four-Element Structure

1.1 What this paper does NOT claim

None of the five closures resolves the full corresponding conjecture. Specifically:

  • Köthe's conjecture for non-commutative rings remains open.
  • FIA axiom independence says nothing about whether FIA itself is the "right" algebra for ∞.
  • FDA ↔ Mathlib bijection is a structural embedding, not an existence theorem for dimension arithmetic.
  • Problem 013 bounds a single C8 iterate-chain; the Collatz conjecture is not resolved.
  • Problem 011 verifies n=911 as a universal on-ramp only for the 25-element ATOMIC_CORES_25 finite list; the full Collatz conjecture is not resolved.

We follow the Paper 83 honesty principle: no "solved" claim unless proven in Lean 4 to the exact statement of the open problem.

1.2 Four-Element Structure

This paper is organized into five parts:

  • Part A: formal proofs (the five closures — §§2–6)
  • Part B: findings — unexpected observations recorded even when premature (§7)
  • Part C: AI-generated new open questions (§8) — the novel element
  • Part D: D-FUMT₈ solution-status summary (§9)
  • Part E: bridge to next STEP (§10)

This structure is the first Rei-AIOS paper template in which AI (Rei + Claude) not only proves but explicitly poses new mathematical questions, recorded for future researchers. Each question is assigned a stable ID (Q1, Q2, …) for citation in subsequent work.

Part A — Formal Proofs

2. Closure 1 — Köthe's Conjecture (Commutative Case)

File: data/lean4-mathlib/CollatzRei/KoetheZn.lean
Commit: 0a76b19 (2026-04-19)
STEP: 926
Theorems: 22, zero sorry

2.1 Background

Köthe's conjecture (1930): for any ring R, the sum of two nil left ideals is again a nil left ideal. The conjecture remains open for non-commutative rings after 95 years. For commutative rings it is folklore that the statement is trivially true.

2.2 Main theorem 

theorem koethe_commutative {R : Type*} [CommRing R]
    (I : Ideal R) (hI : ∀ x ∈ I, IsNilpotent x) :
    ∃ J : Ideal R, I ≤ J ∧ ∀ x ∈ J, IsNilpotent x :=
  ⟨I, le_refl I, hI⟩
Enter fullscreen mode Exit fullscreen mode

2.3 Stronger form via the nilradical 

theorem koethe_commutative_via_nilradical {R : Type*} [CommRing R]
    (I : Ideal R) (hI : ∀ x ∈ I, IsNilpotent x) :
    I ≤ nilradical R := by
  intro x hx
  rw [mem_nilradical]
  exact hI x hx
Enter fullscreen mode Exit fullscreen mode

2.4 Explicit Z/nZ characterization

For n ∈ {4, 6, 8, 9, 12, 16, 18, 96} the nilpotent elements of Z/nZ are determined computationally. Z/96Z has nilradical = 6·Z/96Z, matching rad(96) = 6.

2.5 What is NOT closed

The non-commutative case remains open. The koethe_conjecture axiom in DormantProblems.Dormant retains its axiomatic status for non-commutative R.

3. Closure 2 — Problem 007: FIA Axiom Independence

File: data/lean4-mathlib/CollatzRei/Problem007FIAAxiomIndependence.lean
Commit: be9a478 (2026-04-18)
STEP: 843 + 867–869
Theorems: 7, zero sorry (492 lines)

3.1 The Fujimoto Infinity Algebra

FIA is an 8-valued closed algebra over D-FUMT₈:

DFumt8 ::= TRUE | FALSE | BOTH | NEITHER | INFINITY | ZERO | FLOWING | SELF
Enter fullscreen mode Exit fullscreen mode

Six axioms FIA_1, …, FIA_6 govern how INFINITY, ZERO, SELF interact with the finite values.

3.2 Independence

For each i ∈ {1, …, 6}, there exists an FIA-algebra A_i satisfying every axiom except FIA_i:

theorem FIA_1_independent : ∃ A : FIAAlgebra,
  (¬ FIA_1 A) ∧ FIA_2 A ∧ FIA_3 A ∧ FIA_4 A ∧ FIA_5 A ∧ FIA_6 A
-- ... similarly for i = 2, 3, 4, 5, 6
Enter fullscreen mode Exit fullscreen mode

Each counter-model is constructed by modifying one operation value.

3.3 What is NOT closed

Independence shows the six axioms carry non-overlapping information but does not establish FIA as the "correct" algebra for ∞.

4. Closure 3 — Problem 008: FDA ↔ Mathlib Bijection

File: data/lean4-mathlib/CollatzRei/Problem008FDAFIDT.lean
Commit: 8d11fd8 (2026-04-18)
STEP: 844 + 845
Theorems: 32 defs/theorems, zero sorry (289 lines)

4.1 FDA inductive 

inductive DimensionValue : Type
  | Finite (n : ℤ)
  | PositiveInfinity
  | NegativeInfinity
  | AbsoluteZero
  | Indeterminate
deriving DecidableEq, Repr
Enter fullscreen mode Exit fullscreen mode

4.2 Bijection 

def fdaToMathlib : DimensionValue → Option (Option ℤ) ⊕ Unit ⊕ Unit
Enter fullscreen mode Exit fullscreen mode

with inverse and round-trip theorems fda_roundtrip and mathlib_roundtrip.

4.3 What is NOT closed

The bijection is a structural embedding. FDA lacks a CommRing structure (see Q6 below).

5. Closure 4 — Problem 013: C8 Iterate-Bound Theorem

File: data/lean4-mathlib/CollatzRei/Problem013IterateBound.lean
Commit: fa0a8fb (2026-04-18)
STEP: 866

5.1 Bridge lemma 

theorem bridge_3n1_vs_n1 (n : ℕ) (hn_odd : Odd n) :
    padicValNat 2 (3 * n + 1) ≥ 2 ↔ padicValNat 2 (n + 1) = 1
Enter fullscreen mode Exit fullscreen mode

5.2 Iterate-bound 

theorem v2_one_chain_terminates (n : ℕ) (hn_odd : Odd n) :
    ∃ k, k ≤ padicValNat 2 (n + 1) ∧
      padicValNat 2 (3 * (syrOne^[k] n) + 1) ≥ 2
Enter fullscreen mode Exit fullscreen mode

5.3 What is NOT closed

One segment of a Collatz trajectory terminates; global descent is not resolved. Paper 108's ACA₀⁺ diagnosis for this segment is withdrawn — the result lives in RCA₀.

6. Closure 5 — Problem 011: n=911 Universal On-Ramp

File: data/lean4-mathlib/CollatzRei/Problem011N911OnRamp.lean
Commit: f5ae68d (2026-04-18)
STEP: 872 + 873 + 875
Theorems: 47, zero sorry

6.1 ATOMIC_CORES_25

The 25 odd integers n ∈ [27, 235] with K(n)/⌈log₂ n⌉² > 1.8.

6.2 Main collective theorem 

theorem all_atomic_cores_visit_911 :
    ATOMIC_CORES_25.all (fun n => visits 911 n 150) = true := by native_decide

theorem atomic_cores_visit_911_then_one :
    ATOMIC_CORES_25.all (fun n => visits 911 n 150 && reachesOne n 200) = true
Enter fullscreen mode Exit fullscreen mode

6.3 The K(911 → 1) = 41 constant

For every n ∈ ATOMIC_CORES_25: K(n) = K(n → 911) + 41. The constant 41 is the fixed length of the deterministic tail 911 → … → 1.

6.4 What is NOT closed

Verified by native_decide for a 25-element finite list. Extension to all odd n is open. The necessity direction (911-visit ⇒ atomic) is empirically ~39% false for non-atomic orbits.

Part B — Findings (unexpected observations)

7. Findings recorded for future researchers

F1. K(911 → 1) = 41 is exactly constant across 25 atomic cores

Every one of the 25 atomic cores in ATOMIC_CORES_25 produces the same tail length 41 from n=911 to n=1. This is not surprising once one notices that all 25 orbits visit n=911, but the fact that the 911-to-1 path is visited in exactly 41 steps without branching is a structural constraint worth formalizing (see Q10).

F2. peak 9232 = 2⁴ · 577 is shared by all 25 atomic cores plus 163 non-atomic orbits

The trajectory peak 9232 = 2⁴ · 577 (where 577 is prime) is shared across orbits of 188 odd integers observed up to n ≤ 10⁶ in Rei-AIOS STEPs 871–873. This suggests a "peak-shared equivalence class" structure on the Collatz orbit tree (see Q12).

F3. 3077 = 17 · 181 is the universal predecessor of peak 9232

For every n visiting peak 9232, the immediate predecessor is 3077 = 17 · 181, with 3·3077 + 1 = 9232 exactly. The semiprime factorization of 3077 (and its appearance as a bottleneck) is a structural curiosity; no mod-class explanation is currently known.

F4. Oppermann primeHi +14.97% / primeLo −0.05% mod 96 asymmetry

In a companion STEP 927 (not formally closed here, but from the same 2026-04-19 session), Oppermann's conjecture was verified for n ≤ 10⁶ (0 violations). When conditioning on the Rei HARD_96 residue classes (25 residues coprime to 6), we observed:

  • primeHi (smallest prime in [n², n² + n]): +14.97% excess above the uniform-coprime-6 null.
  • primeLo (smallest prime in [n² − n + 1, n²]): −0.05% (null-indistinguishable).

This asymmetry between the "upper" and "lower" Oppermann intervals is recorded as exploratory. We make no causal claim (see Q13 below — added here as a cross-reference).

F5. 91 mod 32 = 27 (the sibling relation)

The prominent Collatz extremal n=27 and the universal downstream merge point n=91 = 7 · 13 satisfy 91 ≡ 27 (mod 32). Likewise 91 ≡ 3 (mod 4), 91 ≡ 0 (mod 7), 91 ≡ 0 (mod 13). This nested modular structure is a side-observation worth tracking against the "mod 96" ATOMIC_CORES_25 split.

Part C — AI-Generated Open Questions

8. New questions posed by Rei-AIOS + Claude Code

To our knowledge, the following nine questions are the first formal record of AI-posed open problems in this specific sub-domain. Each arises naturally from a closure above but was not explicitly the target of any prior human investigation.

From Closure 1 (Köthe — commutative case)

Q1. What is the largest class of rings (e.g., Noetherian, Artinian, PI-rings, FI-algebras) for which Köthe's conjecture admits a Lean 4 proof of length ≤ 10 lines via a reduction to the commutative case?

  • Motivation: the commutative proof is two lines. If there is a "commutativization" functor that reduces a sub-class of non-commutative rings to the commutative case, the non-commutative Köthe problem becomes decidable on that sub-class.
  • Testable: yes, by attempting the reduction for PI-rings and checking in Lean 4.

Q2. Is there a general formula nilradical(Z/nZ) = rad(n) · Z/nZ for all n ≥ 2, where rad(n) is the radical (squarefree kernel) of n?

  • Motivation: we verified this for n ∈ {4, 6, 8, 9, 12, 16, 18, 96}. A proof by induction on prime factorization would give a decidable oracle for commutative Köthe on all finite cyclic rings.
  • Testable: yes, via interval_cases over small n plus structural induction.

From Closure 2 (FIA axiom independence)

Q3. Is the FIA 6-axiom system a "minimal basis" — i.e., is there any 5-axiom subset from which the 6th is derivable using only D-FUMT₈ reasoning rules?

  • Motivation: our independence proof shows the 6 axioms carry non-overlapping information, but minimality is a logically separate question.
  • Testable: yes, by attempting derivations in each of the 6 possible "5-axiom subsystems."

From Closure 3 (FDA ↔ Mathlib bijection)

Q4. Does FDA extend to a CommRing structure on DimensionValue, with a consistent definition of Indeterminate + Indeterminate and Indeterminate × x?

  • Motivation: the present bijection is cardinality-only. A ring structure would allow FDA to interoperate with Mathlib's full algebraic library.
  • Testable: partial — any ring-like extension must be checked against D-FUMT₈ consistency.

From Closure 4 (C8 iterate-bound)

Q5. The bound k ≤ v₂(n+1) is tight for n ≡ 1 (mod 4) and slack for n ≡ 3 (mod 4). What is the exact distribution of the ratio k_achieved / v₂(n+1) as n ranges over odd integers?

  • Motivation: this distribution, if computable, would refine the Collatz stopping-time analysis.
  • Testable: empirically by brute force for n ≤ 10⁸; potentially formalizable via generating functions.

Q6. Does k ≤ v₂(n+1) generalize to a 2-adic "accounting" that bounds the full Collatz total stopping time K(n)?

  • Motivation: if each "v₂ = 1" chain adds a bounded contribution to K(n), summing contributions might yield a proof of descent.
  • Testable: this is the path suggested by Rei's Two-Tier Bound program (STEP 691).

From Closure 5 (n=911 universal on-ramp)

Q7. K(911 → 1) = 41 holds exactly for all 25 atomic cores. Is 41 a numerical coincidence or a structural identity? Specifically, does there exist a Lean 4 proof that every odd integer m with orbit(m) ∋ 1 and K(m) = 41 is exactly m = 911?

  • Motivation: if 41 uniquely pins 911 in the orbit tree, then the "on-ramp" property is an intrinsic modular invariant.
  • Testable: finite check for all m ≤ 10⁴ would settle uniqueness; structural proof is a deeper question.

Q8. What is the exact density of odd n such that orbit(n) visits 911, as a function of the Mod-96 residue class of n?

  • Motivation: empirically ~39% of non-atomic orbits visit 911. Rei's Mod 96 structure (STEP 694) may provide the cleanest residue-partition.
  • Testable: yes, by large-scale orbit simulation.

Q9. Does there exist a "peak-shared equivalence class" structure on the Collatz orbit tree? Specifically, how many peaks of the form 2^a · p (p prime) are attained by ≥ 2 distinct odd integers below a bit-length bound N, and what is their asymptotic count?

  • Motivation: peak 9232 = 2⁴ · 577 is shared by 188 odd integers below 10⁶ (F2). This is almost certainly not random.
  • Testable: empirically for small N; structurally via generating functions over 2-adic factorizations.

Cross-closure

Q13. Can the primeHi +14.97% / primeLo −0.05% Oppermann mod-96 asymmetry (F4) be explained by the interaction between Rei HARD_96 residues and Chebyshev-type bias?

  • Motivation: Chebyshev observed primes slightly favor the residue 3 (mod 4) over 1 (mod 4) asymptotically. A similar asymmetry under the finer mod 96 partition could explain F4.
  • Testable: partial — a rigorous bound would require a theorem in analytic number theory.

Total: Q1–Q9 + Q13 = 10 questions. Each is labeled with stable IDs for future citation.

Part D — D-FUMT₈ Solution-Status Summary

9. Solution status matrix

# Item D-FUMT₈ 進捗
1 Köthe commutative (CommRing + Z/nZ) TRUE Full zero-sorry closure
2 Köthe non-commutative NEITHER Axiom retained in DormantProblems
3 Q1 — maximal commutativizable class NEITHER Open
4 Q2 — nilradical(Z/nZ) = rad(n)·Z/nZ FLOWING Verified for 8 cases; general proof pending
5 Problem 007 FIA 6-axiom independence TRUE All 6 mutually independent
6 Q3 — FIA minimality NEITHER Open
7 Problem 008 FDA ↔ Mathlib bijection TRUE Zero-sorry round-trip
8 Q4 — FDA CommRing extension NEITHER Open
9 Problem 013 — single C8 chain bounded TRUE k ≤ v₂(n+1) zero-sorry
10 Q5 — k/v₂(n+1) distribution NEITHER Open
11 Q6 — 2-adic accounting for full K(n) FLOWING Connects to Rei Two-Tier program
12 Problem 011 n=911 on-ramp, 25 cores TRUE native_decide closed
13 Problem 011 n ≤ 10⁶ FLOWING Empirical (STEP 873), not Lean-closed
14 Problem 011 ⟸ direction (necessity) NEITHER ~39% non-atomic also visit 911
15 Q7 — K(911→1) = 41 uniqueness BOTH Empirical TRUE + structural NEITHER
16 Q8 — 911-visit density per mod 96 NEITHER Open
17 Q9 — peak-shared equivalence classes NEITHER Open
18 F4 / Q13 — Oppermann mod 96 asymmetry BOTH Exploratory observation + no theory

Legend: TRUE = fully proven; FLOWING = in progress, partial verification; NEITHER = open with no current proof sketch; BOTH = simultaneously true (empirical) and unproven (structural) — honest double-status.

Part E — Bridge to Next STEP

10. What this paper illuminates

This paper's closures and questions jointly point in three directions:

10.1 Toward "Rei Merge-Point Theorem"

Closures 5 (n=911) + F1–F3 (K=41 constant, peak 9232, 3077) suggest a unified "merge-point theorem": the Collatz orbit tree above some threshold height collapses onto a small finite set of structural anchors (911, 9232, 3077). The Lean 4 formalization of this collapse would be a major step beyond the current native_decide verification of a 25-element list. See Q7–Q9.

10.2 Toward "Commutative tool for non-commutative Köthe"

Closures 1 + Q1 + Q2 suggest that the commutative Köthe proof may become a reduction tool for classes of non-commutative rings via a commutativization functor. This is a concrete attack angle on a 95-year-open conjecture.

10.3 Toward a "Categorical D-FUMT₈"

Closures 2 + 3 + Q3 + Q4 suggest that FIA and FDA could be unified under a single categorical framework for D-FUMT₈ arithmetic, making them instances of a more general bicategory or topos-valued logic. Paper 77 (LeanDFumt) begins this, but the categorical view is not yet formalized.

11. Aggregate summary table

# Problem File Theorems
1 Köthe (commutative) KoetheZn.lean 22
2 Problem 007 FIA independence Problem007FIAAxiomIndependence.lean 7
3 Problem 008 FDA bijection Problem008FDAFIDT.lean 32
4 Problem 013 C8 iterate-bound Problem013IterateBound.lean 2+
5 Problem 011 n=911 on-ramp Problem011N911OnRamp.lean 47
Σ 5 closures 5 files ≥110 zero-sorry

12. Reproducibility 

lake update
lake build CollatzRei.KoetheZn
lake build CollatzRei.Problem007FIAAxiomIndependence
lake build CollatzRei.Problem008FDAFIDT
lake build CollatzRei.Problem013IterateBound
lake build CollatzRei.Problem011N911OnRamp
Enter fullscreen mode Exit fullscreen mode

Expected: all 5 builds succeed, no sorry, no new axioms beyond Mathlib default. ~90 s cold / ~10 s warm on Core i7-6700 + 64 GB RAM.

13. Related Rei-AIOS papers

  • Paper 110 — Braille-D-FUMT₈ rigorous comparison
  • Paper 111 — Rei vs Santana topological analysis
  • Paper 112 — Layer D Nested Dot (depth-3/4 compression)
  • Paper 116 — Andrica Lean 4 bound
  • Paper 117 — Erdős-Straus small-n witnesses
  • Paper 118 (this paper) — first adoption of the four-element structure

14. References

  1. Köthe, G. (1930). Die Struktur der Ringe, deren Restklassenring nach dem Radikal vollständig reduzibel ist. Math. Z. 32(1), 161–186.
  2. Mathlib contributors. (2024). Mathlib v4.27.0.
  3. Fujimoto, N. (2026). Rei-AIOS LeanDFumt (Paper 77). Zenodo DOI 10.5281/zenodo.19596351.
  4. Lagarias, J. C. (2010). The 3x+1 Problem: An Annotated Bibliography. AMS.
  5. Tao, T. (2022). Almost all orbits of the Collatz map attain almost bounded values. arXiv:1909.03562.
  6. Santana, L. A. (2026). A topological approach to the 3x+1 problem. arXiv:2601.03297v4.
  7. Oppermann, L. (1882). Original conjecture on primes between n² − n and n² + n.

15. Acknowledgements

This paper consolidates work from STEPs 843, 844, 845, 866, 867, 868, 869, 872, 873, 875, 926, 927 of the Rei-AIOS project. The authors thank chat-Claude (web) for the LTE one-liner (Closure 4), for difficulty evaluations leading to the Köthe closure selection, and for the four-element paper-structure proposal that this paper inaugurates.

This is the first Rei-AIOS paper to include AI-generated open questions (Part C) as a first-class section. Subsequent papers will follow the same template.

End of Paper 118.

Top comments (0)