15 000 страници математика за 24 дни: ИИ агенти проверяват „огромната теорема“ с компютър
Стартъпът Axiom съобщава, че е формализирал изцяло в системата за проверка на доказателства Lean доказателството на класификацията на крайните прости групи – с рояци от ИИ агенти. Независимо възпроизвеждане все още няма.
Графика: TERRA WORLD NEWS (собствена графика по данните от източниците)
Класификацията на крайните прости групи се смята за най-дългото доказателство в математиката: около 15 000 страници в над 500 научни статии от около 100 математици в продължение на десетилетия. Стартъпът Axiom Math съобщава, че е пренесъл цялото доказателство на езика на системата Lean, в която компютърът проверява всяка логическа стъпка. За целта десетки ИИ агенти са работили в рояци 24 дни; резултатът е около 43,1 млн. реда Lean код.
Според Axiom агентите са открили 34 съществени отклонения от публикуваната литература; важните от тях са проучени от математици. Axiom се е консултирала с теоретиците на групите Ричард Лайънс и Роналд Соломон. Хора са проверили и дали формалните твърдения наистина изразяват търсената теорема. Понятието „огромната теорема“ въвежда някога математикът Даниел Горенстейн.
Че това е първото напълно проверено с компютър доказателство, засега е твърдение на самата Axiom. На въпроса дали някой извън компанията вече е възпроизвел и проверил доказателството, главният изпълнителен директор Карина Хонг отговаря според RuntimeWire: „Все още не.“ Axiom публикува файловете за изграждане, за да насърчи външни групи да го направят.