제퍼넷 로고

컴퓨터는 수학자가 될 수 있습니까?

시간

인공 지능에게 수학을 어떻게 가르칩니까? AI는 이미 체스와 바둑과 같은 게임을 포함한 문제 해결 작업에서 인간을 능가했습니다. 그러나 기계가 어떤 작업을 처리하기 전에 컴퓨터가 이해할 수 있는 언어로 지시로 재해석되어야 합니다. 지난 몇 년 동안 전 세계의 연구원과 아마추어는 수학의 필수 공리를 린(Lean)이라는 프로그래밍 언어로 번역하기 위해 협력했습니다. 이 지식을 바탕으로 린을 이해하는 정리 증명 프로그램이 시작되었습니다. 세계 최고의 수학자들을 돕다 그들의 작업을 확인합니다. 스티븐 스트로가츠가 이야기하는 케빈 버자드, 임페리얼 칼리지 런던(Imperial College London)의 순수 수학 교수는 린에게 수학을 “가르치”려는 노력과 이와 같은 프로젝트가 수학의 미래를 어떻게 형성할 수 있는지에 대해 설명합니다.

들어 봐 Apple Podcasts, 스포티 파이, Google 포드 캐스트, 스티, TuneIn 또는 좋아하는 팟캐스트 앱, 또는 스트리밍 콴타.

성적 증명서

스티븐 스트로 가츠 (00:02): 저는 Steve Strogatz입니다. 이유의 기쁨, 팟캐스트 Quanta Magazine 그것은 오늘날 과학과 수학에서 가장 큰 답이 없는 질문으로 안내합니다. 이 에피소드에서 우리는 수학에서 컴퓨터의 미래에 대해 이야기할 것입니다.

(00:19) 컴퓨터는 얼마나 많은 수학을 할 수 있습니까? 그리고 컴퓨터가 최고의 인간 수학자보다 더 잘할 수 있을까요? 말이 터무니없게 들린다면 얼마 전에 체스에서 무슨 일이 일어났는지 기억하십시오. 세계 최고의 인간 체스 플레이어를 이긴 IBM 컴퓨터 Deep Blue에 대해 들어보셨을 것입니다. 게리 카스파로프, 1997년으로 거슬러 올라갑니다. Deep Blue는 물론 컴퓨터이기 때문에 매우 빨랐습니다. 초당 200억 개의 체스 위치를 평가할 수 있습니다. 그리고 그 위치에 대한 평가는 프로그래머가 구축한 거대한 체스 지식 라이브러리를 기반으로 했습니다.

(01:01) 이제 비슷한 방식으로 작지만 성장하는 수학자 커뮤니티가 린이라는 프로그래밍 언어. 그들은 Lean이 참조할 수 있는 수학 지식 라이브러리를 구축하고 있습니다. 인간 수학자들이 증명을 확인할 수 있도록 도와주세요.. 대수, 기하학 및 논리에 대한 지식으로 무장한 증명 보조자로 알려진 이 프로그램은 사람들을 위해 바쁜 작업을 수행하고 작업을 엄격하게 확인합니다. 이것은 수학자들이 더 창의적으로 일할 수 있는 시간과 정신적 공간을 확보합니다. 최근에 Lean은 다음 중 하나를 도왔습니다. 세계 최고의 수학자, 피터 숄츠, 그가 작업하고 있던 복잡한 증거의 정확성을 확인합니다. 그 뒤에는 흥미진진한 이야기가 있습니다. 우리가 그것을 알게 될 것입니다. 그러나 그것은 이 소프트웨어에 대한 일종의 큰 홍보 승리였습니다. 따라서 문제는 컴퓨터가 현재와 미래에 순수 수학을 위해 무엇을 할 수 있느냐는 것입니다. 그들은 단순한 증명 조수에서 진정한 증명 제작자로 이동할 수 있습니까? 그렇다면 나와 내 손님과 같은 수학자들이 실직하게 될까요? 단순히 계산된 것이 아니라 생각에서 벗어난 것입니까? 그래서 지금 저와 합류하게 된 사람은 Imperial College London의 순수 수학 교수인 Kevin Buzzard입니다. 환영합니다, 케빈.

케빈 버자드 (02:16): 안녕하세요. 함께 해주셔서 감사합니다.

스트로가츠 (02:18): 음, 여기 와주셔서 정말 감사합니다. 이것은 정말 매력적인 주제입니다. 그리고 그것에 대해 이야기하게 되어 기쁩니다. 그렇다면 린(Lean)이 무엇인지부터 시작해 볼까요? 그것이 무엇인지 요약해 주시겠습니까? 처음에 왜 만들어졌을까요?

독수리 (02:32): Microsoft가 처음에 Lean을 쓴 이유를 모르겠습니다. 솔직히 말해서, 수학의 규칙을 알고 있고, 당신의 말을 주의 깊게 듣고 정확하지 않은 것은 무엇이든 찾아냅니다. . 재미있는 방식으로 학습할 수 있습니다. 그리고 그것은 당신이 말한 것을 확인할 수 있습니다. 수학에 대해 이야기하고 이해할 수 있습니다. 그리고 그것이 바로 우리가 지금 있는 곳입니다.

(03:00) 그래서, 지금은 일종의 학부생 같습니다. 나는 그것을 학부생처럼 취급합니다. 그리고 저는 학부 시절 이야기를 합니다. 그리고 내가 충분히 정확하지 않을 때 그것은 소란을 일으킨다. 그러나 그것은 컴퓨터 증거 검사기입니다. 그래서 우리는 수학적 증명을 입력할 수 있고 그것을 통과할 것입니다. 그리고 마지막에 그것을 믿는다면 "네, 알겠습니다. 알겠습니다."라고 말할 것입니다. 그러나 그들을 믿는다는 것은 무엇을 의미합니까? 린의 경우, 그것은 당신이 말한 것을 취했고, 그것들을 수학의 가장 기본적인 공리까지 번역하고 모든 것이 확인되는지 확인했다는 것을 의미합니다.

