Shanghai AI Lab's Intern-S2 ground through the long derivations on a 1995 chaos problem while Xu Disheng's team steered, then Peking University machine-checked every core theorem in hundreds of thousands of lines of code, so the scarce skill in math is becoming knowing where to point the model.