페르마를 린으로 열하루 만에 검증했습니다 | DAKER 커뮤니티

Anthropic이 2026년 9월 4일 연구 글로, Claude가 Lean으로 페르마의 마지막 정리(FLT)를 처음부터 끝까지 컴퓨터 검증한 증명을 공개했습니다. 원문은 Formalizing Fermat's Last Theorem입니다. 오늘은 검증·형식화 각도만 정리합니다.

나온 것

1. Claude가 약 11일 동안 거의 자율적으로 FLT의 종단간(Lean) 증명을 썼습니다. 원문은 In 11 days, working largely autonomously, Claude produced the first end-to-end, computer-checked proof of FLT라고 적습니다. 사람이 새 수학을 만든 소식이 아니라, 기존 증명을 기계가 검사할 수 있는 형태로 옮긴 검증 소식입니다.

2. 과정에서 Lean 코드 약 1,300만 줄과 중간 정리 약 29,500개를 썼습니다. 원문은 wrote 13 million lines of Lean and proved 29,500 intermediate theorems라고 적습니다. 최종 경로에서 쓰인 중간 정리와, 도중에 생성된 정리 수를 구분해서 읽으십시오.

3. Kevin Buzzard가 검토 소감을 남겼습니다. 원문은 이 자동형식화가 FLT를 수학의 공리만으로 증명하며, 대수·조화해석·기하·정수론의 자동형식화와 재사용 가능한 산출물을 보여 준다고 전합니다. 「인간 검증이 불필요해졌다」고 단정하지 마십시오.

4. Prove2Me 플랫폼이 전환점이라고 설명합니다. 초반 시도는 상태 추적·협업이 무너져 실패했고, 실패분이 최종 비보일러플레이트 줄의 약 7%를 기여했다고 합니다. Prove2Me는 정리 DAG, 문장·증명 파일 분리, 자연어 설명 검색으로 병렬 작업을 도왔다고 적혀 있습니다.

5. 사람 개입은 고수준 지시 수준이었다고 합니다. 예로 「Jacobian as a scheme sounds high priority」「push Mazur to be done soon」 같은 지시가 인용됩니다. 세부 증명 단계를 사람이 손으로 채웠다는 뜻이 아닙니다.

6. 산출물은 Lean 표준 공리 셋으로 검사됐고, Mathlib의 FLT 문장과 비교기로 일치했다고 합니다. 원문은 just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT라고 적습니다.

7. 토큰·모델 규모도 공개됐습니다. Prove2Me와 Claude Code 기반 멀티에이전트 하네스로 약 2주 안에 끝냈고, 일반 목적 내부 연구 모델에서 출력 토큰 약 60억 개를 썼으며 Fable 5.1과 대략 비슷한 급이라고 적습니다. 소비자 Max 요금제 세 개로 Vinogradov Three Primes를 3일 만에 형식화한 소규모 실험도 소개합니다.

8. GitHub에 전체 증명과 해설이 있습니다. 원문 Learn more는 The full proof is available on GitHub along with a written walk-through라고 안내합니다. 이 잡담에서는 공격·우회 코드가 아니라 형식화 산출물 링크만 다룹니다.

Riemann 가설 관련 AI 작업과 목적을 섞지 마십시오. 원문은 Unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what’s novel here is the verification이라고 대조합니다. 오늘은 「새 정리 발견」이 아니라 「검사 가능한 형식화」입니다.

Wiles 1995 증명과 Darmon–Diamond–Taylor 해설을 따릅니다. 원문은 Claude’s proof follows a simplified version of Wiles’s proof from Darmon, Diamond and Taylor라고 적습니다. Fermat 본인이 여백에 적은 「놀라운 증명」이 맞았다고 주장하지 않습니다. 원문은 초등 증명이 없어 Fermat의 원래 증명은 틀렸을 가능성이 크다고 적습니다.

Buzzard의 Imperial College FLT 프로젝트·flt-regular·Mathlib·Lean FRO 기여를 인정합니다. 자동형식화가 커뮤니티 기반 없이 혼자 이룬 일로 포장하지 마십시오.

형식화는 심사 부담을 줄이는 도구로 소개됩니다. Buzzard는 현대 문헌의 자동형식화, 오류 탐지, 심사 부담 완화, LLM 생성 수학의 엄밀 검사에 도움이 된다고 말합니다. 「논문 심사가 사라진다」고 쓰지 마십시오.

Prove2Me 논문도 링크됩니다. Chen et al., Prove2Me: An open collaborative platform for scaling math formalization, arXiv:2608.28433. 플랫폼 이름만 단독 제품 광고처럼 쓰지 말고, FLT 캠페인에서의 역할을 적으십시오.

Mythos·Fable 캐시 가격·EFS 각도와 섞지 마십시오. 이미 올린 모델·안전장치 글과 제목을 재탕하지 않습니다. 오늘은 Lean FLT 형식화입니다.

에이전트 실패 기록도 사실입니다. 초반 실패와 7% 기여를 숨기지 마십시오. 성공 서사만 남기면 재현 조건이 흐려집니다.

소비자 요금제 실험은 「가능」 사례입니다. Max 세 자리로 Three Primes를 3일에 끝냈다는 문장은 소규모 실험입니다. 모든 정리를 같은 비용으로 할 수 있다고 일반화하지 마십시오.

