A UC Berkeley IEOR researcher used GPT-5.6 Sol Pro over two chat sessions totaling roughly four hours to prove a lower bound in zeroth-order convex optimization that had resisted attempts for 30 years, then formalized the result in Lean 4. A different kind of AI-does-math story than the CDC proof: one expert, one model, one hard problem.
Xiaomi and TileRT published MiMo-V2.5-Pro-UltraSpeed on June 8, pushing a one-trillion-parameter model past 1000 tokens per second on a single standard 8-GPU node — no custom silicon, just three carefully chosen co-design decisions applied to a commodity cluster.
SkyPilot published an experiment where giving Claude Code research papers to read before it optimized llama.cpp's CPU backend yielded 15% faster text generation on x86 for about $29. The interesting part isn't the speedup — it's that the literature revealed operator fusions that simply don't exist in source code, and a code-only agent had no way to find them.