AI가 1만 5천 쪽 증명을 검증했다
수학 최대 증명이 24일 만에 Lean으로
마마우스워리어· 2026년 10월 30일· Axiom, 수학, Lean, AI에이전트, AI과학, 유한단순군· 0
1만 5천 쪽을 24일에 — Axiom, AI 에이전트로 유한 단순군 분류 증명 Lean 검증 주장
걸린 시간
24일
수년짜리 형식화 작업이 한 달 이내로
사람 조직처럼 일했다
이슈를 가져가고 리드가 검토해요.
Lean 코드 분량
4,310만 줄
Axiom 자체 집계 기준
8월 연구의 약 43배
FormaTheoria는 약 99만 줄이었어요.
남은 숙제
수치는 전부 회사 발표예요. 저장소와 전문가의 독립 검증이 필요해요.
— 편집 메모
1 / 8