Skip to content

Erdős problem 1074

Similarly, if PP is the set of all primes pp such that there exists an mm with p≢1(modm)p\not\equiv 1\pmod{m} such that m!+1≡0(modp)m! + 1 \equiv 0\pmod{p}, then does lim⁡∣P∩[1,x]∣π(x) \lim\frac{|P\cap[1, x]|}{\pi(x)} exist?

Sources

The source's own material, retained exactly.

12 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1074.lean

Retained formal statement5 of 12

Erdős, Hardy, and Subbarao proved that SS is infinite.

Formal proof linked here provided by AlphaProof.

FormalConjectures/ErdosProblems/1074.leanErdos1074.erdos_1074.variants.EHSNumbers_infinite1 lineExact file
Erdos1074.EHSNumbers.Infinite
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.