FormalConjectures.OEIS.«62567»

/-
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

Reversible multiples $a(3^n) = 10^{3^{n-2}} - 1$ for powers of $3$

First multiple of $n$ whose reverse is also divisible by $n$, or 0 if no such multiple exists.

References:

A062567

arxiv/2605.22763 Advancing Mathematics Research with AI-Driven Formal Proof Search by George Tsoukalas et al.

namespace OeisA62567open Nat

The number whose digits in base 10 are $n$'s digits reversed.

def reverseNat (k : ℕ) : ℕ :=
  ofDigits 10 (digits 10 k).reverse

open Classical in

First multiple of $n$ whose reverse is also divisible by $n$, or 0 if no such multiple exists.

noncomputable def a (n : ℕ) : ℕ :=
  if n = 0 then 0
  else
    -- P(k) is the predicate for the multiplier k: k > 0 and n divides the reverse of (k*n).
    let P (k : ℕ) : Prop := k > 0 ∧ n ∣ reverseNat (k * n)

    -- We check if a solution exists (using classical reasoning, since P is decidable).
    if h_ex : ∃ k, P k then
      -- k_min is the smallest multiplier k >= 1.
      let k_min : ℕ := Nat.find h_ex
      k_min * n
    else
      0




open Classical in
@[category API, AMS 11]
lemma a_eq_self (n : ℕ) (hn : n > 0) (h_rev : n ∣ reverseNat n) : a n = n := byn:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ a n = n
  unfold an:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ (if n = 0 then 0
  else
    let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
    if h_ex : ∃ k, P k then
      have k_min := Nat.find h_ex;
      k_min * n
    else 0) =
  n
  rw [if_neg (byn:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ ¬n = 0n:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n omegaAll goals completed! 🐙n:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n)]n:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n
  have h_ex : ∃ k, k > 0 ∧ n ∣ reverseNat (k * n) := ⟨1, ⟨byn:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ 1 > 0n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n omegaAll goals completed! 🐙n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n, byn:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ n ∣ reverseNat (1 * n)n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n rw [one_muln:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ n ∣ reverseNat nn:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ n ∣ reverseNat nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n]n:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ n ∣ reverseNat nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n; exact h_revAll goals completed! 🐙n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n⟩⟩n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (let P := fun k ↦ k > 0 ∧ n ∣ reverseNat (k * n);
  if h_ex : ∃ k, P k then
    have k_min := Nat.find h_ex;
    k_min * n
  else 0) =
  n
  rw [dif_pos h_exn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (have k_min := Nat.find h_ex;
  k_min * n) =
  nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (have k_min := Nat.find h_ex;
  k_min * n) =
  n]n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (have k_min := Nat.find h_ex;
  k_min * n) =
  n
  change Nat.find h_ex * n = nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ Nat.find h_ex * n = n
  have hf : Nat.find h_ex = 1 := byn:ℕhn:n > 0h_rev:n ∣ reverseNat n⊢ a n = nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n
    rw [Nat.find_eq_iffn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (1 > 0 ∧ n ∣ reverseNat (1 * n)) ∧ ∀ n_1 < 1, ¬(n_1 > 0 ∧ n ∣ reverseNat (n_1 * n))n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (1 > 0 ∧ n ∣ reverseNat (1 * n)) ∧ ∀ n_1 < 1, ¬(n_1 > 0 ∧ n ∣ reverseNat (n_1 * n))n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n]n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ (1 > 0 ∧ n ∣ reverseNat (1 * n)) ∧ ∀ n_1 < 1, ¬(n_1 > 0 ∧ n ∣ reverseNat (n_1 * n))n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n
    refine ⟨⟨byn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ 1 > 0n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n omegaAll goals completed! 🐙n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n, byn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ n ∣ reverseNat (1 * n)n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n rw [one_muln:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ n ∣ reverseNat nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ n ∣ reverseNat nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n]n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)⊢ n ∣ reverseNat nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n; exact h_revAll goals completed! 🐙n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n⟩, ?_⟩
    intro k hkn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)k:ℕhk:k < 1⊢ ¬(k > 0 ∧ n ∣ reverseNat (k * n))n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n
    interval_cases k«0»n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)k:ℕhk:0 < 1⊢ ¬(0 > 0 ∧ n ∣ reverseNat (0 * n))n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n
    simpn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = nn:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ Nat.find h_ex * n = n
  rw [hf,n:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ 1 * n = nAll goals completed! 🐙 one_muln:ℕhn:n > 0h_rev:n ∣ reverseNat nh_ex:∃ k > 0, n ∣ reverseNat (k * n)hf:Nat.find h_ex = 1⊢ n = nAll goals completed! 🐙]All goals completed! 🐙



