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.
Combinatorics
SolvedWe could not load the accepted results for this problem right now. This is on us - try again shortly.
Must every permutation of , contain a monotone 4-term arithmetic progression?A proof for this one passed the Lean kernel and the bounty was paid.
1 piece from 1 personlast one last month1 proof submitted, 24 days ago
This target is closed.
An accepted submission closed this reward target. Its recorded review determines whether it settles the mathematical problem or identifies a formalization defect.
Formal statement
Proof target
import FormalConjectures.ErdosProblems.«196»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos196.erdos_196" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4Original conjecture source: FormalConjectures/ErdosProblems/196.lean
1 piece · 20 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
2 Sept 2026
Erdős 196: monotone 4-AP API for permutations, decidable AP tests, growth obstruction
5FqLp5…FfZZiK · 20 lemmas
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.