Shanghai AI Lab's Intern-S2 helped close a 30-year conjecture
An AI-assisted proof landed in a form mathematicians can actually audit — and a second team with different tools checked the work.
The arXiv paper proving the codimension-one case of a conjecture Étienne Ghys posed in 1995 now carries an explicit declaration of AI use: its author, Jiesong Zhang, says he used an internal version of Shanghai AI Lab's Intern-S2 "to assist in developing the mathematical ideas and arguments" across multiple rounds of dialogue, and thanks Shanghai AI Lab and Bowen Zhou by name. The declaration arrived in the paper's third revision on October 13, alongside a statement on formalisation — meaning the AI's role is documented in the primary artifact rather than in a press release, which is still rare enough to be notable on its own. Independently, a Peking University team led by Bin Dong and Ruochuan Liu formalised the four main theorems in Lean 4 using SHEAF, their agent pipeline, so a machine has checked that the proofs actually imply the statements. The public repository is substantial: more than 4,200 Lean files in a tree that includes the parts of Ghys's own 1995 classification the argument leans on.
The lab's framing — a 30-year-old world-class problem, solved with a Chinese model — is accurate in outline and narrower than the slogan suggests. What was settled is the codimension-one case, which covers complex dimension three; the general conjecture is untouched, and Zhang states that he independently verified every argument and takes full responsibility for the manuscript, which is the correct way to describe a tool-assisted proof. The operational numbers circulating this week — seven rounds of deduction, a problem graph expanding from 15 nodes to 389, roughly 100 parallel agents and five days for the formalisation — come from the lab's own write-up and appear nowhere in the paper, so treat them as the lab's account rather than a measured result. Claims that Intern-S2 beats Gemini 3.1 Pro on proof benchmarks belong to the model's launch materials, not to this work; Chinese coverage reporting the same announcement says only that scores were comparable.
The part worth keeping is the verification split. A proof produced with model help was checked by a second, unrelated team's agents, in a different institution, against a proof assistant that does not care who wrote it — and the output is a repository anyone can clone. That is the same shape as React's creator closed Conway's 50-year-old conjecture with AI, where the value was an auditable Lean artifact rather than the claim. Formalisation is turning into the referee that human review never quite was for machine-assisted math, and the labs that embrace it will have a much easier time being believed.
Kunlun Tech released Matrix-Game 4.0, which it calls the first video-model game that runs in real time on a single consumer GPU. The company says the system plays at 480p and 60 frames per second on one RTX 5090, with under 150 milliseconds from keypress to a reacting frame, and it ships open source: code, weights and the structural meshes, with the model weights released under Apache 2.0. The architecture is the interesting decision — a game engine keeps world state and collision and score rules in ordinary code, while a video model adapted from Wan2.2 5B renders the picture from the engine's simplified geometry, so the world does not have to live inside a model's memory. That is a different bet from the fully generative route, and it is why the latency numbers are plausible at all.
Keep the performance figures at arm's length. The 60 FPS, 112-millisecond and 18.5 GB VRAM numbers are the company's own, with no third-party reproduction, and the repository's only published throughput table is for an A100 rather than the 5090 it headlines; the project page still labels itself a preview with the paper promised. Against Nvidia's StreamRender-H3, which needs eight GB200s, the claim is that a consumer card does the job — worth watching, not yet worth repeating. If it holds up, the interesting consequence is not games; it is that interactive video generation stops being a datacenter product. Background: AI 101 — What is a world model?.
What to watch: whether Shanghai AI Lab packages the verification loop into its scientific platform as promised, and whether anyone outside Kunlun reproduces the 5090 numbers.
Machine-checked proofs are becoming the price of admission for AI math claims — should journals require a Lean artifact before they'll review the paper? Tell us in the comments.
