Axiom twierdzi, że agenci AI sformalizowali w Lean klasyfikację skończonych grup prostych

Axiom, firma zajmująca się matematyką AI, ogłosiła na X pełną automatyczną formalizację w Lean klasyfikacji skończonych grup prostych — wyniku, który nazywa „układem okresowym symetrii”. Opisuje oryginalny dowód jako liczący około 15 000 stron i napisany przez ponad 100 matematyków z kolejnych pokoleń. Nazywa go też największym dowodem matematycznym w historii zweryfikowanym komputerowo.

Według repozytorium open source Axiom roje agentów AI stworzyły około 43,1 miliona wierszy kodu Lean w 24 dni, obejmując 715 artykułów i książek oraz wskazując 34 rozbieżności z opublikowanymi materiałami. W poście konto informacyjne o AI TestingCatalog dodaje, że agenci podzielili pracę jak zespoły programistyczne i pisali kod szybciej, niż Lean mógł go sprawdzać.

Te liczby pochodzą z relacji samego Axiom; ogłoszenie nie obejmuje niezależnej weryfikacji formalizacji. Do 28 października post miał około 6 200 polubień na X.