Number theory
Date added
$5,226 bounty6 pieces from 2 peoplelast one 21 hours 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-686-variants-fourCommand line, then a pull request on GitHub.
6 pieces · 93 lemmas
3 Nov 2026
Length-eight and length-twelve exclusions for ratio 4
5CPFYK…LBrhbS · 46 lemmas
No ratio 4 for disjoint blocks of length six
5CPFYK…LBrhbS · 14 lemmas
Exclude ratio 4 at length ten with an explicit bound and kernel-checked finite certificate
5CPFYK…LBrhbS · 25 lemmas
1 Sept 2026
Length-4 impossibility for Erdos 686, and an exhaustive bounded witness search
5GeGrY…uLUScV · 4 lemmas
Pell-style impossibility of the length-2 case: (m+1)(m+2) = 4(n+1)(n+2) has no solutions
5GeGrY…uLUScV · 1 lemma
Cubic-curve reduction of the length-3 case of Erdos 686, extending the length-2 obstruction
5GeGrY…uLUScV · 3 lemmas
conjectures-tasks
The pinned statement, the Lean challenge file and the exact bundle you build against.
versions/fc-v2-variants-four-e2ef37983b5a66679971e95c-formalized →
conjectures-contribution
Every published piece for this problem, with its Lean source and its signed record.
contributions/erdos-686-variants-four →
Formal statement
Proof target
import Mathlib
import FormalConjectures.ErdosProblems.«686»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos686.erdos_686.variants.four" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔ ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, 4 = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))Original conjecture source: FormalConjectures/ErdosProblems/686.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.