AI는 페르마의 마지막 정리를 정복할 수 있을까? 100페이지의 증거를 코드로 만들기 위해 5년의 경력을 포기한 수학자
- WBOY앞으로
- 2024-04-09 15:20:02719검색
페르마의 마지막 정리가 AI에 의해 정복될 예정이라고요?
그리고 전체에서 가장 의미 있는 부분은 AI가 풀려고 하는 페르마의 마지막 정리가 바로 AI가 쓸모없다는 것을 증명하는 것이라는 점입니다.
옛날에는 수학이 순수한 인간 지능의 영역에 속했지만 지금은 이 영역이 고급 알고리즘에 의해 해독되고 짓밟히고 있습니다.
Pictures
페르마의 마지막 정리는 수세기 동안 수학자들을 당황하게 만든 "악명 높은" 퍼즐입니다.
1993년에 입증되었으며 이제 수학자들은 컴퓨터를 사용하여 증명 과정을 재현하겠다는 훌륭한 계획을 세웠습니다.
이 버전의 증명에서는 논리적 오류가 있으면 컴퓨터로 확인할 수 있기를 바랍니다.
프로젝트 주소: https://github.com/riccardobrasca/flt3
3월 말, 수학자 Pietro Monticone은 그와 그의 동료들이 LeanProver 형식화에서 지수 3을 사용하여 Fermat를 거의 완성했다고 신나게 말했습니다. 마지막 정리.
FLT 프로젝트에서 사용할 수 있도록 가능한 한 빨리 공식 프로세스를 Mathlib로 포팅할 것입니다.
Pictures
증명 과정은 대략 Wiles의 증명을 따르지만 약간의 변경이 있습니다.
Lean을 사용하여 Fermat의 마지막 정리를 코드로 전환
4월이 오면 수학자이자 프로그래머인 Kevin Buzzard는 컴퓨터 코드를 통해 Fermat의 마지막 정리 증명을 완성하겠다는 계획을 발표합니다.
4월에 프로젝트가 온라인에 공개되면 공개 청사진이 온라인에 표시됩니다. 이때 Lean 커뮤니티의 누구나 공식 증명에 기여할 수 있습니다.
Pictures
획기적인 100페이지 분량의 수학 증명을 컴퓨터 코드로 변환하는 과정이 구현하기 쉽나요?
이는 물론 테렌스 타오(Terence Tao)가 높은 평가를 받고 즐겨 사용하는 증명 도구인 Lean 덕분입니다. 이 도구를 사용하면 산문 스타일의 증명을 테스트용 규칙과 논리로 변환할 수 있습니다.
사진
그러나 이 프로젝트는 간단하지 않고 수년이 걸릴 것으로 예상되며, 케빈 버자드 페이지는 해당 프로젝트에 대한 재정적 지원을 받았습니다.
Pictures
모두가 이 프로젝트가 아마도 지금까지 가장 복잡한 컴퓨터 시연 중 하나라는 것을 알고 있습니다.
Pictures
페르마의 마지막 정리
페르마의 마지막 정리는 역사상 가장 흥미로운 수학 퍼즐입니다.
페르마의 마지막 정리를 증명하는 과정은 바로 수학의 역사입니다.
Pictures
익숙한 페르마의 마지막 정리는 17세기 프랑스 수학자 피에르 드 페르마가 제안했습니다. 불행히도 그는 평생 동안 증거를 찾지 못했습니다.
그래서 300여년 전에 시작된 이 문제는 300년 동안 인류에게 직접적으로 도전했고, 세계를 여러 번 충격에 빠뜨리고, 인류의 가장 뛰어난 두뇌의 에너지를 소진시켰으며, 수천 명의 아마추어를 매료시켰습니다.
Picture
이 정리는 방정식 (a^n + b^n = c^n)을 만족하는 세 개의 양의 정수 a, b, c가 없다고 주장합니다. 여기서 n은 다음보다 큰 정수입니다. 2 .
이 증명의 어려움은 수학자들이 부정적인 경우를 찾는 것이 어렵다는 것입니다. 이 방정식을 만족할 수 있는 무한한 정수 n이 없다고 어떻게 보장할 수 있습니까?
Pictures
다행히 오늘날의 수학자에게 무한의 개념을 논리로 변환하는 것은 새로운 것이 아닙니다.
간단한 증명에서는 귀납법에 의존할 수 있습니다. -
일단 특정 숫자(예: 8)에 대해 특정 논리가 참이면 이후의 모든 숫자(예: 9, 10)에도 해당됩니다. , 11 등)은 무한대까지 동일하게 참입니다.
Pictures
그러나 페르마의 마지막 정리는 수백 년 동안 수학계에서 걸림돌이었습니다.
1993년이 되어서야 영국의 수학자 Andrew Wiles가 100페이지 분량의 증명으로 이 미스터리를 풀었습니다.
Pictures
왜 컴퓨터는 페르마의 마지막 정리를 증명할 수 없나요? 산업은 세 가지 이유가 있다고 믿는다 덧없는 실수가 나타난다
다행히 Lean 보조 증명이 있습니다
100페이지 분량의 수학 증명은 일반 수학 학생이나 수학자에게는 관리하기가 그리 쉽지 않습니다.
다행히도 우리는 더 이상 전통적인 증명 방법에 의존하지 않고 Lean과 같은 도구를 사용할 수 있습니다. C++ 기반으로 개발된 프로그래밍 도구로 유도 증명 작성 및 검증을 위해 특별히 설계되었습니다.
오늘날의 소위 '인공지능'의 대부분은 인간의 언어를 모방하여 교묘하게 배열된 단어에 지나지 않습니다. 그러나 Lean과 같은 컴퓨터 지원 증명은 인간의 사고와 컴퓨터 지원 향상된 기능을 더욱 깊이 통합합니다.
Pictures
학부 강의에 도입되는 린 프로그래밍 도구
Imperial College London에서 수학을 가르치는 Kevin Buzzard는 린 도구를 사용하여 대학의 전체 학부 수학 과정에 대한 지원을 개발하는 데 수년을 보냈습니다.
이러한 도구를 통해 학생들은 수업 중 토론한 내용을 논리적 및 수학적 연산의 단계로 나눌 수 있습니다.
이것은 마치 수학 증명의 로제타스톤과 같습니다.
수학 교사이기도 한 Clarissa Littler는 Kevin Buzzard의 철학에 크게 동의합니다.
그녀는 포틀랜드 커뮤니티 칼리지에서 이산 수학을 가르치고 있습니다. 지난 두 학기 동안 그녀는 이산 수학 수업에서 Kevin Buzzard가 개발한 "Lean Classic 입문 게임"을 사용했습니다.
Pictures
주소: https://adam.math.hhu.de/
학생들이 수학적 귀납법에 익숙해지도록 돕기 위해 "자연수 게임"을 사용하고, "집합론 게임"을 통해 집합에 대한 추론에 익숙해지도록 할 것입니다.
그림
이 과정에서 "논리적 규칙을 엄격히 준수하여 증명을 작성하는 것"과 "사물의 진실을 설명하기 위해 대중적인 언어를 사용하는 것" 사이의 학생들의 이해 격차가 점차 메워질 것입니다.
Littler는 이 과정의 주요 초점은 수학에 대한 기초가 약한 학생들이 수학자의 방식으로 더 자유롭게 생각할 수 있도록 하는 동시에 증명, 증거 및 진실을 보여주는 방법을 더 잘 이해할 수 있도록 하는 것이라고 강조했습니다.
공식 논리에서 규칙 목록, 산문 표현으로의 전환은 프로젝트를 협력적인 코드 조각으로 나누는 데 핵심입니다.
Pictures
그리고 이는 프로그래밍과 순수 수학의 교차점에서 특히 중요하며, 이것이 바로 Lean과 같은 도구가 빛을 발할 수 있는 부분입니다.
Buzzard는 페르마의 마지막 정리에서 촉발된 복잡한 수학적 아이디어를 프로그래밍 가능한 형태로 변환하고 싶다고 말했습니다.
이 정리를 증명하기 위해 수세기에 걸쳐 수학의 가치 있는 새로운 분야가 많이 만들어졌는데, Buzzard의 의견으로는 이 정리는 "실질적인 의미가 없습니다".
예, Buzzard의 관점에서 Fermat의 마지막 정리는 의미가 없으며 현실 세계에 적용할 수 없습니다. 그러나 이 "악명 높은" 문제로 인해 최근 몇 년 동안 수많은 훌륭한 새로운 아이디어가 탄생했습니다.
이제 Wiles의 100페이지 분량의 증명을 컴퓨터가 이해할 수 있는 공식 언어와 규칙으로 변환하면 새로운 세대의 수학자에게 컴퓨터를 이용한 증명의 문이 열릴 것으로 예상됩니다.
Pictures
그리고 이 변환 도구는 프로그래머에게도 도움이 될 수 있습니다.
Littler는 이 분야에서 야심찬 프로젝트는 우리 모두가 배운 교훈과 작성된 라이브러리로부터 이익을 얻을 수 있기 때문에 항상 시도해 볼 가치가 있다고 말했습니다.
대화형 정리 증명은 아직 비교적 새로운 분야이지만 Lean 커뮤니티는 훌륭한 작업을 많이 해왔습니다.
Kevin Buzzard: 린(Lean) 전도사
Kevin Mark Buzzard는 1968년에 태어나 산술 기하학과 Langlands 프로그램 분야에서 전문적 지식이 풍부합니다.
현재 Imperial College London의 순수수학 교수이자 AI 도구 Lean의 '전도자'입니다.
Kevin Buzzard는 Royal Grammar School에서 공부하는 동안 국제 수학 올림피아드에 참가하여 1986년 동메달, 1987년 만점으로 금메달을 획득했습니다.
Pictures
그 후 그는 케임브리지 대학교 트리니티 칼리지에서 수학 학사 과정을 마쳤고 1990년에 수석 랭글러라는 칭호를 받았으며 1991년에 C.A.S.M 학위를 받았습니다.
Richard Taylor의 지도 하에 수학의 복잡한 분야를 탐구하는 그의 박사 학위 논문 "모듈형 표현의 수준"이 1995년에 완성되었습니다.
Pictures
1998년 Imperial College London에서 강사로 일하기 시작했고, 2002년 수석 강사로 승진했으며, 2004년 교수로 임명되었습니다.
그는 또한 하버드 대학교(2002년 10월부터 12월까지)와 몇몇 유명 기관에서 방문 연구를 수행했습니다.
정수론 분야에서 뛰어난 공헌으로 2002년 화이트헤드상, 2008년 시니어 버윅상을 수상했습니다.
2017년 Buzzard는 수학 연구에서 컴퓨터 지원 증명 도구의 사용을 홍보하는 데 전념하는 Lean Theorem Prover에 관한 프로젝트와 블로그를 시작했습니다.
그는 또한 음악가 Dan Snaith(예명 Caribou)를 지도하여 초수렴 Siegel 모듈 기호 연구에 대한 수학 박사 학위 논문을 완성했으며, Snaith는 Imperial College London에서 박사 학위를 받았습니다.
2023년 10월 Kevin Buzzard는 소셜 미디어에서 연구 자금을 받았으며 Lean을 사용하여 Fermat의 마지막 정리를 증명하기 시작했다고 밝혔습니다.
Pictures
버자드는 "10년 전에는 이 작업에 무한한 시간이 걸렸을 것"이라고 말했습니다. 그는 프로젝트를 완료하기 위해 5년 동안 교육 업무를 보류할 예정입니다.
자신의 작업을 보류할 가치가 있나요?
영국 노팅엄 대학교의 동료인 Chris Williams는 이런 종류의 프로젝트가 예상치 못한 이점과 광범위한 영향을 미칠 수 있다고 생각합니다.
"그가 향후 5년 이내에 전체 증명을 공식적으로 공식화할 가능성은 거의 없다고 생각합니다. 그렇지 않으면 정말 놀라운 일이 될 것입니다. 그러나 이제 많은 도구가 정수론과 산술 기하학에 편재되어 있으므로 미래에 실질적인 진행은 매우 유용할 것입니다."
수학 연구에 중요합니다
이 프로젝트는 또한 더 깊은 가치를 드러냅니다.
컴퓨팅 도구가 지속적으로 발전함에 따라 수학의 다양한 분야 간, 심지어 학문 분야 간의 경계가 점점 흐려지고 있으며 이로 인해 검증이 거의 불가능한 몇 가지 증명이 등장하게 되었습니다.
예를 들어, 교토 대학의 일본 수학자 모치즈키 신이치는 너무 복잡하고 부분적으로는 사람들이 어떻게 해야 할지 몰랐기 때문에 출판하는 데 몇 년이 걸린 500페이지 분량의 증명을 썼습니다.
이제부터 우리는 수학의 경계가 점점 더 흐려지는 것을 발견할 수 있습니다.
이것은 진실성이나 논리적 모호성을 의미하는 것이 아니라 증명에 포함될 수 있는 다양한 아이디어의 범위를 의미합니다.
Lean을 사용하면 수학자들은 자신의 아이디어를 코드로 변환하여 동료들이 더 쉽게 이해할 수 있습니다. 선배들이 기록한 선례를 살펴보면 미래의 수학자들은 이를 바탕으로 계속해서 자신의 연구를 발전시킬 수 있습니다.
Buzzard는 Lean에서 수학적 글쓰기의 특징은 정확하게 명시되어 있지만 입증되지 않은 결과를 남길 수 있고 나중에 다른 사람들이 해결할 수 있다는 것이라고 말했습니다.
Lean 자체가 이러한 작업 흐름을 촉진합니다.
사진
즉, Fermat의 마지막 정리는 "크라우드소싱"으로 해결될 준비를 하고 있다는 것입니다. 특히 코딩 작업이 Buzzard의 남은 근무 기간을 초과하는 경우에는 더욱 그렇습니다.
수학적 증명을 완성하려면 커뮤니티 전체의 노력이 필요합니다.
아마 미래에는 수학적 증명을 공유하고 해석하는 Genius.com과 유사한 플랫폼을 가질 수 있을 것입니다.
참고자료:
위 내용은 AI는 페르마의 마지막 정리를 정복할 수 있을까? 100페이지의 증거를 코드로 만들기 위해 5년의 경력을 포기한 수학자의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!