스트로가츠 (03:38): 당신과 함께 조금 더 탐구하고 싶습니다. 하지만 — 당신은 마이크로소프트가 왜 그것을 개발했는지 전혀 모른다고 말하지만, 아마도 당신이 아는 한 최소한 무슨 일이 일어났는지에 대한 역사를 우리에게 알려줘야 할 것입니다.

독수리 (03:47): 따라서 정리 증명자는 1960년대, 1970년대부터 존재해 왔습니다. 그리고 제 인상은, 제 말은, 저는 컴퓨터 과학자가 아닙니다. 하지만 제 인상은 이 두 가지 아이디어를 염두에 두고 설계되었다는 것입니다. 첫째, 수학적 증명이 올바른지 확인합니다. 그리고 실제로, 초기 정리 증명자들은 ... XNUMX의 제곱근의 비합리성과 같은 것에 대한 많은 증거를 봅니다. 그러나 또한 그들은 활에 또 다른 줄이 있습니다. 그들은 또한 컴퓨터 코드에 버그가 없는지 확인할 수 있습니다. 소프트웨어에 버그가 없는지 확인하는 것은 정말 강력한 애플리케이션처럼 들립니다. 따라서 Microsoft와 같은 회사의 경우 이것이 염두에 둔 것 중 하나라고 생각합니다.

(04:35) 하지만 제 느낌은 이 프로젝트가 시작된 2014년에 레오 드 무라 그는 논리 문제를 매우 빠르게 해결하는 논리 문제를 해결하는 더 간단한 종류의 퍼즐 해결사를 설계했습니다. 그리고 그는 이것으로 상을 받았습니다. 그리고 그는 Microsoft Research에서 일하고 있습니다. Microsoft Research는 Microsoft의 푸른 하늘을 생각하는 날개입니다. 그리고 어쩐지 정리 증명자를 쓸 생각이 떠올랐고, 그는 관심을 갖고 앉아서 그것을 썼다. 그리고 나는 그들이 어디로 가고 있는지 생각하고 있었는지 정말로 모릅니다. 그러나 2015년에는 프로토타입이 있었고 2017년에는 꽤 잘 작동하는 무언가가 있었습니다.

(05:17) 그리고 그 이야기 때문에 부딪쳤습니다. 톰 헤일즈 케임브리지의 뉴턴 연구소에서 발표했습니다. Tom Hales는 수학이 어디로 가고 있는지에 대해 매우 추측적인 이야기를 했으며 정리 증명자가 그 일부일 수 있다고 제안했습니다. 그리고 그는 수학 정리의 데이터베이스를 구축할 것을 제안했습니다. 수학 정리의 진술일 뿐이며 모든 것이 정리 증명자에 정확하고 정확하게 기술되어 있습니다. 그는 이 데이터베이스가 수학자에게 유용할 것이라고 생각했기 때문입니다. 따라서 데이터베이스는 모든 정리에 대한 증명을 포함하지 않을 것입니다. 왜냐하면 그것은 어떻게든 상상할 수 없기 때문입니다. 따라잡기가 매우 어려울 것입니다. 아시다시피, 수학은 2,000년 동안 발전해 왔습니다.

(06:05) 그리고 마지막 질문에서 누군가가 그에게 어떤 시스템을 사용할 것인지 물었고 그는 Lean이라고 말했습니다. 저는 이 소프트웨어에 대해 들어본 적이 없지만, 이제 인터넷이 생겼습니다. 그래서 검색을 해보니 Lean이 상대적으로 새롭고 수학이 거의 없다는 것을 알게 되었습니다. 그리고 소프트웨어를 실험해 볼 가치가 있다고 생각했습니다. 그러나 몇 가지 기술적인 이유로 Lean은 다른 정리 증명자보다 우위에 있습니다. 쓸 수 있기 때문입니다. 제 말은, 이것은 약간 기술적인 것이지만 인간은 공리적인 수준에서 컴퓨터와 대화하기를 원하지 않습니다. 그렇죠? 인간은 인간과 대화하는 것과 같은 방식으로 컴퓨터와 대화하고 싶어합니다. "오, 이제 이것을 곱하고 귀납법을 사용하면 끝입니다."라고 말할 것입니다. 그리고 그런 종류의 스케치 증명에서 공리까지 가려면 무슨 일이 일어나고 있는지 해석하고 수학의 기본적인 공리로 모든 것을 번역하려고 하는 백그라운드에서 실행되는 무언가가 있어야 합니다. 그래서 이러한 것들을 전술이라고 합니다. 그리고 한 가지, 린의 흥미로운 속성 중 하나는 린의 프로그래밍 언어로 린 전술을 작성한다는 것입니다. 그래서 수학을 할 수 있고, 이 수학을 공리로 변환하는 알고리즘을 작성할 수도 있는 일종의 만능인 것입니다. 모두 같은 시스템에서 말이죠. 다른 정리 증명자보다 수학에 관해서는 린에게 약간의 우위가 있습니다.

스트로가츠 (07:28): 이것은 흥미로운 일입니다. 그래서 전술의 아이디어는 컴퓨터 과학 박사가 아닌 사람들이나 컴퓨터 종류의 사람들이 수학자들이 편한 자연어로 말하는 것이 더 편안하다고 말씀하셨습니다. . 그러나 어떻게든 번역할 수 있습니다.

