300년이 넘는 릴레이: 테렌스 테루(Terence Teru)에게서 영감을 받은 수학자들은 AI를 사용하여 페르마의 마지막 정리 증명을 공식화하기로 결정했습니다.

테렌스 타오(Terence Tao)에게서 영감을 받아 점점 더 많은 수학자들이 수학적 탐구를 위해 인공 지능을 사용하려고 시도하기 시작했습니다. 이번에 그들의 목표는 세계 10대 수학 문제 중 하나인 페르마의 마지막 정리입니다. 페르마의 마지막 정리는 지금까지 실현 가능한 해결책을 찾지 못한 매우 복잡한 수학적 문제입니다. 수학자들은 강력한 컴퓨팅 성능과 인공 지능의 지능형 알고리즘을 통해 수학을 탐색할 수 있기를 바랍니다

페르마의 마지막 정리(FLT)라고도 알려진 페르마의 마지막 정리는 17세기에 발명되었습니다. 프랑스인이 제안 수학자 피에르 드 페르마. 그 뒤에는 전설적인 이야기가 있습니다. 1637년경 페르마는 디오판투스의 산술의 라틴어 번역본을 읽고 있을 때, 11권 명제 8 옆에 다음과 같이 썼다고 합니다. 또는 일반적으로 두 번째보다 높은 거듭제곱을 동일한 거듭제곱의 두 거듭제곱의 합으로 나누는 것입니다. "나는 이것에 대해 뭔가를 발견했다고 확신합니다. 이것은 훌륭한 시연이지만 불행하게도. 여기 빈칸이 너무 작아서 적을 수 없습니다. ”

이 단락에 명시된 내용은 페르마의 마지막 정리의 내용입니다. 정수 n>2일 때 x^n + y^n=z^n에 대한 방정식에는 양의 정수 해가 없습니다

Fei. 마는 그것을 증명하는 방법을 알고 있다고 말했지만 책의 여백이 너무 작아서 쓰지 않았습니다. 나중에 이야기의 진위 여부와 페르마가 실제로 증명 방법을 알아냈는지에 대한 논란이 있었습니다. 300년 넘게 수학자들은 페르마의 마지막 정리를 증명하기 위해 열심히 노력해 왔습니다. 1995년이 되어서야 미국 프린스턴 대학교의 앤드류 와일즈 교수가 마침내 130페이지에 달하는 증명을 완성했습니다.

이제 페르마의 마지막 정리가 입증되었으니 수학자들이 AI로 또 무엇을 할 수 있을까요? 답은 바로 증명을 형식화하는 것입니다.

수학에서 형식화는 일반적으로 논리와 같은 엄격한 형식 언어를 사용합니다. 집합이론) 수학적 대상, 구조, 정리, 증명을 컴퓨터에서 표현, 검증, 연산할 수 있도록 표현함으로써 수학적 내용의 정확성과 일관성을 확보하는 것입니다. 수학의 발전은 19세기 후반으로 거슬러 올라갑니다. 20세기 초, 현대 형식수학은 20세기에 수리논리학과 컴퓨터과학의 발전과 함께 시작되었다. 형식 수학의 주요 목표는 일련의 기호, 일련의 기본 공리 및 일련의 추론 규칙을 포함하는 형식 시스템을 구축하는 것입니다. 작년 말 Tao Zhexuan과 다른 사람들은 Lean(대화형 정리 증명 및 프로그래밍 언어)을 사용하여 논문 중 하나를 공식화했습니다. 다항식 Freiman-Ruzsa 추측의 증명인 이 논문은 지난 11월 arXiv에 게시되었습니다. Lean 언어 코드를 작성할 때 Tao Zhexuan은 AI 프로그래밍 보조원 Copilot도 사용했습니다. 이 사건은 수학과 인공지능 커뮤니티에서 광범위한 관심을 끌었습니다.

당시 Lean 기술 오픈 소스 커뮤니티의 가장 중요한 발기인인 Imperial College London의 Kevin Buzzard는 다음과 같이 말했습니다. "기본적으로 무언가를 디지털화하면 새로운 방식으로 사용할 수 있다는 것은 명백합니다.

이 버자드 교수는 최근 페르마의 마지막 정리 증명을 공식화했다고 주장한 수학자인데, 그가 사용한 도구도 린이다.

이 일을 하게 된 배경과 동기, 구체적인 방법을 블로그에 소개했습니다.

페르마의 마지막 정리 증명을 공식화하는 이유는 무엇인가요?

