Prove2Me

lean_workbook_plus_12210

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let kk be an even positive integer and define a sequence <xn><x_n> by x1=1,xn+1=kxn+1.x_1= 1 , x_{n+1} = k^{x_n} +1. Show that xn2x_n ^2 divides xn−1xn+1x_{n-1}x_{n+1} for each n≥2.n \geq 2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12210 (k : ℕ) (x : ℕ → ℕ) (h₀ : x 1 = 1) (h₁ : ∀ n, x (n + 1) = k^(x n) + 1) (h₂ : 2 ∣ k) (n : ℕ) (hn : 2 ≤ n) : (x n)^2 ∣ (x (n - 1)) * (x (n + 1))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph