페르마의 마지막 정리 형식화 진행 상황

• FLT 증명을 Lean에 옮기는 작업은 두 달째 진행 중이며, Wiles의 “R=T” 정리에 필요한 R과 T의 정의는 아직 완성 전이지만 추상 가환대수 결과 하나는 이미 증명됨
• 목표는 1990년대 원래 증명을 그대로 복제하는 것이 아니라 Diamond/Fujiwara, Kisin, Taylor, Scholze 등의 후속 작업으로 일반화·단순화된 증명을 Lean과 mathlib 위에 세우는 것임
• 현대적 증명에 필요한 crystalline cohomology를 형식화하던 중, divided power 구조의 표준 문헌인 Roby의 1965년 논문에서 핵심 보조정리가 잘못된 것으로 보이는 문제가 드러남
• Brian Conrad가 Berthelot-Ogus 책 부록에서 대체 증명을 찾아냈고, Arthur Ogus도 그 부록의 오류를 고칠 방법을 안다고 답하면서 프로젝트는 다시 진행 가능해짐
• 이 사례는 현대 수학의 세부 증명이 전문가 기억과 암묵지에 기대는 위험을 보여주며, 형식 시스템에 증명을 기록해야 할 실무적 이유를 강화함

---

Lean으로 FLT 증명을 옮기는 현재 상태

• 페르마의 마지막 정리(FLT) 증명을 컴퓨터에 가르치는 작업은 두 달째 진행 중임
• Wiles 증명의 핵심인 “R=T” 정리에서 R과 T가 무엇인지 Lean에 정의하는 데 많은 작업이 필요하며, 아직 두 정의 모두 완성되지 않았음
• PhD 학생 Andrew Yang은 필요한 추상 가환대수 결과를 이미 증명함
  • “추상적인 환 R과 T가 여러 기술적 조건을 만족하면 서로 같다”는 형태의 결과임
• 현재 작성본은 blueprint로 공개되어 있음
• 사용 시스템은 Lean과 수학 라이브러리 mathlib임
• Lean과 수론을 조금 아는 사람은 contribution guidelines, project dashboard, issue를 통해 참여할 수 있음

1990년대 증명을 그대로 옮기지 않는 이유

• 프로젝트는 Wiles의 1990년대 증명을 그대로 형식화하지 않음
• 이후 Diamond/Fujiwara, Kisin, Taylor, Scholze 등의 작업으로 증명이 더 일반화되고 단순화되었음
• 목표는 FLT만 증명하는 데 그치지 않고, 더 일반적이고 강력한 결과까지 Lean 안에 구축하는 것임
• AI 수학 혁명이 실제로 일어나고 Lean이 중요한 구성요소가 된다면, 컴퓨터가 현대 수론의 핵심 정의를 이해 가능한 형태로 갖추는 일이 도움이 될 수 있음

crystalline cohomology를 위해 필요한 divided powers

• 형식화하려는 증명에는 Wiles의 원래 증명에 없던 crystalline cohomology가 사용됨
• 이 이론은 1960~70년대 파리에서 발전했고, Grothendieck의 아이디어를 바탕으로 Berthelot이 기초를 세웠음
• 고전적인 지수함수와 로그함수는 미분기하와 de Rham cohomology 이해에 중요하지만, characteristic p 같은 산술적 상황에서는 그대로 작동하지 않음
• 1960년대 Roby의 논문들에서 발전한 divided power structures는 산술적 상황에서 쓸 수 있는 유사한 함수를 구성하는 데 핵심 역할을 함
• Lean에 crystalline cohomology를 가르치려면 먼저 divided powers를 형식화해야 함

Lean 작업 중 드러난 Roby 문헌의 문제

• Antoine Chambert-Loir와 Maria Ines de Frutos Fernandez는 Lean에 divided powers 이론을 형식화하고 있었음
• 여름 동안 Lean이 표준 문헌의 인간식 논증에 문제를 드러냈고, 확인 결과 Roby의 작업에 있는 핵심 보조정리가 잘못된 것으로 보였음
• 기술적으로는 Berthelot의 논문이 divided powers 이론을 처음부터 전개하지 않고 Roby의 “Les algebres a puissances divisees”를 사용함
  • 해당 논문은 Bull Sci Math, 2ième série, 89, 1965, 75-91쪽에 실림
  • p86의 Lemme 8이 거짓으로 보이며, 증명을 어떻게 고칠지도 명확하지 않았음
  • 그 증명은 Roby의 1963년 Ann Sci ENS 논문에 있는 다른 보조정리를 잘못 인용함
  • 올바른 명제는 Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R)인데, 적용 과정에서 tensor product 하나가 빠졌음
• 이 문제는 module의 divided power algebra가 divided powers를 갖는다는 Roby의 증명을 깨뜨리고, 그 결과 A_cris 환 정의를 막았음

“이론이 틀렸다”보다 “증명이 비어 있다”에 가까운 상황

• crystalline cohomology 자체가 실질적으로 틀렸다는 뜻은 아님
• 주요 정리들은 여전히 맞는 것으로 보이지만, Antoine과 Maria Ines가 따라가던 증명은 불완전했음
• Roby, Grothendieck, Berthelot은 모두 사망했기 때문에 원래 전문가들에게 직접 물을 수 없었음
• 여러 전문가는 중간 보조정리가 거짓이어도 주요 결과의 증명은 고칠 수 있다고 봄
• 형식화에서는 “고칠 수 있을 것”이라는 판단만으로 충분하지 않고, 실제로 고친 증명이 필요함

Berthelot-Ogus 부록이 열어준 우회로

• Tadashi Tokieda가 이 이야기를 Stanford에서 Brian Conrad에게 전했고, Conrad는 crystalline cohomology가 잘못됐다는 이야기가 무엇인지 물어옴
• 기술적 세부사항을 들은 Conrad는 문제가 있어 보인다고 동의한 뒤 검토에 들어감
• 몇 시간 뒤 Conrad는 Berthelot-Ogus의 crystalline cohomology 책 부록에 universal divided power algebra of a module이 divided powers를 갖는다는 다른 증명이 있다고 알려줌
• Conrad 관점에서는 이 접근법이 괜찮아 보였고, 그 덕분에 증명은 다시 진행 가능해짐
• 이후 Berkeley에서 Arthur Ogus와 점심을 먹으며 이 부록이 문제를 해결해줬다는 이야기를 전하자, Ogus는 그 부록에도 여러 오류가 있지만 고칠 방법을 안다고 답함

현대 수학 문헌이 형식화를 필요로 하는 이유

• 이 과정은 인간이 현대 수학을 문서화하는 방식이 충분히 견고하지 않을 수 있음을 드러냄
• 많은 사실이 “전문가들은 알고 있는 것”으로 남아 있고, 문헌에는 정확히 정리되어 있지 않을 수 있음
• 중요한 아이디어는 이런 충격을 견딜 만큼 견고하더라도, 실제 세부 증명은 기대한 위치에 없을 수 있음
• 형식 시스템에 수학을 제대로 기록하면 오류 가능성을 크게 줄일 수 있음
• 형식주의자가 아닌 수학자에게도, 기계가 인간의 논증을 배워 스스로 수학을 하게 하려면 먼저 논증을 기계에 가르치는 과정이 필요함
• Maria Ines는 Cambridge Formalization of Mathematics seminar에서 divided powers 형식화에 대해 발표했고, 해당 문제들은 정리된 것으로 이해됨
• 프로젝트는 다시 궤도에 올랐지만, 문헌이 다시 발목을 잡을 가능성은 남아 있음

[GN⁺]

Hacker News 의견들

