Number theory
Erdős 1059
Are there infinitely many primes such that is composite for each such that ?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ {p | Nat.Prime p ∧ Erdos1059.AllFactorialSubtractionsComposite p}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«1059»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos1059.erdos_1059" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/1059.lean
- Source type SHA-256
- sha256:98974fba9f1c9ea6a2cacf4fd3f1ef139bb69c2ace4d6e77536cf4aae51995ba
- Task id
- fc-379fc029-erdos1059-erdos-1059-e09749a98e-formalized-v1
- Task commitment
- sha256:5ab0428e2fa52e0ea7dad25a0962f14da089fb3bf549c15155954fd8c671124c
Something wrong with this formalization?
A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.