독수리 (07:48): 네, 공리로 내려가야 합니다. 맞죠? 즉, 이것이 바로 이 게임입니다. 하루가 끝나면 Lean은 수학의 공리를 알기 시작합니다. 이는 극도로 원시적인 진술입니다. 그리고 사실, 여러분은 대부분의 수학자에게 물어봅니다. 그들은 수학의 공리가 무엇인지 말할 수 없을 것입니다.

스트로가츠 (08:03): 네. 무슨 말인지 상기시켜 주시고 한두 가지 예를 들어 주시겠습니까?

독수리 (08:08): 뭐, 집합론의 공리 중 하나는 "집합이 존재한다"는 것입니다. 그리고 또 다른 공리 중 하나는 "두 집합이 동일한 요소를 가지고 있으면 동일합니다."입니다. 그래서 이것들은 이런 종류의 것입니다. 또는 "두 집합의 합집합은 집합입니다." 이런 종류의 것입니다. 따라서 다음을 확인해야 합니다.x + y), 모든 제곱은 x2 + 2xy + y2. 우리는 괄호를 확장하고 싶습니다. 수학의 공리에서 그렇게 하려고 하면 약 20줄이 걸립니다. 어떤 학교 아이도 당신에게 이렇게 말할 수 있습니다(x + y)2 is x2 + 2xy + y2. 우리는 원합니다. 한 번의 움직임이 필요하고, 20번의 움직임이 될 수 없습니다. 그렇지 않으면 전체가 중단될 것입니다. 따라서 전술은 논리의 기본 단계 외에는 아무 것도 할 수 없는 경직된 기계가 아니라 똑똑한 학부생과 의사 소통하는 것처럼 만드는 데 사용할 수 있는 더 강력하고 강력한 주장입니다.

스트로가츠 (09:06): 저는 사실 그 단어 자체를 좋아합니다. 왜냐하면 전술은 우리가 게임에 대해 생각하고 있다는 것을 암시하기 때문입니다. 특히 체스가 생각납니다. 내 말은, 당신은 움직임과 전술을 계속 언급하고 있습니다. 그리고 그것들은 물론 우리가 체스에서 사용하는 단어입니다.

독수리 (09:20): 수학에 대한 나의 현재 이해는 수학이 거대한 퍼즐 게임이라는 것입니다. 그리고 사실, 정말 빨리 내가 ​​가장 좋아하는 퍼즐 게임이 되었습니다. 나는 여가 시간에 컴퓨터 게임을 하곤 했다. 나는 컴퓨터 게임의 퍼즐을 좋아한다. 예를 들어, 저는 아주 교활한 퍼즐이 많이 있는 Zelda 프랜차이즈를 좋아합니다. 하지만 싸움도 있다. 또한 빠른 움직임과 빠른 반응 시간을 요구하는 것들도 있습니다. 그리고 나이가 들수록 이야기의 이러한 부분이 덜 재미있다는 것을 알게 됩니다. 아시다시피 제 반응 속도가 느려지기 때문입니다. 그리고 적과의 전투가 다소 지루하다고 생각합니다. 반면에 나는 문제를 해결하는 것이 매우 흥미롭습니다. 그리고 제가 2017년에 Lean을 사용하기 시작했을 때 발견한 것은 사실 다른 모든 컴퓨터 게임을 하지 않는다는 것이었습니다. 린은 수학을 퍼즐 게임으로 바꿉니다. 내 말은, 이 모든 정리 증명자들이 그렇습니다. 모든 정리 증명자는 수학을 퍼즐 게임으로 바꿉니다. 그리고 수학 정리는 그 퍼즐 게임의 수준입니다. 그리고 만약 당신이 정리를 말한다면, 당신은 수준을 만든 것입니다. 그리고 만약 당신이 정리를 증명한다면, 당신은 그 수준을 푼 것입니다.

스트로가츠 (10:28): 어제 오늘 토론을 준비하면서 링크를 확인했는데, 게임도 생각나게 하는 일종의 리더보드가 있습니다. 저는 지금 생성되고 있는 수학 라이브러리에 70,000개 정도의 정리가 있다는 것을 확인했습니다. 그리고 누가 Lean에 몇 시간을 보냈는지에 대한 목록이 있습니다.

독수리 (10:50): 시간이 아닙니다. 그것은 코드 라인이 측정하는 것입니다.

스트로가츠: 코드 라인입니다.

독수리: 우리는 코드 줄을 세고 있습니다. 그렇습니다. 또는 증명된 정리를 셀 수도 있습니다. 예, 순위표가 있습니다. 저는 경쟁심이 강한 사람이 아닙니다. 그래서 저는 이 순위표에서 높이 올라가려고 하지 않습니다. 그러나 이런 종류의 일은 실제로 매우 강력하게 작동합니다. 캠브리지에 학부생이 있습니다. 야엘 딜리스, 소프트웨어에 관심을 갖게 된 것은 불과 XNUMX개월 전쯤일 것입니다. 그리고 리더보드에서 더 높은 자리에 오르려는 것이 그가 상당히 진지하게 생각하는 일이라는 것을 알게 되었습니다. 이것이 누군가를 위한 경쟁인 줄은 정말 몰랐습니다. 저는 일부를 취하고 있습니다. 도서관이 성장하는 것을 보고 싶은 더 넓은 관점입니다. 린 커뮤니티는 놀라운 사람들의 그룹입니다. 수학자와 컴퓨터 과학자들이 서로 상호작용하고 전에 본 적이 없는 방식으로 협력하고 있습니다.

스트로가츠 (11:42): 글쎄요, 여기에서 구별하기 위해 조심합시다. 제 생각에는 지금까지 우리 언어로 우리가 해야 할 세부 사항과 함께 철자를 쓰지 않았을 수 있기 때문입니다. 린과 라이브러리의 차이점. 그렇다면 린과 관련하여 라이브러리는 무엇입니까?