• 대학원 때 지도교수의 Birch–Swinnerton-Dyer 추측 계산 접근을 돕기 위해 빠른 코드를 짜던 일이 떠오름
  근처 도시의 정수론 세미나에서 “추측을 뒷받침하는 증거를 강화하려는 것이냐”는 질문을 받았고, 웃으며 “아니요, 차라리 반례를 찾고 싶습니다”라고 답했더니 전문가들이 크게 분노했음
  정수론은 너무 오래되고 깊어서 그 분야 박사논문을 쓰는 것이 초심자가 되는 첫 단계에 가깝고, 표기와 정의는 알아도 그 밑의 직관까지는 닿지 못했음
  그래서 “반례를 기대한다”는 말에 전문가들이 보인 분노는 두려움보다 호기심을 남겼고, 그들이 아직 말로 표현하지 못하지만 보고 있는 것이 무엇인지 궁금했음
  이런 형식화의 진전은 프로그래밍이 더 익숙한 사람에게 수학을 훨씬 접근 가능하게 만들어 줌
  형식성이 부족하다는 불안은 정당하지만, 불안에 대한 올바른 반응은 회피가 아니라 호기심이라고 봄

  • 정수론자는 아니지만, 그 전문가들은 아직 증명되지 않은 추측에 너무 많은 연구 인생을 투자했을 가능성이 큼
    당신 같은 풋내기 신참이 거친 계산으로 반례를 찾아 하루아침에 유명해지면, 그 노력과 구조물이 전부 무너질 수 있으니 화가 났을 것 같음
    예전의 젊은 나에게 수학 대학원 조언을 한다면, 사소하지 않은 “X를 증명하라” 과제마다 시간의 최소 1/4은 반례 찾기에 쓰라고 말하겠음
    과제에서는 99% 실패하겠지만 문제에 대한 통찰은 훨씬 커지고, 나머지 1%에서는 천재처럼 보일 수 있음
    실제 수학 연구에 들어가면 그 확률은 반례 우선 접근에 훨씬 유리하게 바뀜

• 학생 때 친구가 어떤 사람이 세미나 첫날을 마쳤고 모두가 그가 Fermat의 마지막 정리를 증명할 것이라며 흥분했다는 얘기를 해줬던 기억이 있음
  그 사람이 Andrew Wiles였고, 이후 출판 전 발견된 문제를 몇 달간 보완한 뒤 마침내 전체가 출판됐음
  수학을 공부하던 입장에서는 엄청나게 흥분되는 사건이었고, 그래서 “구식 1990년대 증명”이라는 표현을 보면 정말 나이 든 느낌이 듦

  • 90년대 Berkeley 컴퓨터과학 학부생으로 상급 수학 수업을 들었는데, 당시 막 새롭고 흥미롭던 그 구식 증명을 함께 따라갔음
    반의 거의 전부가 수학 대학원생이었고, 자료의 20%도 이해하지 못했던 것 같음
  • 이 이야기를 다룬 훌륭한 TV 다큐멘터리가 있었음

• Lean이 가끔 하는 짜증나는 일을 했다는 대목이 좋음: 표준 문헌의 인간식 논증 제시에 불평했고, 자세히 보니 실제로 인간 논증에 부족한 부분이 있었음
  농담 섞인 짜증과 별개로 이건 대단한 일이며, Lean과 다른 정리 증명기는 앞으로 수학에서 중요한 도구가 될 것 같음

  • 컴파일러도 정확히 같은 습관이 있음

• 현대 수학 문서화가 부실하다는 대목은 UI/UX/웹 디자인과 비슷하게 느껴짐
  디자이너가 비형식적이고 부정확한 목업과 프로토타입, 상호작용 흐름을 만들고 개발자에게 넘기면, 개발자는 그것을 코드로 형식화하고 기계에 정확히 설명해야 함
  그 과정에서 설계가 고려하지 않은 상호작용 시나리오나 코드 경로 같은 구멍을 필연적으로 발견하고, 때로는 큰 설계 결함이 드러나며 개발자나 디자이너가 이를 메워야 함
  설계와 개발은 서로 다른 역할이고 다른 사고방식을 요구하며, 대부분의 디자이너는 개발자처럼 일하고 생각하는 데 강한 저항을 보임

  • “수학을 제대로, 즉 형식 체계 안에 기록하자”는 시도는 이미 Hilbert가 했고 실패했음
    그 실패 이후 우리는 수학을 완전히 형식화할 수 없다는 것을 배웠고, 이는 AI로 수학을 하려는 접근의 근본 문제를 가리킴