형식화 결과물을 읽는 순서를 정하십시오. 먼저 Mathlib FLT 문장 일치 여부, 다음 Lean 검사 로그, 다음 GitHub 해설, 마지막에 에이전트 사고 발췌를 봅니다. 발췌만 보고 증명 완료라고 팀에 알리지 마십시오.

토큰 60억·Max 세 자리 실험은 규모 감각용입니다. 예산 산정에 그대로 넣지 말고, 재현 시 Prove2Me·하네스·모델 급을 먼저 맞추십시오. 내부 연구 모델과 공개 Fable 5.1을 동일하다고 단정하지 마십시오.

수학 커뮤니티 기여를 각주에 남기십시오. Wiles·Taylor, Darmon–Diamond–Taylor, Buzzard 프로젝트, Mathlib·Lean FRO 없이 자동형식화만으로 서술하면 맥락이 빠집니다.

실패율 7% 기록도 남기십시오. 초반 협업 붕괴를 숨기면 팀이 같은 함정에 빠집니다. Prove2Me DAG와 문장·증명 파일 분리를 재현 조건에 넣으십시오.

Mythos·캐시·EFS 폴더와 분리하십시오. 오늘은 Lean FLT 검증 각도만 유지합니다.

GitHub 클론 후 로컬 Lean 버전을 맞추십시오. 원문 저장소가 요구하는 툴체인과 Mathlib 커밋을 README에서 확인합니다. 버전을 섞으면 검사 실패를 모델 오류로 오해할 수 있습니다.

중간 정리 재사용 규칙을 팀에 공유하십시오. Prove2Me가 자연어 설명을 유지한 이유가 검색·재사용입니다. 새 캠페인에서도 정리 문장을 먼저 등록하고 증명을 붙이는 순서를 지키십시오.

고수준 지시 로그만 남겨도 재현에 도움이 됩니다. Jacobian·Mazur 우선순위 같은 지시가 경로를 바꿨습니다. 자동 실행만 기록하고 사람 지시를 버리면 실패 분석이 어려워집니다.

형식화와 해설 글을 둘 다 요구하십시오. 원문도 형식화가 인간 가독 해설을 대체하지 않는다고 합니다. 팀에 제출할 때는 Lean 통과와 해설 요약을 한 세트로 받으십시오.

과학 크레딧·할인 구독 안내도 원문에 있습니다. 외부 수학 연구자 지원 확대를 언급합니다. 필요 시 Anthropic 연구 지원 페이지를 별도 확인하십시오.

FLT는 예시이며 모든 정리가 같은 일정으로 끝난다고 쓰지 마십시오. 복잡도·선행 라이브러리 커버리지에 따라 기간이 달라집니다.

발표 슬라이드에는 검증과 발견을 두 구역으로 나누십시오. 왼쪽에는 Lean 검사·Mathlib 일치, 오른쪽에는 신규 수학이 아님을 명시합니다. 한 문장으로 섞으면 오해가 납니다.

관련 권장 읽기 목록도 원문에 있습니다. Lean 역사 책, BBC 다큐, Wadler의 Propositions as Types, Prove2Me 논문, Asterisk Magazine 글을 필요에 따라 팀에 공유하십시오.

팀 세미나에서는 11일과 1,300만 줄만 강조하지 마십시오. Prove2Me 전환 이전 실패와 7% 기여를 같이 말해 재현 조건을 지킵니다.

공개 링크 제출 시 GitHub 커밋 해시를 적으면 추적이 쉬워집니다. 태그 없는 main만 남기지 마십시오.

아닌 것

새 수학 정리의 최초 발견 발표가 아닙니다. 검증·형식화입니다.

Fable 5.1 캐시 인하·Mythos 접근 재공지가 아닙니다.

인간 심사·수학자 역할이 끝났다는 뜻이 아닙니다.

공격용 코드·우회 절차를 적는 글이 아닙니다.

오늘 할 일

첫째, 원문에서 11일·1,300만 줄·29,500 정리·Prove2Me 문장을 표시하십시오. Anthropic — Formalizing Fermat's Last Theorem (2026-09-04)

둘째, GitHub 증명과 해설 위치를 확인하십시오. 원문 Learn more 안내를 따르십시오.

셋째, 「발견」과 「검증」을 팀 문서에서 분리해 적으십시오. Riemann 계열 신규 수학 작업과 섞지 마십시오.

넷째, Prove2Me·DAG·파일 분리 설계를 재현 체크리스트에 넣으십시오. 상태 추적 실패 사례도 같이 적으십시오.

다섯째, Lean 검사·Mathlib 문장 일치 문장을 인용 규칙으로 두십시오. 스크린샷만으로 「증명 완료」라고 단정하지 마십시오.

여섯째, 확인한 링크를 공개로 남기십시오. 올린 링크가 제출입니다.

한 페이지 요약

Anthropic은 Claude가 약 11일 동안 Lean으로 FLT를 종단간 컴퓨터 검증했다고 공개했습니다. 약 1,300만 줄과 중간 정리 약 29,500개가 언급됩니다. Prove2Me와 멀티에이전트 하네스가 전환점이었고, 초반 실패분도 일부 남았습니다. Lean 표준 공리로 검사됐고 Mathlib FLT 문장과 일치했다고 합니다. 목적은 신규 발견이 아니라 검증 가능성과 심사 부담 완화입니다. GitHub에 증명과 해설이 있습니다.

출처: Anthropic Research — Formalizing Fermat's Last Theorem (2026-09-04)