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_two in FormalConjectures/ErdosProblems/36.lean currently uses sorry. The balanced partition A = {1, 4}, B = {2, 3} has all four pairwise differences (±1, ±2) distinct, achieving MaxOverlap = 1.
The test-tagged theorem
Erdos36.M_twoinFormalConjectures/ErdosProblems/36.leancurrently usessorry. The balanced partitionA = {1, 4}, B = {2, 3}has all four pairwise differences (±1, ±2) distinct, achievingMaxOverlap = 1.