• 이 주제에 관심이 있다면 실제 코드를 보는 게 좋음
  예: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
  코드의 전체 구조를 설명하는 청사진도 볼 만함: https://imperialcollegelondon.github.io/FLT/blueprint/
  바깥에서 보는 입장이지만 Lean 코드가 어떻게 생겼고 사람들이 어떻게 기여하는지 보는 것이 매우 흥미로움
  단위 테스트가 필요 없다는 점도 좋음. 어떤 의미에서는 최종 증명 명제가 단위 테스트임

  • 대부분의 큰 Lean 프로젝트에는 여전히 “단위 테스트”가 있음
    예를 들어 어떤 정의가 공허하지 않은지 확인하기 위한 사소한 예시와 반례가 그런 역할을 함

• 순수수학을 했던 입장에서, 큰 문제는 수학자들이 자기완결적인 증명을 거의 제공하지 않는다는 점임
  그렇게 할 유인이 없고, 저자들이 “세부사항 생략”을 자랑스럽게 여기는 경우도 있음
  결국 모든 논리 단계를 따라갈 수 있는 엄밀한 증명을 원하면, 문헌에서 쉽게 찾을 수 없는 빈틈을 전문가가 채워야 함
  그런 사람이 모든 것을 설명하는 책을 써야 가능해지기도 하고, 때로는 그마저도 충분하지 않음
  기록된 내용만 놓고 보면 현대 수학의 많은 부분은 불안정한 기반 위에 있음

  • 현재 순수수학 연구자로서 맞는 말이지만, 쉽게 해결되지는 않는다고 봄
    수학 연구 논문은 해당 분야의 다른 전문가를 위해 쓰이며, 세부사항이 너무 적은 경우도 있어서 동료심사 때 자주 불평하게 됨
    하지만 모든 세부사항을 진짜로 제공하면 논문은 훨씬 길어짐
    고등학교 수학 배경이 탄탄하면 풀 수 있는 예로, 어떤 실수 x > X에 대해 log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx가 되도록 상수 C, X > 0이 존재함을 증명하는 문제를 들 수 있음
    이런 형태의 명제는 해석적 정수론에서 늘 나오고, 전문가에게는 명백해서 논문에서는 거의 항상 증명 없이 적힘
    완전하고 엄밀한 증명을 만들면 길고 재미없으며, 전문가 누구도 읽고 싶어 하지 않을 것임
    이런 태도에 절충 비용은 있지만 관리 가능한 수준으로 보임
  • 누군가 유명한 수학자, 아마 Euler의 작업을 정리하다가 오류를 많이 발견했고 그중 일부는 꽤 심각했지만, 정리 자체는 모두 참이었다는 이야기가 있음
    Tao가 말한 세 번째 단계인 정보를 갖춘 직관처럼 들림
  • 오래전에 수학을 공부했는데, 한 교수는 세부사항을 다루지 않는 것을 자랑스러워했음
    “어떤 것을 100번 해봤다면, ‘쉽게 관찰되듯이’라고 말하고 넘어가도 된다”고 했음
  • 수학 배경은 없어서 순진한 생각일 수 있지만, 증명 검사기가 정리 데이터베이스를 갖고 중간 단계를 채우거나 빠진 단계를 채울 수 있음을 확인할 수 있어야 하지 않나 싶음
    말하자면 머릿속 데이터베이스를 가진 사람이 어떤 정리의 전제조건과 다음 문장의 결론이 맞는지 찾아내는 일을 해야 한다는 뜻으로 이해했음
    아니면 현재 증명 검사기가 평가할 수 있는 방식으로 표현할 수 없는 수학이 있는 건지 궁금함
    혹은 증명 검사기 사용이 생각보다 널리 퍼지지 않았을 수도 있음. 프로그래밍에서 정적 타입 언어의 위치와 비슷하게 들림
  • 이런 태도가 실제로 크게 터진 적이 있는지 궁금함
    즉, 손흔들기로 넘어간 부분 때문에 널리 받아들여진 증명에 치명적 결함이 있었던 경우가 있었는지 묻고 싶음
    그런 일이 없었다면 세부사항을 명시하는 데 느슨한 태도를 보이는 이유도 이해됨

