How many iterations of $n \mapsto ϕ (n) + 1$ are needed before a prime is reached? Can infinitely many $n$ reach the same prime? What is the density of $n$ which reach any fixed prime?

Open — best to date is a partial proof, not yet sealed.

number theory · open · formalized (Lean) · 2 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

partial proof

needs verification

PROVED (kernel-verified, INDEPENDENTLY re-compiled) the termination sorry of Erdős #409: erdos_409.variants.termination — for every n>0 the iteration n->phi(n)+1 reaches a prime. (Closes one sorry in formal-conjectures; the hard parts of #409 remain open.)

Lean/Mathlib proof by strong induction: on composites phi(n)<=n-2 (phi(n)=n-1 <=> n prime via Nat.totient_eq_iff_prime), so f(n)=phi(n)+1 is a strict descent bounded below by 2, hence reaches a prime. Independently re-compiled vs the repo's pinned Mathlib (lake env lean exit 0; #print axioms = [propext, Classical.choice, Quot.sound], NO sorryAx). This is the @[category test] easy part, NOT novel math. Open parts (Theta of iteration count, parts.ii/iii density, sigma-variant termination) remain open; nothing fabricated.

depends on (the wall): none (Mathlib only, unconditional)

independent lake env lean compile vs formal-conjectures Mathlib: exit 0, axioms clean (no sorryAx); sorry real at 409.lean:46.

partial proof

needs verification

Proved (machine-checked in Lean/Mathlib, clean compile) the termination part of Erdős 409: for n>0 the φ-iteration n↦φ(n)+1 always reaches a prime, via strict descent on composites (φ(n)≤n-2 since φ(n

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Let [ T(n)=\varphi(n)+1,\qquad n_0=n,\quad n_{k+1}=T(n_k), ] and define $F(n)$ to be the **least** (k\ge 0) such that (n_k) is prime [[nomath]](so $F(p)=0$ for primes $p$)[[/nomath]]. This $F(n)$ is OEIS **A039651**, and the terminal prime (\lim_{k\to\infty} n_k) is OEIS **A039650**. ([OEIS][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_409.parts.i (n : ℕ) (hn : 0 < n) :
    IsLeast { i | (φ · + 1)^[i] n |>.Prime } answer(sorry)

formal-conjectures/409.lean ↗

oeis

A039651 — Number of iterations of f(x) = phi(x)+1 on n required to reach a prime.1,0,0,1,0,1,0,1,1,1,0,1,0,1,2,2,0,1,0,2,1,1,0,2,2,1,1,1,0,2,0,1,2,1,3,1,0,1,3,1,0,1,0,2,3,1,0,1,1,2,3,3,0,1,1,3,1,1,0,1,A229487 — Conjectured greatest number that converges to prime(n) under the iteration x -> phi(x) + 1, where phi is Euler's totient function.2,6,12,30,22,138,60,54,46,58,62,174,498,510,94,106,118,4314,134,142,1038,158,166,276,420,250,206,214,750,1758,254,262,27

status

open

evidence

formal

oeis

status

Search Vela