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.
$3,556 bounty
A complete proof or refutation in Lean. The first one the validator accepts takes the whole bounty.
Formal statement
Proof target
import FormalConjectures.ResearchTargets.Math15
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Math15Catalog.source06" := by
sorry
end Bounty
Original conjecture (Lean type)
Math15.LonelyRunner.Target06Original conjecture source: FormalConjectures/ResearchTargets/Math15.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.
for closing this problem
Whoever closes it takes the bounty. Published pieces that helped get there share a separate contribution pool, paid out once the problem is closed.
Set by bounty policy linear-age-v3-locked: the amount is worked out from how long the problem has stood open, so it moves as the pool and the pool's age profile move.
Prove it or break it
The same problem accepts both. You can submit a proof of the statement or a counterexample that refutes it, and you choose which when you submit.