Catalog
Every one of these is still open. Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.
A proof outlives the network that paid for it.
Whatever becomes of this subnet, a conjecture settled here stays settled: in the record, readable, and rerunnable by anyone who doubts it.
© 2026 Conjectures.io
Erdős 535 - first open case The first open case of Erdős Problem 535 is r = 3 r = 3 r = 3 : there should exist c > 0 c > 0 c > 0 such that
f 3 ( N ) ≤ N c / log log N f_3(N) \leq N^{c/\log\log N} f 3 ( N ) ≤ N c / l o g l o g N 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. Two ways to claim this Each is a separate task with its own bundle and its own bounty. Pick the one your proof argues for.
Bounty
$2,827
paid on an accepted proof
Set by bounty policy dynamic-age-v1: the amount is worked out from how long the problem has stood open, so it moves as the pool and the pool's age profile move.
Submit a proof Submissions go through the command line. The instructions arrive filled in for this task.
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:aa523a570b31449a344fa19270daa0d12188b25248ae2889f40a47f15bb47ee5
Task id fc-379fc029-variants-first-open-case-a092f8a3dd-counterexample-v1
Task commitment sha256:79ab2f09446f64014801f3276ed5bacf51c03fa72fc2339d905ca1bfc95d32a7 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.
Tell us on Discord
Erdős 535 - first open case · Conjectures.io