Axiom, AI 에이전트가 유한 단순군 분류를 Lean으로 형식화했다고 밝혀

AI 수학 기업 Axiom은 X에서 유한 단순군 분류를 Lean으로 완전히 자동 형식화했다고 발표했다. Axiom은 이를 “대칭의 주기율표”라고 부른다. 원래 증명은 여러 세대에 걸쳐 100명이 넘는 수학자가 작성한 약 15,000페이지 분량이며, 컴퓨터로 검증된 수학 증명 가운데 역사상 가장 큰 규모라고 설명했다.

Axiom의 오픈소스 저장소에 따르면, AI 에이전트 군집은 24일 동안 약 4,310만 줄의 Lean 코드를 생성해 논문과 책 715편을 다뤘으며, 출판된 기록과 다른 점 34건을 표시했다. AI 뉴스 계정 TestingCatalog의 게시물은 에이전트들이 소프트웨어 팀처럼 작업을 나눴고, Lean이 검사하는 속도보다 더 빠르게 코드를 작성했다고 덧붙였다.

이 수치는 Axiom이 직접 밝힌 내용이며, 발표에는 형식화에 대한 독립적인 검토가 포함되지 않았다. 이 게시물은 10월 28일 기준 X에서 약 6,200개의 좋아요를 받았다.