Comment by zone411
3 hours ago
I maintain an LLM-ranked list of the 500 most important open problems in math at https://www.proofatlas.ai/open-problems/. This problem was ranked #159, and it also resolved #244, "All-Pairs Shortest Paths in Truly Subcubic Time." It is formalized in Lean.
But what's crazy is that within the last day or so, we've also gotten LLM-assisted solutions to #95, the Kannan–Lovász–Simonovits (KLS) conjecture, by three different authors in parallel (all extending Song–Zhang's key criterion introduced on Oct. 1), #278, the Mumford–Shah conjecture, and #227, Zauner's conjecture on SIC-POVM existence in every dimension, which also represents a major claimed advance on Hilbert's twelfth problem (#36) for real quadratic fields.
This is likely because OpenAI's solutions to 100 open conjectures are expected to drop any day, so everyone is in a hurry not to get scooped.
does that site have a list of solutions/dates they come out? or do you remove problems once they've been solved?
Yes, you can see the latest resolved ones here: https://www.proofatlas.ai/open-problems/#resolved-problems. I'm currently doing updates in batches, but I'm about to switch to daily updates.
Right now, I'm having LLMs audit the actual math in claimed arXiv solutions because despite its policy changes, arXiv is still a dumping ground. The audits have already found six faulty proofs that caused status issues for problems that should still clearly be fully open.