All 15,973 semigroups of order 6 classified by AI agents in Lean

Bartosz Naskręcki@nasqret

Major announcement in mathematical formalization!

Finally, after 3 months of very intensive, nonstop work by several AI agents (Codex and Claude Code), we have settled a classification of ALL 15,973 semigroups of order 6. Every one of the 15,969 that has a finite basis now has it written down explicitly, and the remaining 4 are proved to have none at all.

The whole list of bases is produced for the first time in history. Until now, for most of these semigroups, mathematicians only knew that a basis exists; nobody had ever written one down. The formalization in Lean, orchestrated with a multi-agent approach, reached more than 5 MILLION lines of verified Lean code, one of the largest auto-formalization projects to date.

It's been an amazing joint work with @JanotaMikolas and @Jan_Hula, accompanied by senior experts in semigroup theory, João Araújo and Edmond W. H. Lee.

Our paper describing this project, "Proving at Scale for Universal Algebra", has been accepted at the MATH-AI workshop, NeurIPS 2026!

When we launched this project, we were a bit pessimistic: producing proofs for 15,973 semigroups seemed out of scope for the current technology. But with a careful setup (agents communicating through a mailbox we arranged, orchestrating the effort with a custom method of bootstrapping and auto-research), it has finally come to the finish line. The last 390 semigroups took 23 more days. The very last one needed a whole structural analysis before its proof could even be written.