Claude, 11일 만에 페르마의 마지막 정리 증명을 컴퓨터로 검증하다

>우리가 이 증명을 생산할 수 있었던 속도는 이제 수학의 광범위한 영역을 형식화하는 것이 가능해졌음을 보여주며, 이는 수학적 증명의 공통된 체계에서 오류를 발견할 수도 있고 새로운 연구의 심사를 줄이는 데 도움이 될 수도 있습니다.

^ 이 부분은 제 생각에 처음 몇 문단에 있었어야 합니다. 왜 이것이 중요한지에 대한 설명이 너무 아래에 있어서는 안 됩니다.

"그 증명은 제가 Khare, Taylor 등의 아이디어를 따라 직접 형식화해 온 현대적 증명이 아니라, Langlands–Tunnell 정리와 Ribet의 레벨 낮춤 정리를 통한 Wiles–Taylor–Wiles 논증에 대한 1995년 Darmon–Diamond–Taylor의 설명입니다. Anthropic의 저장소는 (Galois 표현의 평탄 변형을 연구하기 위해) Fontaine 이론을 개발하고, Mazur의 Eisenstein 아이디얼에 대한 연구를 충분히 발전시켜 어떤 Frey 곡선도 p>=17인 점을 가질 수 없다는 결론을 내립니다. 이는 그들의 FLT 증명이 p>=17에 대해서만 작동한다는 것을 의미하지만, FLT는 이미 Best-Birkbeck-Brasca-Rodriguez에 의해 홀수 정칙 소수에 대해 형식화되었고, 가장 작은 비정칙 소수는 37이므로 모든 것이 괜찮습니다."

이 글을 읽는 수학자들에게 묻고 싶습니다: 위 내용이 당신에게 전혀 이해가 되나요?

이렇게 묻는 이유는 저는 컴퓨터 공학, 프로그래밍, 하드웨어 사양 등과 관련된 대부분의 기술 자료를 읽을 수 있기 때문입니다. 모든 세부 사항을 완전히 이해하지 못하더라도 꽤 잘 따라갈 수 있습니다. 그래서 전문 수학자들이 위의 내용을 보고 숙련된 소프트웨어 엔지니어가 컴퓨터 관련 내용을 이해하듯이 여전히 이해할 수 있는지 궁금합니다.

> 그 과정에서 1,300만 줄의 Lean 코드를 작성하고 29,500개의 중간 정리를 증명했습니다.

꽤 미친 짓이네요. 아마도 올바른 것으로 증명될 수 있는 모든 것은 모델이 할 수 있다는 생각에 더욱 힘을 실어주는 것 같습니다.

> 에이전트 팀이 2주도 안 되어 증명을 완료했으며, Claude Fable 5.1과 대략 비슷한 범용 내부 연구 모델에서 약 60억 개의 출력 토큰을 소비했습니다.

API 요금으로 출력 토큰 100만 개당 50달러를 적용하면, 이는 입력/프리필 토큰에 대한 약간의 비용을 더해 약 30만 달러의 비용이 들었을 것입니다.

주제와는 약간 다르지만, Simon Singh의 이 책을 강력히 추천합니다.

https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

1,300만 줄의 코드라면, Lean 증명 시스템의 잠재적인 문제를 악용하지 않았는지 확실합니까?

AI 도구가 확장됨에 따라 우리는 점점 더 이런 종류의 발표를 목격하게 될 것입니다. 에이전트 코딩이 아무리 인상적이라도 의학, 수학, 물리학 연구의 가치 제안에 비하면 비교할 수 없을 정도로 작습니다.

저는 AI의 노력 덕분에 제 평생에 전 세계적인 '만병통치약'의 도래를 목격하게 될 것이라고 낙관적으로 기대합니다. 비용 효율적인 대규모 유전 공학, 모든 질병의 치료제, 심지어 노화의 치료제까지.

미래는 아름답고도 무섭습니다.

좋아요, 이제 P = NP? 문제에 미친 듯한 에이전트 무리를 투입해 봅시다!

자동 증명 검증이 이렇게 유능하고 저렴해지면서, 수학계의 거의 모든 사람들이 참이라고 믿는 증명 중 얼마나 많은 증명이 거짓으로 판명될지 궁금합니다. 그리고 사소하고 고치기 쉬운 오류가 아니라 추론의 근본적인 결함으로 말이죠.