• “crystalline cohomology가 1970년대부터 너무 많이 쓰였으니 문제가 있었다면 오래전에 드러났을 것”이라는 직관이 정말 맞는지 늘 궁금했음
  결함 있는 증명 위에 수학의 한 분야 전체가 개발되고, 그 분야가 단순히 거짓으로 드러나는 일이 정말 그렇게 불가능할까

  • 다른 곳에서도 말했듯이, 이 점이 Vladimir Voevodsky가 Homotopy Type Theory와 Univalent Foundations 프로그램을 시작한 큰 이유였음
    그는 기초 논문의 “첫 페이지 첫 보조정리”에 있는 실수로 한 분야가 무너지는 것을 직접 봤음
    UniMath에 대한 초기 작업과 IAS 특별년, 그리고 HoTT 책으로 이어진 흐름은 수학 형식화 주제를 오늘날의 위치까지 밀어 올렸다고 볼 수 있음
  • 사람들은 자신이 작업 중인 증명에 대해 반례를 찾음
    기초가 틀렸다면 그 반례 중 하나가 기반 정리까지 반증할 수도 있으므로, 잘못된 기초 위에 쌓는 일은 오히려 기초의 결함을 드러낼 가능성이 큼
    비슷하게 수학이 가끔 적용되어 예측을 만들 때, 수학이 틀리면 예측도 틀리고 그 잘못된 예측은 많은 관심을 끎
  • 그 수학 분야가 얼마나 널리 쓰이는지에 달렸다고 봄
    사실 “분야”라는 말은 조금 오해를 부르며, 많은 이론은 수학 전반의 다른 여러 이론과 묶인 매듭에 더 가까움
    그 이론들도 다시 다른 이론들과 연결됨
    이 매듭의 다른 부분에 아무 영향도 없이 기반만 논리적으로 무너진다면 매우 이상한 상황일 것임
    내부적으로는 완전히 일관적이지만 단 하나의 오류만 있는 거대한 부유 수학 덩어리는, 이 글의 코호몰로지 사례에서는 상상하기 어려움
    엄밀히 말하면 철학적 태도에 가깝지만, 현재 수학의 많은 부분이 어떤 의미에서는 자연스럽게 발견되었다고 믿고 싶음
  • 이런 일은 전에도 있었고, Vladimir Voevodsky의 전기를 보면 됨
    스포일러를 하자면 그래도 세상은 계속 돌아갔음

