Landau’s fourth problem: infinitely many primes of the form n² + 1

Prove that for every bound N there is a natural number n > N for which n² + 1 is prime. This is a particular quadratic prime-values problem. Producing values with a bounded number of prime factors is weaker than the requested primality. The target explicitly quantifies over arbitrarily large n. Research status checked 8 October 2026: no accepted general proof identified in the cited literature. This is a proposed formal statement; independent correspondence review is requested. A successful statement check establishes well-formedness, not the conjecture.

(fun prime : Nat → Prop =>
  ∀ N : Nat, ∃ n : Nat, N < n ∧ prime (n ^ 2 + 1))
(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p)

OA_statement : Prop