Combinatorics
WithdrawnDate added
Withdrawn 5 Aug 2026
SOURCE_MISMATCH (Nat.smoothNumbers k means primes < k; erdosproblems.com/1093 defines k-smooth as primes ≤ k)
Formal statement
Proof target
import FormalConjectures.ErdosProblems.«1093»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos1093.erdos_1093.parts.ii" := by
sorry
end Bounty
Original conjecture (Lean type)
{x |
have k := x.1;
have n := x.2;
2 * k ≤ n ∧ Erdos1093.deficiency n k > 1 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ n.choose k → k < p}.FiniteOriginal conjecture source: FormalConjectures/ErdosProblems/1093.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.