• 지난 1년쯤 학부 복소해석학 과정 일부를 Lean으로 형식화하려고 간헐적으로 시도해 왔음
  배울 점도 많고 보람도 있었지만 때로는 답답했음
  최근에야 C*에서 (-pi,pi] x R로 가는 전단사로서 극형식을 완전히 정의할 수 있었는데, 복소수, 거듭제곱급수, exp, sin을 mathlib에 이미 있음에도 “처음부터” 정의하려고 고집했기 때문임
  어려움의 상당 부분은 수학 학사만 있고 Lean/mathlib에 익숙하지 않으며 지도해 줄 사람이 없어서 생겼을 가능성이 큼. 다만 Zulip 커뮤니티는 매우 도움이 되었음
  mathlib의 많은 결과는 꽤 추상적으로 진술되어 있어, 표준 학부 정리와 어떻게 연결되는지 또는 그런 정리가 mathlib에 있는지 파악하기 어려움
  연구 수학 커뮤니티에는 타당하지만, 개인적으로는 큰 걸림돌이었고 Lean이 교육에 더 쓰인다면 비슷한 문제가 될 수 있음. 다만 시간이 지나면 정리 가능한 부분임
  증명 자동화는 아직 충분하지 않다고 봄
  너무 많은 것들이 마땅히 그래야 할 것보다 증명하기 어렵고, 특히 형 변환이 가장 불만임
  일반 수학에서는 실수가 복소수의 부분집합이라 모든 복소수에 대해 참인 것은 자동으로 모든 실수에 대해 참이지만, Lean에서는 서로 다른 타입이고 단사 사상/형 변환 연산으로 오가야 해서 증명의 핵심이 흐려짐
  자연수를 실수로, 다시 복소수로 바꾸는 식의 형 변환이 쌓이면 특히 지저분해짐
  물론 이는 주제 특유의 문제일 수 있고, 대수학처럼 명시적 사상을 다루는 분야에서는 훨씬 자연스러울 것 같음

  • 이런 상황이라면 Zulip에서 질문을 더 많이 해야 함
    mathlib 사용법, 어떤 것이 존재하는지, 어디에 있는지 안내받기가 정말 쉬움
    겹겹이 쌓인 형 변환 문제는 대체로 norm_cast 전술로 해결됨
    특정 질문이 아니더라도 지나가듯 언급하거나 코드에서 불필요하게 복잡한 증명 스타일이 보이면, 몰랐던 전술에 대한 제안을 받을 수 있음
    형식화가 너무 어렵다는 느낌만 있고 어떤 기법을 써야 할지 모르겠다면, 힘들게 만든 불만족스러운 증명 하나를 고립된 예제로 뽑아 사람들이 더 짧게 줄여 보게 하는 식으로 질문할 수 있음
    이런 질문은 보통 환영받고 모두가 많이 배움

• 이 스레드는 수학을 잘 쓰는 법에 관한 것처럼 보임
  수십 년 동안 수학을 읽고, 쓰고, 가르치고, 적용하고, 출판했으며 응용수학 박사도 받았음
  수학 글쓰기에 문제가 있는 건 맞고, 일부 수학은 형편없이 쓰임
  하지만 꽤 잘 쓰인 수학도 있음
  최소한 모든 기호는 사용 전에 정의해야 하고, 수학을 제시하기 전에 동기를 주면 도움이 되며, 때로는 직관적 설명도 유용함
  잘 쓰인 수학을 주의 깊게 읽는 것이 수학 글쓰기를 배우는 데 도움이 됨
  예로 Paul R. Halmos의 Finite-Dimensional Vector Spaces, R. Creighton Buck의 Advanced Calculus, Tom M. Apostol의 Mathematical Analysis, H. L. Royden의 Real Analysis, Walter Rudin의 Real and Complex Analysis, Leo Breiman의 Probability, Jacques Neveu의 Mathematical Foundations of the Calculus of Probability를 들 수 있음

  • 이건 단순히 수학 글쓰기를 잘하는 문제만은 아님
    글쓴이는 문헌에 전개된 방식 그대로 Fermat의 마지막 정리를 검증하려 했고, 그 과정에서 한 하위 분야를 떠받치던 보조정리가 사용된 형태로는 참이 아님을 발견했음
    그래도 그 분야가 대체로 구제 가능하다고 믿는 이유는, 정말 틀렸다면 누군가 부정적 결과를 이미 찾았을 것이라는 신뢰 때문임
    이제 그 분야를 떠받칠 적절한 대체물을 찾아야 했음

• 글쓴이가 꽤 재미있게 쓰는 사람이라, 절반쯤은 이해하지 못했는데도 읽기 쉬워서 묘한 경험이었음
  증명이 반박되거나 결함이 발견되었을 때 쓸 좋은 단어로 vitiated를 찾았음
  결론이 거짓으로 증명됐다는 오해를 덜 부르면서도, 해당 증명은 손상되었고 새 증명이나 수리가 필요하다는 뜻을 담을 수 있어 마음에 듦

  • 증명이 내장이 꺼내졌다고 표현하면 귀에는 더 즐거울지도 모름