Combinatorics
Erdős 141 - eleven
Are there consecutive primes in arithmetic progression?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ ∃ s, Erdos141.Set.IsAPAndPrimeProgressionOfLength s 11What you must prove
import FormalConjectures.ErdosProblems.«141»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos141.erdos_141.variants.eleven" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/141.lean
- Source type SHA-256
- sha256:b10dd0ad30bf63d1a026393ffb397b5829c954f5752cf7e7f40bc089e2db4c5e
- Task id
- fc-379fc029-variants-eleven-7f0c7a22b7-formalized-v1
- Task commitment
- sha256:a6e0289bf626dc278707e096eae2edee682387786d3d69ea01d5aeb1bcbb285b
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.