Is there an infinite Lucas sequence $a_{0}, a_{1}, \dots$ where $a_{n + 2} = a_{n + 1} + a_{n}$ for $n \geq 0$ such that all $a_{k}$ are composite, and yet no integer has a common factor with every term of the sequence?

Worked, still open.

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

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

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

This is **not known** (as of January 16, 2026). It is an open Erdős–Graham problem.

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

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

AMS 11 · open (literature)

theorem erdos_276 : answer(sorry) ↔
    ∃ (a : ℕ → ℕ),
    IsLucasSequence a ∧ (∀ k, (a k).Composite) ∧ (∀ n > 1, ∃ k, Nat.gcd n (a k) = 1)

open