AI agents just machine-checked the longest proof in mathematics 🧮

Some proofs are so long that checking every step by hand is almost impossible. The Classification of Finite Simple Groups is the most famous example: roughly 15,000 pages, spread over more than 500 articles by about 100 mathematicians, nicknamed "the enormous theorem". On 26 October, Axiom Math released what it calls the first complete computer-checked proof of it, written in the Lean proof assistant. For me, this is one of the most beautiful agent stories of the year.

What was actually done

Finite simple groups are the "atoms" of symmetry. The classification says every one of them is either a cyclic group of prime order, an alternating group, one of sixteen infinite families of groups of Lie type, or one of exactly 26 sporadic groups, the largest being the Monster with about 8 × 10^53 elements.

Axiom rewrote the first-generation proof in Lean, a language precise enough that a computer checks every single logical step. The public repository is "sorry-free", which means no step was skipped or left as an assumption, and it uses only Lean's standard axioms. The final statement is short: every finite simple group is isomorphic to a group on the classification list.

How the agents worked

This is the part that fascinates me as someone who builds agent systems. The project started on 1 October with a Slack channel and a proof map assembled from the literature, split into 108 milestones and about 380 smaller tasks. Over 24 days, engineers and mathematicians directed swarms of dozens of AI agents that produced about 43.1 million lines of Lean.

Agents claimed tasks through GitHub issues, delegated missing prerequisites to other agents, and pushed results into a shared repository. Lead agents broke down hard arguments and reviewed statements. Engineers built a shared build cache because agents were writing proofs faster than Lean could recheck them. And when early milestones turned out to rest on unproven assumptions, the team deleted tens of thousands of lines and replanned. That honesty about what failed is exactly what makes the result convincing.

What the machines found

Formalization does not let you wave your hands. The agents surfaced 34 noteworthy deviations from the published record. Most were small, like typos, table errors or dropped hypotheses. One was substantial: in John Walter's 1986 route to the Unbalanced Group Theorem, the agents found explicit counterexamples to a closure assertion. Working with group theorists Richard Lyons and Ronald Solomon, AxiomProver produced and formalized an alternative argument, including a new result Axiom calls "Preservation of simple tops", written up in an accompanying paper.

The honest part

Axiom is careful here, and I appreciate it. Humans still have to check that the formal statement really says what we mean; Lean checks the deductions. The formalization also follows a different route than Walter at one point, so it is not a step-by-step replay of the history. The errata list is still being compiled with an advisory board of group theorists. The theorem itself remains the achievement of the mathematicians who built it.

Why it matters

Results across algebra, number theory and even physics lean on this classification, often in one sentence. Now that dependency is explicit and checkable. And for agent builders, it shows a pattern worth copying: many agents, a shared dependency map, and a strict machine checker that refuses to accept "looks right".

Sources

Decades of human insight, now checked line by line. That feels like a good use of AI.

Reacties

Een reactie posten

Populaire posts van deze blog

Meta just shared the full recipe for a 30B agent model you can run at home 🧠

When Meta released Muse Glimmer in August, the pitch was simple: an open-weight, Apache 2.0 model built for AI agents that run on your own Mac or PC. What was missing was the "how". On 19 October, Meta Superintelligence Labs published the full technical report, and for anyone who cares about distillation and local agents, it is one of the most useful reads in a while. What the model is Muse Glimmer is a dense model of about 29.6 billion parameters, including a 1.8B perception encoder, so it reads text and images and writes text. It has a 128K+ context window and was trained on data from more than a hundred languages. The design goal was strict: everything has to fit in 32 GB of GPU memory, and a smaller 4-bit variant targets 24 GB cards. The parts I found most interesting Dense beat mixture-of-experts here. That surprised me. The team trained scaling ladders for a dense model and two MoE designs with the same memory footprint. Under a fixed memory ceiling and their compu...
Meer lezen

AI that can actually "see" a crystal 🔬

Most of the solid stuff around us, from battery materials to chips, is made of crystals: atoms stacked in neat, repeating 3D patterns. Large language models are great at reading papers about those materials, but they have never really looked at the structures themselves. A team at MIT just showed a clever way around that, and the trick is one I keep coming back to: good synthetic data. What they built The model is called CLaC, short for Contrastive Language-Crystal model, and it is described in a paper in Nature Communications by Yang Jeong Park, Mayank Kumaran, Chia-Wei Hsu, Elsa Olivetti and Ju Li. MIT News covered it on 18 October 2026. If you know CLIP, the model that taught image generators to connect pictures and words, you already get the idea. CLaC has two branches: a graph neural network that reads the 3D crystal structure, and a text encoder that reads a description. Contrastive training pulls matching structure-text pairs together in one shared space and pushes mismatche...
Meer lezen

A 35B model on a Mac mini, using just 2.9 GiB of memory 🚀

There's something special about running a capable language model on hardware you own: no API bill, no data leaving the house, just a small box on your desk doing the thinking. A paper that's currently #2 on Hugging Face's trending list takes that idea further than I expected: it runs a 35-billion-parameter model on a Mac mini at about 20 tokens per second while using under 3 GiB of memory. The trick: leave the experts on the SSD The paper is called The Other Half of the Memory Wall: Serving 35B MoEs from SSD with Trained Routing Prediction , and the system is named Edge0 . It builds on a Mixture-of-Experts (MoE) model, Qwen3.6-35B-A3B. In an MoE, each token only uses a few "experts" per layer (here 4 out of 256 in each of 40 layers), so most of the weights sit idle at any given moment. Edge0 takes that literally. The expert weights (quantized to int4) stay on the SSD and are streamed in only when needed. The clever part is a small prerouter : a tiny trained he...
Meer lezen