You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The test-tagged theorem Erdos36.M_one in FormalConjectures/ErdosProblems/36.lean currently uses sorry. For n = 1 the only balanced partition of {1, 2\} is {1} ∪ {2} (up to swap), giving MaxOverlap = 1.
The test-tagged theorem
Erdos36.M_oneinFormalConjectures/ErdosProblems/36.leancurrently usessorry. Forn = 1the only balanced partition of{1, 2\}is{1}∪{2}(up to swap), givingMaxOverlap = 1.