Number theory
Approved
The accepted file establishes a result about a faulty formal statement. It does not settle the intended mathematical problem. The recorded review explains the mismatch.
Submitted by 5H3ZSq…NHznXs
Withdrawn 6 Aug 2026
SOURCE_MISMATCH + EXPLOITABLE + SOLVED (Erdos939Sums omits positivity of the summands and Nat.Full is vacuous at 0 and 1, so the r = 4 case — the one with no known example — is satisfied by {0, 1}; submission 91915fc3 discharged it that way)
Read the recorded decisionFormal statement
Proof target
import FormalConjectures.ErdosProblems.«939»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos939.erdos_939" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔ ∀ r ≥ 4, (Erdos939.Erdos939Sums r).NonemptyOriginal conjecture source: FormalConjectures/ErdosProblems/939.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.