GPT-5.6 Sol improved an upper bound from a 2019 paper by Terry Tao in just 13 minutes
There is a classical result in operator theory with broad implications for quantum mechanics: the operator equation [D, X] = 1 has no exact solutions for bounded operators. What if we want to solve it approximately?
Popa proved that, for a solution with error less than ε, the operators must have norm at least ½ log(1/ε). However, we do not yet know whether this bound is achievable. In 2019, Tao constructed a solution with norm O(log5(1/ε)). Today, GPT-5.6 Sol improved this result to O(log4(1/ε)) in just 13 minutes, then formalized it in Lean in less than three hours.
Perhaps the biggest highlight is that both the proof and the formalization were completed with just a Plus subscription, so you do not need Pro to obtain new results already. Could Tao or anyone else do it themselves? Definitely, but it would likely take much more time: Tao himself improved the exponent from 16 to 5 following reviewer comments.
Challenge: Can Pro achieve the conjectured O(log(1/ε)) bound?