Number theory
Date added
$5,226 bounty2 pieces from 1 personlast 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-1107Command line, then a pull request on GitHub.
2 pieces · 7 lemmas
1 Sept 2026
[test] The list introduction rule and the degenerate r < 2 cases for SumOfRPowerful
5Hn8NE…hth574 · 3 lemmas
31 Aug 2026
[test] Introduction rules for Erdos1107.SumOfRPowerful
5Hn8NE…hth574 · 4 lemmas
conjectures-tasks
The pinned statement, the Lean challenge file and the exact bundle you build against.
versions/fc-v2-erdos1107-erdos-1107-f919b95503ad4ddd0d19b46a-formalized →
conjectures-contribution
Every published piece for this problem, with its Lean source and its signed record.
contributions/erdos-1107 →
Formal statement
Proof target
import Mathlib
import FormalConjectures.ErdosProblems.«1107»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos1107.erdos_1107" := by
sorry
end Bounty
Original conjecture (Lean type)
∀ r ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1107.SumOfRPowerful r nOriginal conjecture source: FormalConjectures/ErdosProblems/1107.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.