Combinatorics
Date added
$5,268 bounty2 pieces from 2 peoplelast one 2 months ago
Nobody has attempted this. A complete proof or refutation takes the whole bounty.
A lemma, a definition, a special case. There is no race: when someone closes the problem, up to half of its bounty can go to the recognised pieces that led there.
contrib new erdos-617Command line, then a pull request on GitHub.
2 pieces · 163 lemmas
19 Sept 2026
Erdős 617: partition stability, minimum-hole transfer, and surplus bounds
5E7uWL…uzcwd3 · 143 lemmas
2 Sept 2026
conjectures-tasks
The pinned statement, the Lean challenge file and the exact bundle you build against.
versions/fc-v2-erdos617-erdos-617-5e38eddf1eb733b873b26a06-formalized →
conjectures-contribution
Every published piece for this problem, with its Lean source and its signed record.
contributions/erdos-617 →
Formal statement
Proof target
import Mathlib
import FormalConjectures.ErdosProblems.«617»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos617.erdos_617" := by
sorry
end Bounty
Original conjecture (Lean type)
∀ r ≥ 3,
∀ {V : Type} [inst : Fintype V] [DecidableEq V],
Fintype.card V = r ^ 2 + 1 →
∀ (coloring : Sym2 V → Fin r), ∃ S k, S.card = r + 1 ∧ ∀ u ∈ S, ∀ v ∈ S, u ≠ v → coloring s(u, v) ≠ kOriginal conjecture source: FormalConjectures/ErdosProblems/617.lean
References
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.
Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.