'Formalizing Fermat's Last Theorem' 공개
AIAI가 만든 글AI(Claude)가 출처를 읽고 쓴 기록이에요. 중요한 내용은 아래 출처에서 확인해 주세요.만드는 방법
'Formalizing Fermat's Last Theorem' 공개 — Claude Fable 5.1과 대략 비등한 수준이라고 설명한 내부 범용 연구 모델로 와일즈의 페르마의 마지막 정리 증명을 Lean으로 형식화. 11일 소요, 출력 토큰 약 60억, Lean 코드 1,300만 줄, 정리 3만 300개 증명(최종 증명에 2만 9,500개 사용)을 보고하고 Lean이 표준 3공리만으로 검증했다고 밝힘. Columbia의 Tianyi Peng 팀이 설계한 협업 형식화 플랫폼 Prove2Me에서 다수 Claude 에이전트가 협업했고, Lean 커뮤니티의 FLT 형식화를 이끌던 Kevin Buzzard(임페리얼)가 검토해 FLT의 첫 종단간 기계 검증 증명이라고 확인했다고 서술. Wiles 원논문이 아니라 Darmon·Diamond·Taylor의 간명화된 서술을 따름
왜 중요한가
인간 커뮤니티가 수년 단위로 진행하던 대형 형식화 과제를 에이전트 군집이 단기간에 수행했다는 주장. 검증 가능한 산출물(Lean 증명)이 결과물이라 벤치마크와 달리 외부 재검증이 가능하다는 점에서 자율 연구 주장 중 검증 난도가 낮은 사례
출처 — 1차 출처를 우선 확인하고, 2차 보도는 「보도」로 따로 표시해요
공식 발표anthropic.comhttps://www.anthropic.com/research/formalizing-fermats-last-theorem2026년 36주차에 더한 기록이에요 · 그 주 보기
노선도에서 — ⑥ 추론 모델·AGI 논쟁 노선
- 앞 역Claude Fable 5.1
- 이 기록'Formalizing Fermat's Last Theorem' 공개
- 다음 역OpenAI, ChatGPT 채팅에 GPT-6과 Intelligent UI 도입