Catalog
Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.
Number theory
WithdrawnWithdrawn 8 Sept 2026
QUARANTINE_DISPUTED_CLAIM (Bradford arXiv:2602.11774 claims an Erdos-Straus solution; source discussion disputes its credibility. Other advertised Lean solutions only supply finite checks or unsupported periodicity. The pinned target additionally requires distinct ordered denominators, so the exact implication would need checking even if the paper were accepted. No verified solution is asserted here. The all-numerators Schinzel generalization is a separate retained target.)
Formal statement
Proof target
import FormalConjectures.ErdosProblems.«242»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos242.erdos_242" := by
sorry
end Bounty
Original conjecture (Lean type)
∀ (n : ℕ), 2 < n → ∃ x y z, 1 ≤ x ∧ x < y ∧ y < z ∧ 4 / ↑n = 1 / ↑x + 1 / ↑y + 1 / ↑zOriginal conjecture source: FormalConjectures/ErdosProblems/242.lean
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.