350년 난제 '페르마의 마지막 정리' 컴퓨터 증명 나선 수학자들
(dongascience.com)페르마의 마지막 정리, 컴퓨터 언어로 새로 증명한다
- 임피리얼 칼리지 런던의 케빈 버저드(Kevin Buzzard) 교수님이 2024년 10월부터 페르마의 마지막 정리(FLT)의 형식 증명을 린(Lean) 정리 증명기로 작성할 예정입니다.
- 영국의 공학 및 물리 과학 연구 회의[EPSRC]에서 버저드 교수님에게 연구비를 그달부터 5년 동안 지원하기로 했습니다.
- 린 블루프린트(Lean blueprints)라는 plasTeX 플러그인을 이용해 만든 프로젝트 계획서가 2024년 4월 말에 공개될 예정입니다.
페르마의 마지막 정리는 이미 증명되지 않았나?
이미 증명됐습니다. 영국의 수학자 앤드루 와일스가 1994년에 증명을 공개했고, 이 증명은 1995년에 공식적으로 출간됐습니다. 하지만 상호 작용 정리 증명기[ITP]의 언어로 작성된 형식 증명은 아직 없습니다.
상호 작용 정리 증명기? 형식 증명? 이게 뭐야?
- 상호 작용 정리 증명기[ITP]: 사람이 형식 증명을 작성하도록 돕는 컴퓨터 프로그램. 증명 보조기[proof assistant]라고도 함.
- 형식 증명: 증명 검증기[proof verifier]라는 컴퓨터 프로그램으로 검증할 수 있는 증명. 증명 보조기는 대개 증명 검증기 역할도 함.
정리 증명기는 인공 지능인가?
신경 정리 증명기[NTP]는 그렇다고 볼 수 있지만, 린을 비롯한 많은 상호 작용 정리 증명기는 기계 학습 기반의 프로그램이 아닙니다.
린(Lean) 정리 증명기를 소개해 줘.
- 상호 작용 정리 증명기 겸 순수 함수형 프로그래밍 언어.
- 의존 유형론에 기반을 둠.
- 유형 클래스, 확장 가능한 구문, 매크로, 메타프로그래밍 등의 기능이 있음.
- 다른 증명 보조기와 비교할 때, 린의 이용자층에는 (수학 기초론 밖의 분야를 연구하는) 수학자가 특히 많음.
페르마의 마지막 정리의 형식 증명은 왜 작성하려는 거야?
케빈 버저드 교수님이 X에 올린 포스트를 인용하자면, "컴퓨터로 하여금 현대 정수론을 이해시켜서, 결국에는 정수론자들을 도울 수 있게 하기 위함입니다."
링크
- 2023년 10월 3일에 케빈 버저드 교수님이 린 줄립(Zulip) 챗에 올린 메시지: https://leanprover.zulipchat.com//…
- 린 수학 라이브러리: https://github.com/leanprover-community/mathlib4
- 뉴사이언티스트 기사: https://institutions.newscientist.com/article/…
- 파퓰러메카닉스 기사: https://popularmechanics.com/science/math/…
응원합니다. Formal proof에 관심이 있으신 분들은 Terrence Tao 교수님의 Machine Assisted Proofs (https://www.youtube.com/watch?v=AayZuuDDKP0) 강의 들어보시는 것도 추천드려요.