인상적인 기사가 있어서 하나 번역해 봅니다..
증명검증 프로그램 Lean에 대한 기사입니다.
수학적 증명들은 이해하는 사람이 없을정도로 복잡해졌다.. 하지만 컴퓨터는 가능할지도 모른다.
지금은 수학에 새로운 시대를 열 시간이라고 Kevin Buzzard는 말한다. Imperial College London의 정수론 교수 Kevin Buzzard는
컴퓨터가 순수수학에서, 특히 증명에서 더 큰 역할을 하기를 원한다. 수학적 증명들은 모든 디테일을 증명은 커녕 이해하는 사람조차
없을정도로 복잡해졌다. 그는 이미 인정된 많은 증명들이 사실 틀렸음을 우려하고있다.
수학은 수천년에 걸쳐온 학문으로, 현대적 증명들은 많은 과거의 지식들위에 서있다.
하지만 그는 많은 새로운 증명이 제시된 오래된 증명들이 사실은 확실하게 이해되지 않았다고 한다.
"수학자들이 작은 디테일들을 모두 검증하지 않고, 실제로 제가 그것들이 틀렸음을 보았기 때문에, 여태까지 알려진 수학 자체가 틀렸을까
저는 무섭습니다." 라고 그가 우리에게 전했고, 또 한 발표에서는 다음과 같은 말을 했다.
"제 생각에는 우리가 지어놓은 여러개의 성들 중 여러개들이 모래성이 아닐 확률은 0에 수렴한다고 생각합니다."
원래는 새로운 정리들의 증명은 기초부터 증명되어야 하고, 모든 스텝들이 검증되어야 한다. 다른말로는 순수수학에선 경험이 많고 인정받는 대가들이
중요한 역할을 한다. 만약에 한 대가가 한 논문을 인용하고, 그걸 기반으로 그의 업적을 쌓는다면, 그 인용된 논문은 아마 한번도 다시 검증되지 않을것이다.
Buzzard는 현대수학이 너무 대가들에게 의존한다며 비난한다. 하나의 새로운 논문은 대개 20개의 논문을 인용하고, 그 중 1000페이지에 가까운 증명들도 있다.
아마 한 대가가 그 1000페이지의 논문을 인용한다면, 많은 수학자들은 이미 인용된 논문이 맞음을 가정하고, 사실상 그 누구도 모든걸 다시 검증할 노력을 하지 않는다.
그에 따르면, 1994년도에 발표된 수학계의 가장 어려운 난제 중 하나인 페르마의 마지막 정리의 증명을 제대로 이해하고 있는 사람은 아무도 없다고 한다.
"제 생각에는 지금 죽었거나 살았거나 이 증명의 모든 디테일을 아는사람은 아무도 없습니다. 그럼에도 불구하고 수학자들은 이 증명을 받아들였습니다. 대가들이
이 증명은 OK하다. 라고 판단했기 때문이죠"
몇년전 그는 대가들인 Thomas Hales와 Vladimir Voevodsky의 강연에서 처음 증명검증 소프트웨어에 대해 알게되었다.
이 소프트웨어를 이용해 증명들이 컴퓨터에 의해 시스템적으로 검증된다.
처음 이 프로그램 Lean을 이용해 연구하기 시작하자마자 그는 바로 매료되었다. 이 프로그램은 증명의 모든 의심가는 부분들을 검증할 뿐 아니라,정제되고 실수없는 수학적 사고를 지원하기 때문이다.
"컴퓨터는 오직 아주 엄밀한 Input만을 받아들이고, 이것은 제가 수학에 접근할때 가장 중요하게 생각하는 것입니다."
또 그가 말하길,"전 영혼의 파트너를 찾았다는 생각이 들었고, 사랑에 빠졌습니다. 이 프로그램은 수학에 대해 저와같이 생각합니다."
Lean을 이용해 증명을 검증하기 위해서는 증명은 형식화되거나, 인간의 언어와 기호들을 Lean의 프로그램 언어로 번역되어야 하는데, 이 작업이 매우 고단하지만, Lean은 Buzzard가 입력하는 모든 수학적 문제들을 잘 해결한다. 이것이 Lean과 다른 프로그램들의 차이점이다.
바로 그 점 때문에 Lean에 대한 수학자들의 관심은 날로 커져가는데, 특히 교육쪽에서 그것이 두드러진다.
Jeremy Avigad는 Carnegie Mellon 대학의 증명이론의 교수이다. 그와 Buzzard는 Lean을 증명이론의 개론세미나에 이용하기 시작했다.
이 프로그램은 증명의 모든 구절을 검증하고, 피드백을 주는데, 이것은 학생들에게 특히 도움이 된다.
그렇지만 날로 갈수록 늘어가는 Lean에 대한 관심에도 불구하고, Avigad는 주의를 요구한다. 아직 이 프로그램은 많은 개선이 필요하고, 이런 증명보조를 투입시키는건 시간이 아주 오래걸린다. 그는 다음과 같이 말한다. "이 분야는 수십년전부터 존재하고,항상 개선되고 있지만, 아직 목적에 다다른것은 아니다."
Buzzard의 말에 따르면,여러개의 장애물들을 넘고나면 이 프로그램은 다른 방식으로도 이용될 수 있다.
매년 새로운 연구결과들은 쏟아지기 때문에,이것들의 증명을 검색하는 능력은 말할것도 없이 중요하다.
만약 모든 새로운 Abstracts들이 Lean에 입력된다면, 모든 수학자들은 이 데이터뱅크로부터 엄밀한 수학적 Object를 불러올 수 있을것이고, 그것과 관련한 모든 정보를 얻을 수 있다.
--이하 생략 --
수학의 역사적 흐름에 대한 이해가 부족한 것이 아닌가 합니다. 수학은 오류로부터도 배우고 발전하고 더 단단해집니다. 19세기 중반 대수곡면을 연구하기 시작한 이탈리아 대가들은 여러개의 멋진 결과들을 증명하였으나 또 그만큼 틀린 결과들도 많이 발표하였습니다. 몇 십년이 지난 후 오류가 있음이 드러납니다.
그러나 틀린 부분을 고치고 발전시키는 노력은 계속되었고, 대수기하학의 언어가 새롭게 쓰여지면서 더 단단하게 발전하게 됩니다. 오류로부터 새로운 추측이 만들어지고, 이 추측은 최근에서야 완벽하게 해결되어 대수곡면론과 4차원 사교다양체 사이에 새로운 다리를 놓습니다.
오류가 있을 수 있단 걸 아무도 두려워하지 않는다고요. 오히려 기회죠. 왜 틀렸는지를 파고드는 과정에서 더 멋지고 단단한 것들이 만들어지니까요.
더 문제는... 저 프로그램이 참이라고 내뱉으면, 그건 누가검증합니까? 프로그램 오류의 가능성은요? 또한 와일즈이 증명은 이제 관련 분야 대학원생이면 다들 이해할 수 있는 수준인데 무슨 이야기를 하고 있는지도 도무지 이해가...
이사람 글 안읽어 봤네
제 생각에는 이 텍스트가 말하는 바는 다른거같아요. 첫번째로.. 큰그림으로 봤을땐 그게님 말이 타당한데 수학의 근간이 틀렸을까 우려하고 무서워하는건 일평생을 수학에 바친 한 개인으로써,충분히 느낄 수 있는 감정이라고 생각하고요. 다음으로는 글을 읽어서는 Lean은 0과 1 을 내뱉는 자판기가 아닌거같아요. 매 줄 마다 검증을하고 그에 대한 피드백을 내놓
는다고 하니까, 원하는건 Theorem을 집어넣어서 0 1 을 얻어내는게 아니라, 인간이 할 수 있는 실수들,예를들면 대가중심적이 된다던가 작은 디테일들을 챙기지 못한다거나, 하는 놓치는 부분들을 컴퓨터를 이용해서 보조하려고 한다는 점이 위에 말한 수학의 새로운 시대가 필요하다. 라는 말의 설명인거 같아요. 가래로 막을거 호미로 막는다는말이 있듯이,
예시가 좀 적절하지 않은듯... 일단 와일즈 본인이 살아있는데 ㅋㅋ 실제 수학 역사에서 틀린 증명이 옳다고 받아들여졌던 경우가 있고(반대의 경우도 물론 있고) 또 와일즈 증명 이상으로 '거대한' 증명들이 더 많은거로 암.
그건 또 그렇네요.
우리가 인간으로써 범하는 실수를 아니까, 그것조차 미연에 방지하기 위한 새로운 시도라고 이야기하는거같아요. 그리고 오류로부터 배운다고 하셨는데, 이런 보조하는 도구들을 사용하면,대수기하학처럼 긴 시간이 지나고나서가 아니라 더 빠른시간안에 전부 다는 아니더라도 단 하나의 오류라도 더 빨리 찾아서 보안할 수 있지않을까요? 오류를 통해 더 단단해지는건 모든 학문
이 마찬가지니까, 저것도 연구하다보면 더 좋은 결과를 주지않을까요? 보완*
이거 외에는 전반적으로 동의함. 적어도 이미 알려진 증명들을 기계적으로 검증할 방법이 생기는게 나쁜일일리는 없지. 그게님은 그 프로그램은 누가 검증하냐고 했지만 비슷한 프로그램을 짤 수 있는 모두가 집의 컴퓨터로 검증할 수 있고, 증명과정이 논리기호의 나열수준으로 기초적이면 그야말로 간단한 치환으로도 가능하고,
모두가 집의 컴퓨터로 검증할 수 있다고 생각하듯이, 해당 분야를 공부하는 대학원생부터 연구자까지 모두가 세대를 반복하며 증명을 복기하고 다시 따지고 있거든요. 대가가 참이라고 했다고 그냥 묻고 더블하는게 아니에요.
음 좀더 분명히하자면 수학에서의 human error는 (연구자들의 성실성과 별개로) 드물지만 분명히 발생해왔다고 생각함. 또한 모든 증명들을 모두가 논리기호 나열수준의 low level로 검증하면서 연구하고있거나 그래야한다고 생각하지 않음. 컴퓨터는 분명히 이런걸 (빠르고 오류없이,적게)할 수 있는 계산능력이 있음. 그럼 이를 써먹는 시도가 당연하지 않나
증명 검증기의 존재 이유와 활용 가능성에 대해서 이 글에 동의한거지 페르마 대정리나 대가 운운에 대해서 동의한건 아니었음. 돌다리를 두들기는 방법이 하나 더 있으면 좋은게 당연한게 아닌가
사람수준의 정의 등을 빌린 증명이면 지금처럼 사람이 할 수도 있지 않을까? 어쩌면 지금 알려진 증명과는 다른/더 간단한 증명을 내놓을 수도 있고. 적어도 난 컴퓨터가 수학에 있어서 짜놓은 알고리즘 실행이상을 할 수 있을거고 언젠간 그 이상을 해야만 한다고 생각함.
유투브가 뭔가를 진지하게 다룰때는 걸르는게 낫지
이게 맞네 ㅋㅋㅋㅋ - dc App
ㄹㅇ정론ㅋㅋㅋㅋㅋㅋㅋㅋ
컴퓨터가 현대의 증명을 커버할 수 있을까? 난 회의적이라고 본다. 언젠가는 가능할 수도 있겠지만 아직은 컴퓨터가 할 수 있을 거라는 가능성을 언급할 때가 아니야