FormalConjectures.Wikipedia.LychrelNumbers

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

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:

Wikipedia: Lychrel number

MathWorld: Lychrel Number

OEIS A023108

OEIS A023109


namespace LychrelNumbers

The base (10) used for digit reversal.

abbrev base : ℕ := 10

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.

def rev10 (n : ℕ) : ℕ :=
  Nat.ofDigits base (Nat.digits base n).reverse

A number is a (base-10) palindrome if it equals its digit reversal.

def IsPalindrome10 (n : ℕ) : Prop :=
  rev10 n = n

One step of the Lychrel iteration: n ↦ n + rev10 n.

def lychrelStep (n : ℕ) : ℕ :=
  n + rev10 n

The number $n$ is a (base-10) Lychrel number if no iterate of the Lychrel process is a palindrome.

def IsLychrel10 (n : ℕ) : Prop :=
  ∀ k : ℕ, ¬ IsPalindrome10 (lychrelStep^[k] n)

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.

@[category research open, AMS 11]
theorem declaration uses 'sorry'no_lychrel_numbers_base10 :
    answer(sorry) ↔ ∀ n : ℕ, 0 < n → ¬ IsLychrel10 n := by⊢ True ↔ ∀ (n : ℕ), 0 < n → ¬IsLychrel10 n
  sorryAll goals completed! 🐙

The first widely studied open case: whether 196 is a base-10 Lychrel number.

@[category research open, AMS 11]
theorem declaration uses 'sorry'isLychrel10_196 : answer(sorry) ↔ IsLychrel10 196 := by⊢ True ↔ IsLychrel10 196
  sorryAll goals completed! 🐙

An equivalent formulation of no_lychrel_numbers_base10.

@[category API, AMS 11]
theorem eventually_palindrome_base10 :
    (∀ n : ℕ, 0 < n → ∃ k : ℕ, IsPalindrome10 (lychrelStep^[k] n)) ↔
      (∀ n : ℕ, 0 < n → ¬ IsLychrel10 n) := by⊢ (∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)) ↔ ∀ (n : ℕ), 0 < n → ¬IsLychrel10 n
  constructormp⊢ (∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)) → ∀ (n : ℕ), 0 < n → ¬IsLychrel10 nmpr⊢ (∀ (n : ℕ), 0 < n → ¬IsLychrel10 n) → ∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)
  ·mp⊢ (∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)) → ∀ (n : ℕ), 0 < n → ¬IsLychrel10 n intro h nmph:∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)n:ℕ⊢ 0 < n → ¬IsLychrel10 n hnmph:∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)n:ℕhn:0 < n⊢ ¬IsLychrel10 n hn_lychrelmph:∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)n:ℕhn:0 < nhn_lychrel:IsLychrel10 n⊢ False
    rcases h n hn with ⟨k, hk⟩mph:∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)n:ℕhn:0 < nhn_lychrel:IsLychrel10 nk:ℕhk:IsPalindrome10 (lychrelStep^[k] n)⊢ False
    exact hn_lychrel k hkAll goals completed! 🐙
  ·mpr⊢ (∀ (n : ℕ), 0 < n → ¬IsLychrel10 n) → ∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n) intro h nmprh:∀ (n : ℕ), 0 < n → ¬IsLychrel10 nn:ℕ⊢ 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n) hnmprh:∀ (n : ℕ), 0 < n → ¬IsLychrel10 nn:ℕhn:0 < n⊢ ∃ k, IsPalindrome10 (lychrelStep^[k] n)
    by_contra hcontramprh:∀ (n : ℕ), 0 < n → ¬IsLychrel10 nn:ℕhn:0 < nhcontra:¬∃ k, IsPalindrome10 (lychrelStep^[k] n)⊢ False
    have : IsLychrel10 n := by⊢ (∀ (n : ℕ), 0 < n → ∃ k, IsPalindrome10 (lychrelStep^[k] n)) ↔ ∀ (n : ℕ), 0 < n → ¬IsLychrel10 n
      intro k hkh:∀ (n : ℕ), 0 < n → ¬IsLychrel10 nn:ℕhn:0 < nhcontra:¬∃ k, IsPalindrome10 (lychrelStep^[k] n)k:ℕhk:IsPalindrome10 (lychrelStep^[k] n)⊢ False
      exact hcontra ⟨k, hk⟩All goals completed! 🐙
    exact h n hn thisAll goals completed! 🐙

Sanity check: digit reversal of 120 is 21.

@[category test, AMS 11]
theorem rev10_120 : rev10 120 = 21 := by⊢ rev10 120 = 21
  native_decideAll goals completed! 🐙

Sanity check: 121 is a base-10 palindrome.

@[category test, AMS 11]
theorem palindrome_121 : IsPalindrome10 121 := by⊢ IsPalindrome10 121
  dsimp [IsPalindrome10]⊢ rev10 121 = 121
  native_decideAll goals completed! 🐙

Sanity check: 56 → 121 in one Lychrel step.

@[category test, AMS 11]
theorem lychrelIter_56_one : lychrelStep^[1] 56 = 121 := by⊢ lychrelStep^[1] 56 = 121
  native_decideAll goals completed! 🐙

Sanity check: the Lychrel iteration at 56 reaches a palindrome.

@[category test, AMS 11]
theorem eventually_palindrome_56 : ∃ k : ℕ, IsPalindrome10 (lychrelStep^[k] 56) := by⊢ ∃ k, IsPalindrome10 (lychrelStep^[k] 56)
  refine ⟨1, ?_⟩⊢ IsPalindrome10 (lychrelStep^[1] 56)
  dsimp [IsPalindrome10]⊢ rev10 (lychrelStep 56) = lychrelStep 56
  native_decideAll goals completed! 🐙

end LychrelNumbers