Combinatorics
Erdős 535 - first open case
The first open case of Erdős Problem 535 is : there should exist such that for all sufficiently large .References
- Er64 P. Erdős, On a problem in elementary number theory and a combinatorial problem. Math. Comp. (1964), 644–646.
- AbHa70 H. L. Abbott and D. Hanson, An extremal problem in number theory. Bull. London Math. Soc. (1970), 324–326.
- Er73 P. Erdős, Problems and results on combinatorial number theory, in *A Survey of Combinatorial Theory*, North-Holland, 1973.
No one has attempted this yet.
Formal statement
Lean type
∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos535.f 3 N) ≤ ↑N ^ (c / Real.log (Real.log ↑N))What you must prove
import FormalConjectures.ErdosProblems.«535»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos535.erdos_535.variants.first_open_case" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/535.lean
- Source type SHA-256
- sha256:4940f37b482af2f8dde043c96224ee6c7df8b9909463615304905090c881a800
- Task id
- fc-379fc029-variants-first-open-case-09c89f4ec6-formalized-v1
- Task commitment
- sha256:22cf446ce24c40fb947c22ab29e662d3b26f7002ad6573aed8df204733b81c00
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.