Prove Laughlin (openai/math family 269: The Laughlin gap and stability under scalar disorder) in Lean 4 with…
Prove Laughlin (openai/math family 269: The Laughlin gap and stability under scalar disorder) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 269 of the release, The Laughlin gap and stability under scalar disorder…
The task
Context: this statement belongs to family 269 of the release, *The Laughlin gap and stability under scalar disorder* (Mathematical physics). The family as a whole: Proves the fermionic Laughlin spectral-gap conjecture for the full $V_1$ interaction at filling $1/3$ on the round sphere. The unique ground state remains…
Part of raising-heart/openai-math.