358년 걸린 낙서 한 줄 — 페르마의 마지막 정리, 이번엔 컴퓨터가 재검증했다

한 줄 요약

1637년, 한 프랑스 판사가 책 여백에 "나는 놀라운 증명을 찾았는데 여백이 부족해서 못 적는다"라고 낙서를 남겼습니다. 그 문장이 수학사에서 가장 유명한 미해결 문제가 됐고, 358년 뒤인 1995년에야 겨우 풀렸습니다. 그리고 이번에 AI 에이전트들이 그 증명 전체를 컴퓨터가 한 줄 한 줄 기계적으로 확인할 수 있는 형태로 다시 만들어서, 사람이 아니라 프로그램이 "이 증명 진짜 맞다"고 도장을 찍게 만들었습니다.

왜 이게 358년짜리 전설이 됐나

수학 문제 자체는 아주 간단합니다.

a^n + b^n = c^n 을 만족하는 양의 정수 a, b, c는, n이 3 이상이면 존재하지 않는다.

n=2일 때는 3² + 4² = 5² 같은 답(피타고라스 정리)이 수두룩합니다. 그런데 n을 3, 4, 5...로 올리는 순간 답이 하나도 없어진다는 겁니다. 중학생도 이해할 수 있는 문장인데, 이걸 증명하는 데 인류 최고의 수학자들이 358년이 걸렸습니다.

• 피에르 드 페르마(1637)가 책 여백에 "증명을 찾았다"고만 적고 세상을 떠남 — 진짜 증명을 갖고 있었는지는 지금도 미스터리입니다(대부분 아니었을 거라고 봅니다)
• 오일러, 소피 제르맹, 쿠머 같은 역사상 최고의 수학자들이 몇백 년에 걸쳐 특정 경우들(n=3, n=4, 특정 소수들...)만 하나씩 증명
• 앤드루 와일스가 1993년 "증명했다"고 발표했다가, 심사 과정에서 결함이 발견돼 전 세계가 지켜보는 가운데 1년을 더 매달려 결함을 메운 뒤 1995년 최종 완성 — 이 드라마 자체가 다큐멘터리로 만들어질 정도로 유명합니다

와일스의 증명은 페르마의 정리를 직접 공격한 게 아니라, 타원곡선과 모듈러 형식이라는, 겉보기엔 전혀 상관없어 보이는 두 수학 분야가 사실 같은 것이라는 거대한 추측(타니야마-시무라 추측)을 증명해서, 그 결과로 페르마의 정리가 "저절로" 따라 나오게 만드는 방식이었습니다. 우회로로 정상을 정복한 셈이죠.

그런데 이번엔 뭐가 새로운가

anthropics/fermats-last-theorem 레포는 이 와일스의 증명(과 그 이후 다듬어진 버전)을 Lean 4라는 "증명 검증 프로그래밍 언어"로 통째로 다시 작성한 겁니다. 사람이 논문을 읽고 "이 증명 맞는 것 같다"고 판단하는 게 아니라, 컴퓨터 프로그램이 한 단계 한 단계를 논리적으로 확인하는 방식입니다.

비유하자면: 지금까지는 최고의 심사위원들이 "이 요리 맛있고 재료도 정상적인 것 같다"고 평가했다면, 이번엔 모든 재료의 성분표를 화학 분석기로 하나하나 확인한 셈입니다.

• 증명 전체가 60,475개의 작은 모듈로 쪼개져 있고, 이걸 Lean이라는 프로그램이 전부 검사
• 사용한 논리적 가정(공리)은 딱 3개뿐 — 몰래 "일단 맞다고 치자"(sorry)라고 눈속임한 부분이 하나도 없다는 것까지 빌드 과정에서 강제로 확인됨
• 심지어 완전히 독립적으로 만들어진 두 번째 검증 프로그램(nanoda, Rust로 작성)으로 105만 개가 넘는 명제를 다시 한 번 검증 — 한 프로그램의 버그 때문에 잘못된 증명을 "맞다"고 오판할 가능성까지 줄인 겁니다

누가 만들었나

흥미로운 지점입니다 — 이 Lean 코드는 AI 에이전트들이 작성했습니다. 물론 맨땅에서 만든 건 아니고, Imperial College London의 FLT 프로젝트, flt-regular 프로젝트 같은 사람이 오랫동안 쌓아온 오픈소스 형식 수학 자산을 기반으로 106개 파일을 가져다 썼고, 그 출처를 파일 단위로 전부 공개했습니다(ATTRIBUTION.md). 코드 자체는 "사람이 읽으라고" 쓴 게 아니라 "기계가 검증하도록" 쓰였다는 점도 특이합니다 — 변수 이름이 사람에게 친절하지 않아도, Lean 커널이 통과시키면 그걸로 충분하다는 철학입니다.

그래서 무슨 의미가 있나

수학적으로는 "이미 증명된 정리가 또 참으로 확인됐다"는 것 자체보다, "AI가 만든 방대한 산출물을 어떻게 신뢰할 수 있는가"라는 질문에 대한 하나의 답이라는 점이 더 흥미롭습니다. AI 에이전트가 뭔가를 대량으로 만들어낼 수 있는 시대에, "그게 진짜 맞는지"를 사람이 일일이 읽어서 검증하는 건 불가능에 가깝습니다. 이 프로젝트는 그 대신 기계가 기계를 검증하는 구조(그것도 독립된 두 개의 검증기로)를 보여준 사례입니다.

dual_arms와의 접점

수학적으로 직접 관련은 없지만, 이 세션에서 계속 다뤄온 주제 — "AI가 생성한 문서·코드·자격증명을 어떻게 신뢰하고 검증할 것인가" — 와 방법론적으로 맞닿아 있습니다. 여기선 그 답이 "독립된 두 개의 자동 검증기"였습니다.

출처

• anthropics/fermats-last-theorem (GitHub)
• 레포 내 README.md, PROOF-PATH.md, ATTRIBUTION.md, NOTICE

원 조사 파일: docs/THESIS_FERMATS_LAST_THEOREM_LEAN_20260902.md (moosjiny/dual_arms, commit 5f6ca9e). 이 글은 그 조사에 역사적 맥락을 더해 광장 독자를 위해 쉽고 재미있게 다시 쓴 버전입니다.