독수리 (11:57): 린은 모든 것을 움직이는 힘입니다. 그러나 린 자신은 수학을 거의 알지 못합니다. 자연수 또는 정수에 대해 알고 있습니다. 그것은 이러한 것들에 대한 몇 가지 기본적인 사실을 알고 있습니다. 예를 들어 정수를 더하고 곱하여 정수를 얻을 수 있다는 것을 알고 있습니다. 정수를 더하고 곱할 수 있다는 것을 알고 있습니다. 하지만 실수, 숫자선, 대부분의 수학자들이 당연시 여기는 것들. 핵심 린(Lean)이 작동하도록 하는 데는 이러한 것들이 필요하지 않습니다. Core Lean은 프로그래밍 언어가 되기 위한 절대적인 기초만 있으면 됩니다.

(12:32) 그러면 수학은 어디로 갑니까? 2017년에 그들은 이 새로운 수학 도서관이 탄생하기로 결정했습니다. 그것은 불렸다 mathlib, 린의 수학 도서관. 그리고 당시에는 아주 작은 프로젝트였습니다. 그리고 아이디어는 Lean이 확인하는 컴퓨터 확인 수학이 될 것이라는 것이었습니다. 따라서 Lean은 프로그래밍 언어입니다. Lean은 정리 증명자일 뿐만 아니라 프로그래밍 언어입니다.

(13:00) 이제 우리는 정리에 해당하는 이 프로그래밍 언어로 작성된 XNUMX/XNUMX만 줄의 코드를 가지고 있습니다. 하지만 이는 린 자체와는 별개입니다. 그래서 Lean은 성장하고 발전하고 수학 라이브러리는 성장하고 발전합니다. 그러나 이들은 두 개의 다른 실체입니다. Lean은 Microsoft에서 운영하고 수학 라이브러리는 커뮤니티에서 운영합니다. 우리는 그들의 소프트웨어와 함께 작동하는 라이브러리를 만들고 있을 뿐입니다.

(13:24) 이제 이 개발자들도 Microsoft에서 일하지 않는다는 점을 말씀드리고 싶습니다. 우리는 그들의 프로젝트의 포크를 만들었습니다. 그래서 마이크로소프트는 린 3을 작성하고 그것을 내세웠다. 그것은 무료 및 오픈 소스 소프트웨어이며, 거기에 집어넣었습니다. 하지만 요즘은 린 4를 열심히 개발하고 있습니다. 그래서 커뮤니티가 린 3을 실행하게 되었습니다. 따라서 린 3 코드 자체를 유지 관리하는 것은 대부분 컴퓨터 과학자들입니다. 그러나 수학자들은 거기에 가지 않는 경향이 있습니다. 수학자들은 모두 도서관을 짓는 데 관심이 있습니다. 린 자체가 힘을 실어주는 것 같아요. 모든 검사를 수행하지만 라이브러리는 모든 수학이 진행되는 곳입니다.

스트로가츠 (14:01): 린 3과 4를 언급하면 ​​사실 긴장됩니다. 이전 버전과의 호환성 문제가 있습니까? 예를 들어, Lean이 일부 새 버전에서 만들어지고 귀하와 라이브러리가 호환되지 않을 수 있습니까?

독수리 (14:15): 물론, 정확히 무슨 일이 일어났는지입니다. 이것은 실제로 이야기의 흥미로운 부분 중 하나입니다. 제 말은, 마이크로소프트가 린 3를 출시했고 그들은 "알았어, 여기 있다. 이제 사용자 기반을 확보할 수 있는지 봅시다.” 그러다가 사회학적인 이유로 갑자기 그 사용자 기반이 매우 빠르게 나타나는 것 같았습니다. 그러나 그것은 어떤 이유에서인지 이 수학 라이브러리를 작성하는 것에 매우 흥분한 수학자들로 가득 차 있는 것 같았습니다.

(14:43) 내가 말했듯이 이 정리 증명자들은 아주 오랫동안 존재해 왔습니다. 그러나 실제로 수학자들이 연구 수준의 수학을 하도록 강요한 것은 사실이 아닙니다. 그리고 그것이 일어나기 시작했을 때, 우리는 Lean 3와 관련된 문제에 부딪히기 시작했습니다. 그리고 Microsoft와 특히, 소프트웨어 작성자인 de Moura는 우리가 하는 일을 살펴보았습니다. 다시 시작하고 싶은 기분이 듭니다. 더 나은 방법으로 처음부터 전체를 다시 작성하십시오.” 그래서 마이크로소프트는 지난 4년 정도 린 3를 작성해 왔으며, 약간의 심각한 디자인 변경이 있었기 때문에 린 4과 역호환되지 않습니다. 그래서 이제 우리는 거대한 수학 라이브러리를 갖게 되었고 아주 새로운 린 4가 생겼습니다. 그리고 "이 수학 라이브러리를 린 XNUMX로 어떻게 가져갈 것인가?"에 대한 큰 질문이 있습니다.

(15:37) 그래서 바로 지금, 이것이 어떻게든 린 4 커뮤니티에서 일어나고 있는 주요 사건입니다. 그들은 3/4백만 줄의 수학을 린 XNUMX에서 린 XNUMX로 변환하는 컴퓨터 프로그램을 작성하고 있습니다. 그들은 몇 달 안에 완료될 수 있다고 말합니다. 그러나 이것은 매우 어려운 문제입니다.