@[category API, AMS 11]
lemma reverseNat_of_lt (k : ℕ) (hk0 : k ≠ 0) (hk10 : k < 10) : reverseNat k = k := byk:ℕhk0:k ≠ 0hk10:k < 10⊢ reverseNat k = k
  unfold reverseNatk:ℕhk0:k ≠ 0hk10:k < 10⊢ ofDigits 10 (digits 10 k).reverse = k
  rw [Nat.digits_of_lt 10 k hk0 hk10k:ℕhk0:k ≠ 0hk10:k < 10⊢ ofDigits 10 [k].reverse = kk:ℕhk0:k ≠ 0hk10:k < 10⊢ ofDigits 10 [k].reverse = k]k:ℕhk0:k ≠ 0hk10:k < 10⊢ ofDigits 10 [k].reverse = k
  rflAll goals completed! 🐙



@[category test, AMS 11]
lemma a_1 : a 1 = 1 := by⊢ a 1 = 1
  apply a_eq_self 1 (by⊢ 1 > 0 omegaAll goals completed! 🐙) (by⊢ 1 ∣ reverseNat 1 rw [reverseNat_of_lt 1 (by⊢ 1 ≠ 0All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙) (by⊢ 1 < 10All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙)



@[category test, AMS 11]
lemma a_2 : a 2 = 2 := by⊢ a 2 = 2
  apply a_eq_self 2 (by⊢ 2 > 0 omegaAll goals completed! 🐙) (by⊢ 2 ∣ reverseNat 2 rw [reverseNat_of_lt 2 (by⊢ 2 ≠ 0All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙) (by⊢ 2 < 10All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙)



@[category test, AMS 11]
lemma a_3 : a 3 = 3 := by⊢ a 3 = 3
  apply a_eq_self 3 (by⊢ 3 > 0 omegaAll goals completed! 🐙) (by⊢ 3 ∣ reverseNat 3 rw [reverseNat_of_lt 3 (by⊢ 3 ≠ 0All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙) (by⊢ 3 < 10All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙)



@[category test, AMS 11]
lemma a_4 : a 4 = 4 := by⊢ a 4 = 4
  apply a_eq_self 4 (by⊢ 4 > 0 omegaAll goals completed! 🐙) (by⊢ 4 ∣ reverseNat 4 rw [reverseNat_of_lt 4 (by⊢ 4 ≠ 0All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙) (by⊢ 4 < 10All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙)



@[category test, AMS 11]
lemma a_5 : a 5 = 5 := by⊢ a 5 = 5
  apply a_eq_self 5 (by⊢ 5 > 0 omegaAll goals completed! 🐙) (by⊢ 5 ∣ reverseNat 5 rw [reverseNat_of_lt 5 (by⊢ 5 ≠ 0All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙) (by⊢ 5 < 10All goals completed! 🐙 decideAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙)

The conjecture that $a(3^n) = 10^{3^{n-2}} - 1$ for $n > 1$ was shown to be false for $4 < n < 21$ by Farideh Firoozbakht, who conjectured that for all $n > 4$, $a(3^n) \neq 10^{3^{n-2}} - 1$. This latter conjecture is proved here.

A formal proof has been found with the methods described in arxiv/2605.22763.

@[category research solved, AMS 11, formal_proof using formal_conjectures at
"https://github.com/mo271/formal-conjectures/blob/a32396489dcb8f86c3549b93aa358ac6a10a3a1f/FormalConjectures/OEIS/62567.wip.lean#L324"]
theorem a_three_pow_eq (n : ℕ) :
    2 ≤ n → (a (3 ^ n) = 10 ^ (3 ^ (n - 2)) - 1 ↔ n = 2 ∨ n = 3 ∨ n = 4) := byn:ℕ⊢ 2 ≤ n → (OeisA62567.a (3 ^ n) = 10 ^ 3 ^ (n - 2) - 1 ↔ n = 2 ∨ n = 3 ∨ n = 4)
    sorryAll goals completed! 🐙

end OeisA62567