LychrelNumbers.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

12 declarations, 2 contain sorry, 0 declared as axioms

Lychrel numbers in base 10

A (base-10) Lychrel number is a positive integer which never becomes a palindrome under the iteration

$$a_{0} = n, \qquad a_{k+1} = a_k + \operatorname{rev}_{10}(a_k).$$

One commonly stated conjectural direction is that there are no Lychrel numbers in base 10. The smallest widely studied open case is 196.

References:

Imports (1)

FormalConjecturesUtil

Imported by 2 files

abbrev LychrelNumbers.base The base (10) used for digit reversal line 44 source
Source documentation
The base (10) used for digit reversal.

no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
abbrev base : ℕ := 10
```
def LychrelNumbers.rev10 The digit-reversal map $\operatorname{rev}_{10}(n)$ line 53 source
Source documentation
The digit-reversal map $\operatorname{rev}_{10}(n)$.
Implementation note: Nat.digits base n returns the digits of n in little-endian order. Reversing this list and interpreting it again as little-endian digits gives the usual digit reversal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Nat.ofDigits, LychrelNumbers.base, List.reverse, Nat.digits
1 instances, coercions and auxiliary constants left out.
```
def rev10 (n : ℕ) : ℕ :=
…
```
def LychrelNumbers.IsPalindrome10 A number is a (base-10) palindrome if it equals its digit reversal line 57 source
Source documentation
A number is a (base-10) palindrome if it equals its digit reversal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Eq, LychrelNumbers.rev10
```
def IsPalindrome10 (n : ℕ) : Prop :=
…
```
def LychrelNumbers.lychrelStep One step of the Lychrel iteration: n ↦ n + rev10 n line 61 source
Source documentation
One step of the Lychrel iteration: n ↦ n + rev10 n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: HAdd.hAdd, LychrelNumbers.rev10
2 instances, coercions and auxiliary constants left out.
```
def lychrelStep (n : ℕ) : ℕ :=
…
```
def LychrelNumbers.IsLychrel10 The number $n$ is a (base-10) Lychrel number if no iterate of the Lychrel process is a palindrome line 65 source
Source documentation
The number $n$ is a (base-10) Lychrel number if no iterate of the Lychrel process is a palindrome.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Not, LychrelNumbers.IsPalindrome10, Nat.iterate, LychrelNumbers.lychrelStep
```
def IsLychrel10 (n : ℕ) : Prop :=
…
```
theorem LychrelNumbers.no_lychrel_numbers_base10 Lychrel conjecture (base 10): conjecturally, there are no Lychrel numbers in base 10 sorry line 74 source
Source documentation
Lychrel conjecture (base 10): conjecturally, there are no Lychrel numbers in base 10.
Equivalently, every positive integer eventually becomes a palindrome under the Lychrel iteration.

depends on sorry what this means
Statement uses: Iff, True, Nat, LT.lt, OfNat.ofNat, Not, LychrelNumbers.IsLychrel10
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem no_lychrel_numbers_base10 :
    answer(sorry) ↔ ∀ n : ℕ, 0 < n → ¬ IsLychrel10 n := by
…
```
Mentions: LychrelNumbers.IsLychrel10
theorem LychrelNumbers.isLychrel10_196 The first widely studied open case: whether 196 is a base-10 Lychrel number sorry line 82 source
Source documentation
The first widely studied open case: whether 196 is a base-10 Lychrel number.

depends on sorry what this means
Statement uses: Iff, True, LychrelNumbers.IsLychrel10, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isLychrel10_196 : answer(sorry) ↔ IsLychrel10 196 := by
…
```
Mentions: LychrelNumbers.IsLychrel10
theorem LychrelNumbers.eventually_palindrome_base10 An equivalent formulation of no_lychrel_numbers_base10 line 87 source
Source documentation
An equivalent formulation of no_lychrel_numbers_base10.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, Nat, LT.lt, OfNat.ofNat, Exists, LychrelNumbers.IsPalindrome10, Nat.iterate, LychrelNumbers.lychrelStep, Not, LychrelNumbers.IsLychrel10
Proof uses: Iff.intro, False, Classical.byContradiction, Exists.intro
5 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem eventually_palindrome_base10 :
    (∀ n : ℕ, 0 < n → ∃ k : ℕ, IsPalindrome10 (lychrelStep^[k] n)) ↔
      (∀ n : ℕ, 0 < n → ¬ IsLychrel10 n) := by
…
```
Mentions: LychrelNumbers.IsPalindrome10, LychrelNumbers.lychrelStep, LychrelNumbers.IsLychrel10
theorem LychrelNumbers.rev10_120 Sanity check: digit reversal of 120 is 21 line 104 source
Source documentation
Sanity check: digit reversal of 120 is 21.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, LychrelNumbers.rev10, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rev10_120 : rev10 120 = 21 := by
…
```
Mentions: LychrelNumbers.rev10
theorem LychrelNumbers.palindrome_121 Sanity check: 121 is a base-10 palindrome line 109 source
Source documentation
Sanity check: 121 is a base-10 palindrome.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LychrelNumbers.IsPalindrome10, OfNat.ofNat, Nat
Proof uses: id, of_decide_eq_true, Eq, LychrelNumbers.rev10, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem palindrome_121 : IsPalindrome10 121 := by
…
```
Mentions: LychrelNumbers.IsPalindrome10
theorem LychrelNumbers.lychrelIter_56_one Sanity check: 56 → 121 in one Lychrel step line 115 source
Source documentation
Sanity check: 56 → 121 in one Lychrel step.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Nat.iterate, LychrelNumbers.lychrelStep, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lychrelIter_56_one : lychrelStep^[1] 56 = 121 := by
…
```
Mentions: LychrelNumbers.lychrelStep
theorem LychrelNumbers.eventually_palindrome_56 Sanity check: the Lychrel iteration at 56 reaches a palindrome line 120 source
Source documentation
Sanity check: the Lychrel iteration at 56 reaches a palindrome.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, LychrelNumbers.IsPalindrome10, Nat.iterate, LychrelNumbers.lychrelStep, OfNat.ofNat
Proof uses: Exists.intro, id, of_decide_eq_true, Eq, LychrelNumbers.rev10, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem eventually_palindrome_56 : ∃ k : ℕ, IsPalindrome10 (lychrelStep^[k] 56) := by
…
```
Mentions: LychrelNumbers.IsPalindrome10, LychrelNumbers.lychrelStep