(15:55) 사실 Microsoft가 저에게 접근하여 “왜 이 수학 라이브러리를 밀어붙이는 겁니까? 우리는 아직 준비가 되지 않았기 때문입니다. 아시다시피, 린 3은 실험입니다.” 그리고 내 대답은 "정말 미안하지만 너무 재미있어서 멈출 수 없습니다."였습니다.

스티브 스트로가츠 (16:12): 린에 대한 린이란 무엇입니까?

독수리 (16:13): Lean의 장점은 커널이 상당히 작다는 것입니다. 이것은 신뢰 문제에 관한 것입니다. 이것은 컴퓨터 과학에 가깝습니다. 아이디어는 정리가 옳다고 말하는 것이 무엇을 의미합니까? "글쎄, 충분한 수치 데이터가 있는 한 이것은 물리학에서 사용하기에 완벽하게 실행 가능하고 작동하는 가설입니다"라고 말하는 물리학자가 있을 수 있습니다. 그리고 나서 "글쎄요, 사실, 우리가 진정으로 원하는 것은 증거입니다."라고 말하는 수학자들이 있습니다. 저널은 권위 있는 수학 저널에 게재된 저널 기사를 의미하며, 이 같은 심사 과정을 거쳤습니다.”

그러나 컴퓨터 과학자들은 실제로 수학 문헌의 말뭉치가 오류로 가득 차 있다는 점을 지적하기에는 너무 빠르지 않습니까? 그리고 우리가 정리가 증명되었다고 말할 때, 우리는 "오, 이 정리는 참이다"라고 말할 때가 있습니다. 그러나 4.3년 후, 일부 똑똑한 대학원생이 보조 정리 XNUMX의 증명에서 일부 오류를 발견했기 때문에 우리는 이것에 대해 일종의 롤백을 해야 했습니다.

(17:12) 또는 때때로 수학 커뮤니티에서 약간의 논쟁이 있습니다. 그리고 컴퓨터 과학자들이 말하는 것은 "음, 사실, 우리는 더 나은 것을 제공합니다. 알다시피, 린에서 정리를 증명할 수 있다면 수학의 공리까지 확인되기 때문입니다." 좋아, 하지만 이제 더 편집증적으로 가자. 린에 버그가 있다면? 그러나 아이디어는 Lean의 커널이 극도로 작아야 한다는 것입니다. 따라서 린에 버그가 있는 것이 정말 걱정되고 컴퓨터 과학자라면 해당 코드를 읽어보는 것이 어떻겠습니까? 무리한 말이 아니기 때문입니다.

스트로가츠 (17:45): 컴퓨터 수준에서 피어 리뷰와 거의 비슷합니다.

