Axiom zegt dat AI-agenten de classificatie van eindige enkelvoudige groepen in Lean hebben geformaliseerd

Axiom, een AI-wiskundebedrijf, maakte op X bekend dat het de classificatie van eindige enkelvoudige groepen volledig automatisch heeft geformaliseerd in Lean. Het noemt dit resultaat de "periodieke tabel van symmetrie". Volgens het bedrijf besloeg het oorspronkelijke bewijs ongeveer 15.000 pagina's en is het gedurende meerdere generaties opgesteld door meer dan 100 wiskundigen. Het noemt dit het grootste wiskundige bewijs uit de geschiedenis dat door een computer is geverifieerd.

Volgens de open-sourcerepository van Axiom produceerden zwermen AI-agenten in 24 dagen ongeveer 43,1 miljoen regels Lean-code, waarmee ze 715 artikelen en boeken bestreken. Ook signaleerden ze 34 afwijkingen van de gepubliceerde literatuur. In een bericht voegt het AI-nieuwsaccount TestingCatalog eraan toe dat de agenten het werk verdeelden als softwareteams en sneller code schreven dan Lean die kon controleren.

Deze cijfers zijn afkomstig van Axiom zelf; de aankondiging omvat geen onafhankelijke beoordeling van de formalisering. Op 28 oktober had het bericht ongeveer 6.200 likes op X.