Suppose you have n integers, and you want to decide whether some three of them sum to zero. It's not hard to solve this problem in O(n^2) time (think how to do it, the dumbest algorithm takes O(n^3) time!) and for a long time it was thought that getting time O(n^{1.999999}) is not possible. This hardness assumption was shown to imply many other interesting hardness results. Not anymore! Claude obtained the O(n^{1.9992}) time algorithm together with a Lean proof, and the algorithm was checked and digested by Josh Alman and Virginia Williams who are leading experts in fine-grained hardness, so my a priori estimate that it's 99.99%-likely to be correct. My mind is just absolutely blown! It's crazy that in such simple to state problems progress is still possible after decades of many smart people thinking hard about them.