prime_spiral_ulam

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result prime_spiral_ulam is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Ulam spiral: The distribution of primes on the Ulam spiral exhibits unexpected diagonal patterns. The prime-generating polynomial 4n²+2n+1 appears more prominent. No rigorous explanation for the patterns is known.

Why this node was retired

The posted statement is

import Mathlib

theorem prime_spiral_ulam :
    ∀ eps : ℝ, 0 < eps →
    ∃ C : ℝ, 0 < C ∧
    ∀ n : ℕ, 1 ≤ n →
      {k : ℕ | k ≤ n ^ 2 ∧ Nat.Prime k ∧
        ∃ a b : ℤ, k = (4 * a ^ 2 + (2 * b + 1)) ∨ True}.ncard ≤
      C * n ^ 2 / Real.log n := by
  sorry

The set-builder condition ends in ∃ a b : ℤ, k = (4 * a ^ 2 + (2 * b + 1)) ∨ True, whose right disjunct is True, so the quadratic condition is discharged for every k and the set is just the primes below n ^ 2. What remains is a Chebyshev-type upper bound on π(n ^ 2), with nothing left of the Ulam-spiral phenomenon the node is named for.

What a faithful statement would require

The ∨ True must be removed so that membership really requires the prime to lie on the intended quadratic diagonal of the spiral.

No corrected replacement node exists yet.