Claude spent 11 largely autonomous days translating Fermat’s Last Theorem into Lean, producing 13 million lines of code and 29,500 intermediate theorems. The result is a complete computer-checked formalization of Wiles’s 1995 proof, not a new proof of the theorem itself. That distinction matters: formalizing difficult mathematics could shrink the years-long gap between a result being announced and every logical step being independently checked.
The model did not solve the packing problem directly. It repeatedly rewrote the optimizer, checked each candidate with an independent verifier, and kept only genuine improvements. In 15 iterations, that loop beat Packomania's best-known solutions for 10 values of N from 101 to 114, with gains of 2.4% to 5.4%, at a total LLM cost of $27.72. The interesting shift is from asking AI for an answer to using it as a cheap search operator for algorithms.
The interesting part is not that Meta built another agent. AIRA₃ placed eighth out of roughly 4,000 teams in an NVIDIA Kaggle contest, fine-tuning a 30B Nemotron model against a private test set. It gets there with long-running agents working in isolated environments, sharing hypotheses through a forum and artifacts through a filesystem, without a central planner. That architecture points toward research systems that improve by coordinating exploration, not just by scaling one model.
The interesting result is not that Qwen3.8-27B can be compressed. It is that a task-aware quant reportedly scores 82.81% on the reasoning test, just 0.78 points behind BF16 at roughly 15% of the size, while byte-matched Unsloth IQ2_S reaches 77.34%. That points to a practical rule for local inference: where you spend the remaining bits matters more than the headline bit count.
Most LLM agents still stop, call a tool, append the result, and start again. Yandex argues the bottleneck is not necessarily model training but how inference state is scheduled: shared KV-cache branches could let perception, reasoning, tool use, and action progress concurrently, while revising a trajectory without recomputing everything. The proposal points toward more responsive agents for robots, games, and live software, without changing model weights.
The usual trick is to store the video somewhere. This experiment instead trains a 417,000-parameter recurrent dynamical system to roll the entire Bad Apple animation forward from one initial state, with no frame-by-frame playback loop. That makes the demo more than a meme: it is a compact test of whether learned dynamics can turn a static seed into a long, structured sequence, and a striking alternative to the earlier SIREN-style implicit-memory approach.
A single leaderboard snapshot can hide a model getting worse at the work you actually care about. In a study spanning eight models, four tasks, and eight languages, Gemini 2.5 Pro led overall at 4.73/5, yet no model won everywhere, and GPT-5’s strengths in translation did not carry over to content generation in Chinese and Polish. The practical fix is repeated, task-specific evaluation, not blind trust in release-era scores.