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 10 Sept 2026
PRIOR_EXTERNAL_FORMALIZATION (Green 44, also Erdos 1202, was resolved negatively by Price and GPT-5.4 Pro. The public plby/lean-proofs Erdos1202 counterexample predates pool admission; its unchanged source and an exact-target bridge were independently kernel-checked on September 9. See EXTERNAL-SOLUTIONS-2026-09-10.md for public sources.)
1 proof submitted, 26 days ago
Formal statement
Proof target
import FormalConjectures.GreensOpenProblems.«44»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Green44.green_44" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔
∀ (N : ℕ) (p : Fin 1000 → ℕ) (A : (i : Fin 1000) → Finset (ZMod (p i))),
have remaining := {x ∈ Finset.Icc 1 N | ∀ (i : Fin 1000), ↑x ∉ A i};
(∀ (i : Fin 1000), Nat.Prime (p i)) →
StrictMono p → p 999 ^ 10 < N ^ 9 → (∀ (i : Fin 1000), (A i).card = p i / 2) → 10 * remaining.card ≤ NOriginal conjecture source: FormalConjectures/GreensOpenProblems/44.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.