Spin glass
In a model of magnets, every arrow points up or down and every arrangement gets a score. Two arrangements can both score almost the best while about half their arrows differ. When the scoring is random, the chance that such a pair exists approaches 100% as the number of arrows grows.
Limits: The Lean proofs are OpenAI’s and cover OpenAI’s theorem. They do not cover this result about two arrangements.
The result follows from a 2020 paper by Auffinger, Chen and Zeng and an OpenAI theorem released in October 2026.
Lean is a program that checks mathematical proofs.