독수리 (17:48): 네, 컴퓨터 피어 리뷰입니다. 그래서 정말 할 수 있습니다. 예, 누군가 다른 운영 체제에서 실행되는 다른 프로그램을 다른 언어로 작성하여 동료 검토를 수행할 수 있습니다. 하지만 — 하지만 수학자로서 저는 이것에 대해 그다지 신경 쓰지 않습니다. 제 말은, 어느 시점을 넘어서면 좀 우스꽝스러워지는 것 같아요. 내가 증거를 이해하거나 커뮤니티가 증거를 이해한다면 저는 그것이 사실이라고 말할 수 있어 기쁩니다. 예를 들어, 페르마의 마지막 정리(Fermat's Last Theorem)는 매우 기쁩니다. 페르마의 마지막 정리가 증명되었습니다. Lean에서 그것을 증명하는 것은 수백 인년의 작업 가치가 될지라도 수학 커뮤니티에 의해.

스트로가츠 (18:22): 그러면 질문이 생깁니다. 다시 이 문제로 돌아가 보겠습니다. 당신은 어떤 것이 린에게 가르쳐졌다고 언급했고, 어떤 부분은 수학, 어떤 부분은 제가 인상을 받았습니다. 글쎄요, 당신은 페르마의 마지막 정리를 언급했습니다. 그리고 거기에 들어가는 모든 거대한 수학 장치는 아직 수학 라이브러리의 일부가 아닙니다. 그렇다면 현재 그곳에는 어떤 것들이 있고, 지평선 너머에는 무엇이 있을까요?

독수리 (18:45): 도서관이 생긴 지 XNUMX년이 되었습니다. 그리고 제 생각에는 학부생이 학교에서 XNUMX년을 보냈다면 알 수 있는 정도에 대해 알고 있다는 점에 주목하는 것이 흥미로울 것 같습니다. 그래서 인간과 거의 같은 속도로 학습하는 것 같습니다. 하지만 물론 강조하지만, 그것은 인간과 같은 방식으로 생각하지 않는 것입니다. 그렇죠? 사람이 입력한 결과를 확인하는 것 맞죠? 질문을 하면 "예, 알겠습니다. 질문 내용을 이해합니다."라고 말합니다. 그러나 학부생에게 문제를 해결하도록 요청하면 학부생이 아이디어를 내기 시작할 수 있습니다. 반면에 지금 Lean은 이렇게 말합니다.

스트로가츠 (19:23): 내 소개에서 Peter Scholze를 언급했습니다. 수학의 천재 린을 위해 당신에게 찾아온 사람. 무슨 일이 있었는지 알려주세요.

독수리 (19:31): 그래서 다시, 이것은 정리가 증명된다는 것이 무엇을 의미하는지에 대한 생각으로 돌아갑니다. 우리는 어떻게 그 정리가 참인지 어떻게 압니까? 그래서 피터 숄즈와 더스틴 클라우젠 그들은 새로운 이론을 개발하고 있으며, 그들은 그들의 새로운 이론이 분석의 특정 분야에서 대수학의 기술을 사용할 수 있게 해주기를 바라고 있습니다. 이전에는 어려웠던 문제를 공격하는 데 사용할 수 있는 새로운 기술이 갑자기 많이 생겨나기 때문에 이것은 멋진 일입니다. 그래서 Scholze와 Clausen은 몇 가지 아이디어를 개발했고 Scholze는 2019년과 2020년에 Bonn에서 이에 대해 강의했습니다. 강의 노트는 인터넷에 올라와 있습니다. 그리고 이 강의 노트에는 모든 것을 하나로 묶는 몇 가지 정리가 있습니다.

(20:21) 그리고 이것은 Scholze가 하기로 결정한 실험입니다. 그는 생각했습니다. 어떤 수학자들이 지금까지 그것을 주의 깊게 확인했는지 궁금합니다.” 그러나 그는 두 번째 과정에서 하나의 특정 정리인 Theorem 9.1에 특히 관심이 많았습니다. 그래서 그는 저에게 연락을 취해서 이렇게 말했습니다. "네, 알다시피, 우리는 그것들을 살펴보는 데 많은 시간을 보냈습니다." 그리고는 “그래서 정리 9.1의 내용을 다 확인했습니까?”라고 물었다. 그리고 저는 말했습니다. 우리는 9장에 도달하는 데 9.1시간이 걸렸습니다. 그리고 우리는 그것에 대한 어떤 종류의 개요를 얻어야 합니다. 그래서 우리는 모든 기술적 세부 사항을 확인하지 않았습니다.” 그래서 그는 정리 XNUMX의 이러한 기술적 세부 사항을 정확히 누가 확인할 것인지에 대한 질문을 제기했습니다.

(21:07) 아마 아무도 그 증거를 읽지 않을 것입니다. 하지만 물론 Scholze는 Fields 메달리스트이므로 사람들은 그가 똑똑한 사람이라고 생각할 것이므로 이 정리가 맞다고 확신합니다. 그래서 그는 "음, 사실, 아마도 컴퓨터는 이러한 세부 사항을 확인할 수 있는 아주 좋은 위치에 있을 것입니다."라고 말했습니다. 그래서 우리는 그것이 흥미로운 프로젝트가 될 것이라고 생각했습니다. 그리고 천천히 이것을 린에게 가르치는 절차를 시작했습니다. 이 팀, 제 말은, 많은 사람들이 관련되어 있었고, 협력적인 노력이었습니다. 누구나 참여할 수 있습니다. 거기에는 — 박사 학위가 있었습니다. 캠브리지에서 온 학생이 나타났습니다. 워털루의 연구원이 나타났습니다. 그리고 두 명의 이탈리아 대수기하학이 나타났습니다. 이 사람들은 목공 작업에서 막 나타나기 시작했고 수학에서 Scholze-Clausen 단어를 Lean의 언어로 번역하는 이 일을 시작했습니다. 왜냐하면 그것은 일종의 번역 과정이기 때문입니다.

(21:59) 그래서 이 번역 과정은 약 9.4개월이 걸렸습니다. 그리고 그 시점에서 우리는 정리 9.4를 모두 증명했습니다. 그리고 우리는 현재 정리 9.1가 정리 9.4을 의미한다는 증거를 아직 번역하지 않았기 때문에 아직 끝나지 않았습니다. 하지만 우리는 이것을 깨닫지 못했지만, 정리 9.4를 끝냈을 때 Scholze가 말했습니다. “좋아, 이제 나는 믿는다.” 이것이 그가 걱정했던 것 같다. 9.1에서 9.4까지는 좀 더 개념적이었고 그는 주장에 자신이 있었습니다. XNUMX의 증거는 우리의 현재 시스템이 세부 사항을 확인하지 않을 것이라고 우려했기 때문에 이제 컴퓨터가 확인했습니다. 그래서 그는 기본적으로 지금, 그는 행복하다고 발표했습니다.

스트로가츠 (22:43): 음, 당신이 제기하는 사회학적 문제에 대해 묻겠습니다. 당신은 정리 9.4의 이 증명의 성공을 고려할 때 더 보수적인 반대론자들이 이제 합류하기 시작할 것이라고 생각할 것이라고 말합니다. 그런 일이 일어나고 있습니까? 당신이 말할 수있는 한?

독수리 (22:58): 사람들, 특히 젊은 사람들이 오고, 그래서 더 많은 프로젝트가 나타나고 있습니다. 우리는 Lean 커뮤니티에서 기하급수적인 성장을 하고 있습니다. 수학자들이 관심을 갖고 참여하면서 "아, 우리가 다른 프로젝트를 하는 게 어때?"라고 생각하는 것 같습니다. 예를 들어 페르마의 마지막 정리는 실제로 수백 인년 떨어져 있다고 언급했습니다. 그래서 여전히 매우 야심찬 프로젝트입니다. 그러나 정규 소수에 대한 페르마의 마지막 정리를 증명하는 것은 100년이 넘은 결과입니다. 그리고 그것은 여전히 ​​​​매우 존경할만한 결과입니다. 이런 종류의 일을 하려면 상당한 양의 대수적 정수론이 필요합니다.

그리고 저와 같은 수학자 그룹이 있습니다. 우리는 아마도 미디어 소음에 매료되어 이제 정규 소수에 대한 페르마의 마지막 정리를 증명하고 있습니다. 그리고 다른 일을 하는 사람들이 있고, 구체 반전의 증거를 연구하는 사람들이 있습니다. 그들은 당신이 구체를 뒤집을 수 있다는 것을 증명하려고 노력하고 있습니다. 다른 프로젝트가 막 뜨고 있습니다. 그리고 결국에는 무슨 일이 일어날지, 흥미로운 일이 충분히 일어나서 결국 사람들이 알아차리게 될 것이라고 생각합니다. 이 소프트웨어는 현대 수학자들이 사용하고 있는 정리를 증명하고 있습니다.

스트로가츠 (24:07): 그래서 지금은 수학자들이 린에게 수학을 가르치고 있는 것 같습니다. 그리고 나서 린은 자신이 잘하는 일을 하고 있는 것 같습니다. 논리적 단계를 확인하여 요약된 증명 전략이 실제로 수행될 수 있는지 확인합니다. 모든 세부 사항이 공리 수준에 이르기까지 제자리에 놓이도록 만들 수 있습니다. 그러나 머지않은 미래에 린의 후손이 인간 교사가 도서관을 만드는 대신 스스로 수학을 가르칠 수 있는 때가 올 것이라고 상상하십니까? 그들은 문헌을 읽고 일종의 독학을 할 수 있을 것입니다.

독수리 (24:48): 그래서 저는 컴퓨터 과학자가 아닙니다. 그리고 저는 이것을 일종의 주요 목표로 절대적으로 집중하는 많은 컴퓨터 과학자와 인공 지능 전문가를 만났습니다. 그리고 저는 이 모든 것이 10년 안에 일어날 것이라고 말하는 낙관론자들을 많이 만났습니다. 10년이 지나면 컴퓨터는 인간이 할 수 없는 정리를 증명할 것입니다.

(25:14) 페르마의 마지막 정리를 증명하는 데 무엇이 필요한지 알기 때문에 더 신중할 것입니다. 제 말은, 저는 대수적 수 이론가입니다. 그리고 이 모든 일이 제가 박사였을 때 일어났습니다. 학생 및 박사후 연구원. 그리고 페르마의 마지막 정리의 증명은 믿을 수 없을 만큼 길고 기술적이며 그것을 증명하기 위해 우리가 현재 알고 있는 유일한 알려진 증명은 타원 곡선, 모듈 형식 및 갈루아 표현과 같은 이국적이고 보다 현대적인 수학적 대상을 포함합니다. 이것들은, 알다시피, 페르마가 전혀 몰랐던 것들입니다. 그리고 이러한 아이디어가 모듈 형식의 개념으로 구체화되기까지 아주 많은 세월이 걸렸습니다. 이것은 정확히 올바른 종류의 것으로 판명되었습니다. 이것은 정수론의 중심 개념입니다.

(26:00) 그게 수학의 예술적인 부분인 거 알지? Lean은 과학적인 부분을 아주 잘 수행하고 있습니다. 알다시피, 모든 것은 매우 엄격하게 정의되어 있으며 매우, 매우 명확한 규칙이 있습니다. 하나는 과학을 따르고 하나는 정리를 증명합니다. 그러나 모듈 형식의 개념이나 타원 곡선의 개념을 만들거나, 갈루아 표현의 아이디어, 이것들은 인간에 의해 매우 많이 형성된 것들입니다. 따라서 컴퓨터가 그러한 통찰력을 가질 수 없다면 — 그리고 나는 그들이 필요한 수준에서 그러한 통찰력을 가질 수 있다고 아직 확신하지 못합니다 — 제 수학 영역에서 정리를 증명할 때 큰 불이익을 받게 될 것입니다. 예를 들어, 수 이론에서.

그러나 수학의 다른 분야에서는 기발한 아이디어를 모아서 새로운 정리를 증명했지만 새로운 도구를 만들 필요가 전혀 없었습니다. 도구는 이미 그곳에 있었다. 따라서 우리가 컴퓨터, 이 분야 중 한 곳에서 알려진 모든 도구를 가르친 다음, 이제 가십시오. 이제 그것들을 수십억 가지 다른 방식으로 조합하기 시작하고 어떤 방법이 생산적인지 확인하면 컴퓨터가 더 많은 성공을 거두십시오.

스트로가츠 (26:06): 좋습니다. 다음 질문에 대한 완벽한 설정입니다. 우리가 탐구하고 싶은 질문은 다음과 같습니다. 우리는 다른 영역, 훨씬 더 제한된 영역에서 해당 질문에 대한 답변을 가지고 있습니다. 수학 — 즉, 최고 수준의 체스 영역. 우리는 대답이 예라는 것을 압니다. 내 말은, Deep Blue가 우리에게 그 답을 주었기 때문입니다. 이것은 체스 위치, 초당 200억 위치를 계산할 수 있는 기계였습니다. 그것은 그랜드 마스터에 의해 내장 된 어떤 위치가 좋고 어느 쪽을 선호하는지 결정하는 방법에 대한 평가 기능을 가지고 있습니다. 그것은 어떤 의미에서도 상상할 수 없었지만 매우 빠르게 계산할 수 있었습니다. 그리고 요즘에는 누구나 본질적으로 지구상의 모든 사람을 이길 수 있는 체스에서 컴퓨터로 게임을 할 수 있습니다. 그래서 저는 우리가 알고 있는 것 같습니다. 그렇습니다. 도메인이 충분히 제한된다면 순수한 속도로 상상력 부족을 보완할 수 있습니다. 체스처럼.

독수리 (28:07): 나는 당신이 정확히 옳다고 생각합니다. 체스는 일종의 경계 영역입니다. 하지만 다시, 지금 컴퓨터는 바둑에서 인간을 이길 수 있다 지금, 그렇지? 또한 Go가 제한된 도메인이라고 주장할 수도 있습니다. 하지만 바둑 게임을 시작할 때 361개의 움직임을 만들 수 있습니다. 그리고 물론, XNUMX번의 이동으로 우리는 이미 엄청나게 많은 숫자에 도달하고 있습니다. 그럼에도 불구하고 바둑에서는 컴퓨터가 인간을 이기고 있습니다. 게다가 그들은 그 데이터 세트 없이 바둑에서 인간을 이기고 있지 않습니까? Deep Blue는 사용할 수 있는 수천 개의 그랜드마스터 체스 게임에 대한 방대한 데이터 세트를 보유하고 있었지만 DeepMind는 실제로 스스로 바둑을 가르치는 기계를 만들 수 있으며 어떤 인간보다 빠르게 더 나은 사람이 될 수 있음을 보여주었습니다.

(28:53) 보드 게임과 수학의 또 다른 큰 차이점은 보드 게임은 XNUMX인용 게임이라는 것입니다. 알다시피, 컴퓨터는 스스로를 상대로 놀고 스스로의 실수로부터 배우려고 노력할 수 있습니다. 그것은 실수를 할 수 있고, 그런 다음 실수를 악용할 수 있습니다. 그리고 수학은 어떻게 보면 XNUMX인용 게임입니다. 그렇지 않습니다, 그것은 같은 종류의 것이 아닙니다. 문제를 풀고 공리 뒤에 공리를 던질 수 있습니다. — 우리는 문제에 대해 정리 후에 정리를 던질 수 있으며, 알다시피, 점점 더 많은 이론을 발전시킬 수 있습니다. 그리고 결국, 당신은 많은 사실을 알게 되었고 질문은, 당신이 이기고 있느냐는 것입니다. 당신은 그 게임에서 이기고 있습니까? 당신, 당신은 - 그 정리를 증명하는 데 더 가까워졌습니까? 그리고 지금 이것이 가장 큰 문제라고 생각합니다. 당신은 당신이 이기고 있는지 아닌지 전혀 알 수 없습니다.

(29:35) 그리고 나는 이것을 학부 시절로 절대적으로 기억합니다. 우리는 정리를 증명하려고 하고 있고, 강사는 칠판에 올라가서 글을 쓰고 있습니다. 그리고 저는 생각하고 있습니다. 가고 있다? 우리는 이 정리를 증명하는 데 더 가까워졌습니까?” 그리고 갑자기 화려하게 번성하다가 모든 것이 내리막길입니다. 당신은 기발한 움직임처럼 기발한 아이디어를 생각해냅니다. 그러다가 갑자기 쉬워집니다. 이것이 수학의 큰 문제입니다. AI를 끌 수 있고 수백 줄의 코드를 작성할 수 있다는 것입니다. 그런 다음 뒤로 물러나서 이렇게 말할 수 있습니다. “우리가 실제로 시작할 때보다 더 가까워졌습니까? 아니면 우리가 훨씬 더 멀리 떨어져 있습니까?” 그리고 바로 지금, 이것은 우리가 전혀 알지 못하는 또 다른 영역이라고 생각합니다. 나는 컴퓨터가 그것을 알아낼 수 있다고 생각하지 않는다.

스트로가츠 (30:25): 컴퓨터를 위한 창의적인 수학자가 되는 것이 어렵다는 것을 알려주는 공식이 마음에 듭니다. 왜냐하면 그것은 우리 모두가 창의적이 되기 위해 노력하면서 겪었던 경험을 많이 상기시키기 때문입니다. 수학자. 아니면 고문으로서, 지금은 대학원생이 있을 때 항상 이것을 봅니다. 그 학생은 몇 년 동안 일하면서 “우리가 좋은 박사 학위를 받는 데 더 가까이 다가갔습니까?”라고 궁금해 할 수 있습니다. 문제, 그리고 그것에 대한 좋은 해결책은?”

독수리 (30:51): 수학은 어렵습니다. 이게 문제 야. 그리고 여러 가지 다른 방식으로 어렵습니다. 제 말은, 우리가 지금 하고 있는 한 가지는 수학이 얼마나 어려운지 컴퓨터 과학자들에게 가르치는 것입니다. 그리고 제 생각에 이 협업에서 일어나고 있는 일 중 하나는 컴퓨터 과학자들이 현대 수학이 실제로 어떻게 생겼는지에 대해 더 많이 배우기 시작했다는 것입니다. 그리고 AI 사람들이 거기에서 가져갈 수 있습니다. 하지만 이것은 이번 협업에서 나온 것 중 하나입니다.

스트로가츠 (31:22): 멋지네요, 케빈. 이러한 마음을 뒤흔드는 질문을 탐구하는 데 시간을 할애해 주셔서 감사합니다.

독수리 (31:28): 정말 감사합니다.

아나운서 (31:31): 원하는 경우 이유의 기쁨, 체크 아웃 Quanta Magazine 과학 팟캐스트, 이 쇼의 프로듀서 중 한 명인 Susan Valot가 진행합니다. 또한 이 팟캐스트에 대해 친구들에게 알리고 좋아요를 누르거나 듣고 있는 곳을 팔로우하십시오. 사람들이 찾는 데 도움이 됩니다. 이유의 기쁨 팟 캐스트.

스트로가츠 (31 : 51) : 이유의 기쁨 의 팟캐스트입니다. Quanta Magazine, Simons Foundation에서 지원하는 독립적인 편집 간행물. Simons Foundation의 자금 지원 결정은 이 팟캐스트 또는 이 팟캐스트의 주제, 게스트 또는 기타 편집 결정에 영향을 미치지 않습니다. Quanta Magazine. 이유의 기쁨 Susan Valot와 Polly Stryker가 제작했습니다. 편집자는 John Rennie와 Thomas Lin입니다. 우리의 테마 음악은 Richie Johnson이 작곡했으며 저는 귀하의 호스트인 Steve Strogatz입니다. 질문이나 의견이 있으시면 언제든지 듣고 싶습니다. quanta@simonsfoundation.org로 이메일을 보내주십시오. 듣기 주셔서 감사합니다.

spot_img

최신 인텔리전스

spot_img