8P by chabulhwi 2달전 | favorite | 댓글 1개

페르마의 마지막 정리, 컴퓨터 언어로 새로 증명한다

페르마의 마지막 정리는 이미 증명되지 않았나?

이미 증명됐습니다. 영국의 수학자 앤드루 와일스가 1994년에 증명을 공개했고, 이 증명은 1995년에 공식적으로 출간됐습니다. 하지만 상호 작용 정리 증명기[ITP]의 언어로 작성된 형식 증명은 아직 없습니다.

상호 작용 정리 증명기? 형식 증명? 이게 뭐야?

  • 상호 작용 정리 증명기[ITP]: 사람이 형식 증명을 작성하도록 돕는 컴퓨터 프로그램. 증명 보조기[proof assistant]라고도 함.
  • 형식 증명: 증명 검증기[proof verifier]라는 컴퓨터 프로그램으로 검증할 수 있는 증명. 증명 보조기는 대개 증명 검증기 역할도 함.

정리 증명기는 인공 지능인가?

신경 정리 증명기[NTP]는 그렇다고 볼 수 있지만, 린을 비롯한 많은 상호 작용 정리 증명기는 기계 학습 기반의 프로그램이 아닙니다.

린(Lean) 정리 증명기를 소개해 줘.

페르마의 마지막 정리의 형식 증명은 왜 작성하려는 거야?

케빈 버저드 교수님이 X에 올린 포스트를 인용하자면, "컴퓨터로 하여금 현대 정수론을 이해시켜서, 결국에는 정수론자들을 도울 수 있게 하기 위함입니다."

링크

응원합니다. Formal proof에 관심이 있으신 분들은 Terrence Tao 교수님의 Machine Assisted Proofs (https://www.youtube.com/watch?v=AayZuuDDKP0) 강의 들어보시는 것도 추천드려요.