페르마의 마지막 정리의 형식은 매우 간단하고 직관적이지만 이를 증명하는 것은 매우 어렵습니다. 이는 의심할 여지 없이 수학의 심오한 아름다움을 훌륭하게 보여주는 사례입니다. 지난 몇 세기 동안 수학자들은 이 문제를 해결하기 위해 암호학에서 물리학에 이르기까지 다양한 분야에 적용할 수 있는 수많은 수학 이론을 개발하고 혁신했습니다. 앤드류 와일즈(Andrew Wiles)는 FLT에서 영감을 받았을지 모르지만 실제로 그의 작업은 정수론, 대수기하학 및 축소군 표현 이론을 연결한 일련의 광범위한 수학 아이디어인 랭글랜즈 프로젝트(Langlands Project)에서 획기적인 발전을 이루었으며 앞으로도 계속될 것입니다. 2024년에도 많은 관심을 부탁드립니다.

역사적으로 대수적 정수론(수 필드의 인수분해 이론, 순환 필드의 산술 등)의 여러 다른 주요 혁신은 적어도 부분적으로는 FLT에 대한 더 깊은 이해에 대한 열망에서 비롯되었습니다.

Wiles의 작업은 그의 학생 Richard Taylor가 보완했으며, 20세기 수학의 방대한 기초를 바탕으로 구축되었습니다. Wiles가 도입한 기본 기술인 "모듈성 리프팅 정리"는 원본 논문이 출판된 이후 30년 동안 개념적으로 크게 단순화되고 널리 일반화되었습니다. 이 분야는 오늘날에도 여전히 매우 활발하게 활동하고 있습니다. 2022년 국제 수학자 회의에서 Frank Calegari가 발표한 논문으로 Wiles의 획기적인 발전 이후 진행 상황을 설명합니다(참조: https://arxiv.org/abs/2109.14145). Kevin Buzzard는 이 분야에서의 지속적인 활동이 FLT 증명을 공식화하려는 동기 중 하나라고 말했습니다.

수학의 형식화, 종이에 적힌 수학을 정리를 이해하고 개념을 증명할 수 있는 컴퓨터 프로그래밍 언어로 변환하는 기술입니다. ITP(대화형 정리 증명기)라고도 알려진 이러한 프로그래밍 언어는 수십 년 동안 사용되어 왔습니다. 그러나 최근 몇 년 동안 이 분야가 수학계에서 어느 정도 주목을 받은 것 같습니다. 우리는 수학 연구의 형식화에 대한 몇 가지 예를 목격했으며, 그 중 가장 최근의 것은 Terence Tao와 다른 사람들이 다항식 Freiman-Ruzsa 추측의 증명을 형식화한 것입니다. 이 2023년 획기적인 논문은 단 3주 만에 Lean에서 공식화되었습니다. 이러한 성공 사례를 통해 보는 사람들은 Lean과 같은 ITP가 이제 모든 현대 수학을 공식화할 준비가 되었다고 생각하게 될 수 있습니다.

그러나 진실은 그렇게 단순하지 않습니다. 조합론과 같은 수학의 일부 영역에서는 현대의 획기적인 발전이 실시간으로 공식화되는 것을 볼 수 있습니다. 그러나 Buzzard는 정기적으로 런던 정수론 세미나에 참석했으며 현대 수학적 정의에 대한 Lean의 지식이 세미나에서 발표된 결과를 공식화하기에는 충분하지 않으며 증명을 검증하는 것조차 불가능하다는 사실을 자주 발견했다고 말했습니다.

사실 이러한 측면에서 정수론의 "지연"은 Buzzard가 FLT의 현대 증명 형식화를 시작하게 된 주요 동기 중 하나였습니다. 프로젝트가 끝날 때까지 Lean은 자동형(복소 변수 함수의 특수 클래스) 및 표현, 갈루아 표현, 잠재 자동형, 모듈성 승격 정리, 대수 변종의 산술, 클래스 필드 이론, 산술 쌍대 정리를 이해할 수 있게 됩니다. , 시무라 품종 및 현대 대수 정수론에 사용되는 기타 개념. Buzzard의 견해에 따르면 이러한 기반이 마련되면 자신의 전문 분야에서 일어나는 일을 공식화하는 것은 더 이상 공상 과학 소설이 아닐 것입니다.

그럼 왜 이러는 걸까요? Buzzard는 "일부 컴퓨터 과학자의 말을 믿는다면 인공 지능의 기하급수적인 성장으로 인해 결국 컴퓨터가 수학자들의 연구를 도울 수 있게 될 것입니다. 이러한 작업은 현대 수학 연구에서 우리가 수행하는 작업을 컴퓨터가 이해하는 데 도움이 될 수 있습니다."라고 설명합니다. 프로젝트?

페르마의 마지막 정리 공식화 프로젝트가 시작되었습니다. Buzzard는 현재 진행 상황을 그래픽으로 보여줍니다.

관심 있는 연구자는 자세한 내용을 읽을 수 있습니다: https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_document.html

이 프로젝트는 EPSRC의 자금 지원을 받으며 Buzzard는 처음 5년 동안 자금 지원을 받게 됩니다. 이 기간 동안 그의 첫 번째 목표는 FLT를 1980년대 후반 수학자에게 알려진 진술로 줄이는 것이었습니다.

물론 버자드가 혼자서 이 일을 할 생각은 없었습니다. 그는 주장의 일부 부분에 대해서는 기본 원리를 이해했지만 세부 사항을 자세히 검토한 적이 없다고 말했다. 또한 Project Langlands는 GL_2의 순환 기반 변환 및 Jacquet-Langlands를 포함하여 몇 가지 중요한 사항도 도입했습니다. 이 심오한 것들에 대한 그의 이해는 충분히 깊지 않습니다.

그러나 이것이 바로 정식 프로젝트의 장점입니다. Buzzard는 Lean에서 필요한 결과를 명확하게 표현하고 이를 다른 사람들에게 전달할 수 있습니다. 이 시스템의 장점은 기여하기 위해 FLT의 전체 증거를 이해할 필요가 없다는 것입니다. 위의 다이어그램은 증명을 여러 개의 작은 기본정리로 나누어 크라우드소싱에 매우 편리하게 만듭니다. 이러한 기본정리 중 하나라도 공식적으로 증명할 수 있다면 Buzzard는 귀하의 끌어오기 요청을 간절히 기다릴 것입니다.

프로젝트에 참여하고 싶은 분들은 Lean에 대해 좀 알아야 합니다. 이를 위해 Buzzard는 Mathematics in Lean 온라인 교과서를 추천합니다.

교과서 링크: https://leanprover-community.github.io/mathematics_in_lean/

이 프로젝트는 수학자 및 컴퓨터 과학자를 위한 강력한 연구 포럼인 Lean Zulip 채팅의 FLT 스트림에서 진행됩니다. 실시간으로 코드와 수학을 쉽게 게시하고 스레딩 및 스트림 시스템을 사용하여 동시에 여러 개의 독립적인 대화를 효과적으로 지원합니다.

Lean Zulip 채팅 링크: https://leanprover.zulipchat.com/

Buzzard는 프로젝트가 얼마나 오래 걸릴지 전혀 모르지만 확실히 낙관적이라고 말했습니다.

동시에 Lean과 같은 공식 증명 도구도 지속적으로 반복되고 있습니다. 원래 Lean과 비교하여 최신 Lean 4 버전은 더 빠른 컴파일러, 향상된 오류 처리, 외부 도구와의 더 나은 통합을 포함하여 많은 최적화가 이루어졌습니다.

지난해 말 오픈 플랫폼 LeanDojo 팀과 Caltech의 연구진은 대규모 언어 모델이 인간과 상호 작용할 수 있도록 설계된 협업 도구인 Lean Copilot을 출시하여 대규모 AI 모델의 힘을 수학 연구에 주입했습니다.

"올바르게 사용된다면 AI는 2026년까지 수학 연구 및 기타 여러 분야에서 신뢰할 수 있는 공동 저자가 될 것이라고 예측합니다." Terence Tao는 이전 블로그에서 말했습니다.

테렌스 타오의 예측이 하루빨리 이루어졌으면 좋겠습니다.

관련 읽기:

• 《테렌스 타오의 AI를 활용한 형식 증명은 무엇인가요? 하나의 기사로 PFR 추측의 과거와 현재를 이해하세요》

• 《Tao Zhexuan이 선호하는 증명 보조자 Lean, 대형 모델을 사용합니다》

• 《대형 모델은 Tao Zhexuan이 문제를 해결하고 수학 정리를 증명하는 데 도움이 됩니다. 수학이 정말 중요해요. AI의 도움으로 돌파구를 찾는 첫 번째 학문이 되었나요? 》

• 《Tao Zhexuan의 새 프로젝트: Lean에서 소수 정리 증명, 연구 청사진 준비됨》

^{참조 링크: https://leanprover.zulipchat.com/#narrow/ 스트림 /416277-FLT}

^{https://mp.weixin.qq.com/s/d9RSkRhlKH5ZMek3yTqe4Q}

위 내용은 300년이 넘는 릴레이: 테렌스 테루(Terence Teru)에게서 영감을 받은 수학자들은 AI를 사용하여 페르마의 마지막 정리 증명을 공식화하기로 결정했습니다.의 상세 내용입니다. 자세한 내용은 PHP 중국어 웹사이트의 기타 관련 기사를 참조하세요!