Number theory
Solved elsewhereDate added
Withdrawn 6 Oct 2026
SOLVED_EXTERNALLY (the release coordinator confirmed a solution of this exact target: conjectures.io result 71c87792-e08f-413c-9b7a-3b61e577eed6 and the public Lean repository tokengr1nder/Erdos252 at commit dc071aafce41bbae41caf4c015499db6dafafd11. This retirement did not independently rebuild that proof. See EXTERNAL-SOLUTIONS-2026-10-06.md.)
1 piece from 1 personlast one 2 months ago1 proof submitted, 2 months ago
This target is closed.
This conjecture was resolved outside the subnet, so no bounty is payable. It stays in the catalog as a record; it no longer takes submissions.
Formal statement
Proof target
import FormalConjectures.ErdosProblems.«252»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos252.erdos_252" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔ ∀ k ≥ 1, Irrational (Erdos252.erdos_252_sum k)Original conjecture source: FormalConjectures/ErdosProblems/252.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.
1 piece · 83 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
1 Sept 2026
Checked cases k = 0, 1, 2 of Erdős 252
5FqLp5…FfZZiK · 83 lemmas