Number theory
Erdős 376
Are there infinitely many such that is coprime to ?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ {n | n.centralBinom.Coprime 105}.InfiniteWhat you must prove
import FormalConjectures.ErdosProblems.«376»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos376.erdos_376" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/376.lean
- Source type SHA-256
- sha256:f4e6248cce761d39d1351429041fa49c2ce574bb3752e60498d3ebaa5fd0dbc9
- Task id
- fc-379fc029-erdos376-erdos-376-abc0a42eb1-formalized-v1
- Task commitment
- sha256:b8737d95fa0666ef5dde64e06578aea312e2e563470ccf8075c900a6d9d151bb
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.