Are there infinitely many primes $p$ such that $p - k!$ is composite for each $k$ such that $1 \leq k! < p$ ?

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

The primes with this property are commonly called **Erdős primes**: primes $p$ such that every number [ p-k! \quad\text{for } 1\le k!!<p ] is composite. Erdős asked whether there are **infinitely many** such primes; it is listed as an **open Erdős problem** (reported in Guy’s *Unsolved Problems in Number Theory*). ([Er…

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_1059 :
    answer(sorry) ↔ Set.Infinite {p | p.Prime ∧ AllFactorialSubtractionsComposite p}

formal-conjectures/1059.lean ↗

oeis

A064152 — Erdős primes: primes p such that all p-k! for 1 <= k! < p are composite.2,101,211,367,409,419,461,557,673,709,769,937,967,1009,1201,1259,1709,1831,1889,2141,2221,2309,2351,2411,2437,2539,2647,

status

open

evidence

formal

oeis

status

Search Vela