1. FormalConjectures
  2. Wikipedia
  3. 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:

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 no_lychrel_numbers_base10 : answer(sorry) ↔ ∀ n : ℕ, 0 < n → ¬ IsLychrel10 n := ⊢ True ↔ ∀ (n : ℕ), 0 < n → ¬IsLychrel10 n All goals completed! 🐙

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

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

An equivalent formulation of no_lychrel_numbers_base10.

h:∀ (n : ℕ), 0 < n → ¬IsLychrel10 nn:ℕhn:0 < nhcontra:¬∃ k, IsPalindrome10 (lychrelStep^[k] n)this:IsLychrel10 n⊢ False All goals completed! 🐙

Sanity check: digit reversal of 120 is 21.

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

Sanity check: 121 is a base-10 palindrome.

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

Sanity check: 56 → 121 in one Lychrel step.

@[category test, AMS 11] theorem lychrelIter_56_one : lychrelStep^[1] 56 = 121 := ⊢ lychrelStep^[1] 56 = 121 All 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) := ⊢ ∃ k, IsPalindrome10 (lychrelStep^[k] 56) ⊢ IsPalindrome10 (lychrelStep^[1] 56) ⊢ rev10 (lychrelStep 56) = lychrelStep 56 All goals completed! 🐙end LychrelNumbers