The board / additive combinatorics / #1112
Erdős Problem #1112
OPEN LEANdatabase updated 2026-07-25
No proof or disproof is known, and it isn't known whether a finite computation could settle it. A solution has been formally verified in Lean, but no human reader has digested it yet — which is why the database doesn't call it solved.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Prizenone
Topicsadditive combinatorics
Statement in Leannot yet
Solution in Leanyes
Original pageerdosproblems.com/1112
Attempts
submit one →Read our working report →
The live page status is “OPEN (LEAN)”, but it lists “1 claimed proof” and JohanLand as “Currently working on this problem”; per the mandatory collision rule, no mathematical attempt was made.
SKIPPED