Axiom Math: dziesiątki agentów AI przepisały w Lean najdłuższy dowód matematyki w 24 dni

Axiom Math, firma budująca system AI do dowodzenia twierdzeń, opublikowała 26 października kompletny, sprawdzony przez komputer dowód klasyfikacji skończonych grup prostych. To twierdzenie mówi, z jakich niepodzielnych "atomów" składa się każda skończona grupa symetrii, a jego oryginalny dowód rozciąga się na około 15 tysięcy stron. Axiom przepisał go w języku Lean, w którym definicje i dowody zapisuje się tak dokładnie, że komputer sprawdza każdy krok, a krok bez uzasadnienia po prostu się nie kompiluje. Zajęło to 24 dni i dziesiątki agentów AI.

Sama matematyka obchodzi mnie tu mniej niż to, że mamy jeden z największych opisanych projektów kodu napisanego głównie przez roje agentów, a jego autorzy piszą wprost, co się psuło. Trzeba przy tym pamiętać, że to relacja samej firmy. Sprawdzić da się repozytorium, listę błędów znalezionych w literaturze i artykuł z nowym dowodem jednego twierdzenia, a liczby o tempie i skali przyjmuję na słowo.

Kamienie milowe na GitHubie, raporty na Slacku