아마 최근의 수학계에서의 화두들 중 하나는 수많은 수학적 정리들을 computer assistant로 검증하려는 것이겠죠. 예를 들면 Scholze의 condensed mathematics에서의 중요한 정리 하나가 formalizing되었단 건 꽤 유명한 것 같아요. 이 사이트를 들어가 보면 수많은 우리가 기초적이라고 생각하는 수학적 정리들이 lean으로 formalizing되어 있는 걸 발견할 수 있어요.
수학자들이 스스로의, 혹은 다른 사람의 정리를 computer assistant로 검증하려는 주된 동기는 "어느 정리가 정말로 맞는지 인간의 불확실한 검증 말고 컴퓨터로 확실히 검증하려는 것"일 거예요. Voevodsky는 다음 인터뷰에서 다음 둘을 말했지요.
"Cohomological Theory of Presheaves with Transfers"라는 자신의 논문의 key lemma가 사실은 틀렸고, 결국 main theorem을 좀 더 weak form의 형태로 다시 증명해야 했다. 수많은 사람들이 이미 자신의 논문을 공부하는 세미나를 열었는데, 아마 자신이 대가로 유명한 수학자라 다들 내 실수를 제대로 확인 안 하고 넘긴 것 같다.
Carlos Simpson는 자신과 Kapranov의 논문 "∞-groupoid and homotopy types"의 main theorem이 사실은 틀렸음을 증명했다. 하지만 자신은 Simpson이 틀렸다고 2013년까지(!) 생각했는데, 결국 내가 틀렸었다.
Voevodsky는 이런 경험들을 바탕으로 univalent foundations이란 걸 만들게 되었죠. 인터뷰 말미엔 computer assistent가 good idea가 아니라는 수많은 수학자들의 불평에 "I think this is very wrong"이란 표현까지 쓰고 있네요.
이런 식으로, 저를 포함한 꽤 많은 수학자들은 스스로, 혹은 다른 사람들의 정리들이 "틀리는" 것에 꽤 민감하곤 하고, 이런 틀린 것들을 줄이기 위해서 꽤 노심초사하는 것 같아요. Computer assistant도 이런 "틀리는" 것을 줄이기 위함이고 말이죠.
그렇다면, 우리가 이렇게나 우리의 정리들이 틀리는 것에 민감하다면, "틀렸다"라는 것이 무슨 의미인지 한 번 보는 게 좋을 것 같아요. 다음 슬로건을 보지요.
Slogan 1. 어느 정리, 혹은 그 증명이 "틀렸다"라는 것은, 그 정리, 혹은 그 증명을 형식화할 수 없을 때를 말한다. 혹은, 형식화했을 때 invalid하단 결과가 나오는 것을 말한다.
이는 얼핏 보면 꽤 만족스러운 것 같아요. 만일 제가 리만 가설을 증명했다고 소리치고서 그 증명으로 "외계인이 나에게 전파를 쏴서 리만 가설이 참이라고 나에게 영감을 줬다"라고 말한다면, 그 누구도 이를 믿지 않겠죠. 그리고 그 근거로 제대로 수식으로 형식화되지 않은 증명을 제가 전혀 가져오지 않아서 그렇고 말이에요.
하지만 이 슬로건은 한편으론 너무 강력한 것 같아요. Kevin Buzzard의 다음 에세이에도 드러나듯이, 수학자들의 수많은 "canonically isomorphic"이란 용어의 사용은 굉장히 이상하고 제대로 정의되지 않은 용어예요. 그리고 형식주의의 입장에서 이 용어가 쓰인 증명은 아무래도 전혀 형식화될 수 없거나, 적어도 형식화되기 너무나도 어려운 용어지요. 그렇담, 이런 용어를 맘대로 쓴 모든 정리들, 예를 들면 Grothendieck의 EGA와 SGA의 대부분은 틀린 것인가? 이렇게 말하는 건 너무 힘들어 보여요. 그리고 많은 사람들은 왜 이렇게 보기 너무 힘든지에 대한 이유도 잘 댈 수 있겠죠. 어차피 이런 정의로서의 "틀렸음"은 우리가 수학을 하는데 있어서 별 문제가 되지 않기 때문에. 역사를 파고 보면 칸트의 순수이성비판에서도 나오는 주장으로, 수학은 우리의 직관으로 하는 것이고, 우리가 수학을 직관으로써 해나가는데 있어서 별 문제가 되지 않는다면 이런 식으로 "틀렸음"을 정의해봤자 이런 식의 틀림을 우리가 왜 신경써야 하는지 전혀 모르겠죠. 이는 Buzzard도 이런 수학적 실천은 important하다고 인정하고 있죠.
덤으로, Slogan 1은 "형식화"라는 것이 무슨 의미인지에도 대해서 별로 말하는 게 없어요. 우리는 수학을 엄밀하게 해야 한다고 생각하곤 하지만, 정작 "엄밀하게"가 뭔 뜻인지에 대해선 설명하기 힘들죠. "형식화"라는 것을 예를 들어 lean으로 정리 내지 증명을 코딩한단 의미로 쓴다고 대충 정의해도 문제인 것이, 우리가 증명 내지 정리를 형식화하려는 것, 혹은 우리가 computer assistant를 쓰려는 이유는 우리가 틀리지 않기 위함인데, "틀렸음"을 이런 식으로 정의해버리면 우리가 왜 틀리지 말아야 하는지에 대한 근거를 댈 수 없을 것 같아요. 왜 틀려지 말아야 하지? 우리는 증명을 형식화해야 하므로. 우리는 왜 증명을 형식화해야 하지? 우리는 틀리지 말아야 하므로. 이런 식으로 순환논증에 빠져버리니 말이죠.
따라서, 슬로건을 Slogan 1에 대한 비판을 의식해서 다음과 같이 바꿔보지요.
Slogan 2. 어느 정리, 혹은 그 증명이 "틀렸다"라는 것은, 그 정리, 혹은 그 증명을 받아들였을 때 수학자 커뮤니티의 수학적 실천을 방해할 때를 말한다.
Voedvosky의 예시를 들면, Simpson과 Kapranov-Voevodsky 둘 중 하나가 틀린 이유는 어느 결과가 동시에 맞으면서 틀릴 수는 없기 때문이고, 이런 모순됨은 우리의 수학적 실천을 크게 방해하기 때문이겠죠. 이는 수학을 학문으로써 기능하게 하지 못 하고 마치 어느 것을 마음 내키는 대로 "리만 가설은 그냥 아름다우니 맞는 거야"라고 말하도록 우리를 유도하는 것 같으니 말이죠. 그리고 이런 마인드를 극단적으로 적용해보면 수학자 커뮤니티는 그저 직관의 아름다움과 황홀함을 실토하는 장이 될 것이고, 우리는 이런 수학자 커뮤니티를 왜 존중해야 하는지 전혀 알 수 없지요. 그리고 이는 (형식화가 가능하단 가정 하에) 우리가 왜 형식화를 해야 하는지에 대한 좋은 답이 될 수도 있을 것 같아요. 둘 중 하나는 틀렸고, 누가 틀렸는지 판가름하기 위해서 우리의 수학적 직관을 잘 형식화해야 한단 답을 내면 말이죠. (만약에 둘 다 틀렸고 우리가 이 셋이 하는 수학 분야를 없애야 한다고 주장하게 된다면, 아래에서 답할 것인데, 이는 풍요로운 수학을 하는 게 아니므로 결국 이런 판가름 과정은 반드시 있어야 한다고 말할 수 있을 것 같아요.)
수학적 실천의 방해가 수학의 학문성을 저해하는 것만 있진 않을 거예요. 예를 들면 꽤나 많은 수학자들은 선택 공리를 자연스럽게 쓰면서 선택 공리의 사용을 반대했던 Brouwer를 잘 이해 못 하는 경향이 있는데, 이는 선택 공리가 참이라고 받아들였을 때 우리가 할 수 있는 수학적 실천의 폭이 대폭 확대되기 때문이죠. (Hilbert가 했던 말을 반복한다면, "Brouwer와 Weyl의 주장을 받아들이면, 우리는 가장 값진 보물을 잃어버리고 말 것이다.") ([Reid70], p155) 우리는 좀 더 풍요롭게 수학을 할 필요가 있고, 이런 풍요로운 수학을 위해 선택 공리를 참인 것으로 여기고 선택 공리의 부정을 틀린 것이라고 여길 필요가 있다고 말할 수도 있겠죠. 덤으로 우리가 Slogan 2를 받아들일 때, 우리가 형식화를 진행한다면, 최대한 풍요로운 수학을 할 수 있는 방향으로 우리가 형식화를 진행해야 한단 결론까지 얻을 수 있겠죠. 우리가 유클리드 공리계 내지 페아노 공리계가 아니라 ZFC, 혹은 HoTT를 수학의 기초로 여기는 이유를 아마 여기서 찾을 수 있을 테고요.
그리고 Slogan 1하곤 다르게 Slogan 2는 우리에게 반드시 수학 증명들의 형식화를 하는 것을 요구하지는 않는 것 같고, 따라서 모든 증명들을 반드시 형식화할 필요는 없고, 우리가 할 수 있는 만큼만 형식화하고 나머지 수학 분야들은 전통적인 방식으로 증명을 체크하란 식으로도 나올 수 있을 것 같아요. 예를 들면 위에서도 언급한 "canonical isomorphism"이 많이 등장하는 분야나, 다른 분야들에 비해서 형식화가 많이 까다로운 것 같은 위상수학, 집합론같은 분야가 말이죠. 이는 모든 수학들을 하나의 형식화로 묶는 보편적인 수학을 포기하는 방식이지만 말이죠.
(우리가 정말로 형식화를 해야 한다면 어느 방식으로 해야 하는지, computer-assistant proof에 대한 더 많은 이야기들은 나중에...)
[Reid70] C. Reid: Hilbert, Springer, Berlin, 1970.
푸앵카레는 "과학의 가치"란 책에서 수학자들을 크게 "논리파"와 "직관파"로 나눈 바 있어요. 논리파는 최대한 주어진 조건 하에서 어느 성질이 성립할 수 있는지 매우 꼼꼼하게 따지는 버릇이 있고, 직관파는 뭔가 직관적으로 성립할 것 같은 무언가를 대충 증명해내죠. (그리고 전 제가 생각하기론 전적으로 직관파에 속해요. 푸앵카레도 푸앵카레 추측에 담긴 스토리를 생각해보면 전적으로 직관파인 것으로 보이고요.)
대체로 이 둘은 수학이 무엇인지에 대해서 견해차를 드러내는 것 같아보이진 않지만, 가끔씩 이 둘이 충돌하는 경우를 볼 수 있는 것 같아요. 예를 들면 전 일명 "병적"인 예시를 찾는데 그다지 소질은 없어서 논문에 예시가 별로 없단 소리를 들은 적이 많고, 이는 그냥 수학적 직관이 이끄는 대로 수학을 하는 제가 수많은 예시 없이, 그니까 조심성 없이 수학을 한단 지적일 테고 말이죠. 정 반대의 경우를 들어보면, 꽤 많은 수학자들은 수학을 "직관" 혹은 "철학"이라고 불리는 무언가로 한다고 생각하곤 하고, 수많은 수학 논문의 자그마한 빵꾸들은 대체로 무시하는 경향을 보이죠. 그리고 왠만하면 이것들을 모두 lean으로 코딩해서 검증해야 한다는 Kevin Buzzard와 같은 몇몇 수학자들의 말에 그렇게 귀기울이진 않고 말이죠.
이런 충돌은 그렇게 새삼스럽진 않을 것이고, 먼 과거에도 많이 있던 충돌이죠. 이 글에선 특히 수학이, 칸트의 분석/종합 구분을 빌려서 분석적인지 종합적인지에 대한 논쟁을 논리/직관의 구분 하에서 설명해보고 싶어요. 어쩌면 예상하셨겠지만, 수학이 분석적이라고 주장하는 사람들은 대체로 논리파의 경향을 보이고, 수학이 종합적이라고 주장하는 사람들은 대체로 직관파의 경향을 보이곤 하는 것 같죠.
분석/종합 구분을 아마 처음으로 철학에 도입한 칸트는 수학을 전적으로 선험적 종합명제들의 집합으로 봤죠. 칸트의 근거는, 수학은 우리의 머릿속의 직관으로 하는 것이란 거예요. 예를 들면, 우리는 7+5를 계산할 때, 뭔가 동그라미 일곱개를 상상하고, 다섯개를 상상하고, 이 둘을 모아서 동그라미가 12개라는 걸 상상하니, 이는 7+5=12란 것이고 덤으로 이는 (모든 총각은 미혼이라는 뻔한 정보가 아닌) 우리에게 새로운 정보를 주니 종합적이란 것이죠. 이를 볼 때 칸트는 수학적 직관의 활용이 분명 우리에게 새로운 것을 준다고 판단한 모양이네요.
그에 비해서 프레게는 "산수의 기초"에서 칸트에게 과연 31859235+357892752과 같은 계산들도 그런 식으로 종합적 판단이라고 판단할 수 있는지 묻고 있죠. 이것이 389751987라고 계산하는 과정은 순전히 가장 먼저 5+2를 해서 7이 나오고, 3+5를 해서 8이 나오고, 2+7을 해서 9가 나오고, 9+2를 하면 11이 나오니 일단 네번째엔 1을 쓰고 나머지 1은 다섯번째로 올림하고,... 이런 식으로 매우 기계적인 과정을 거쳐서 나오죠. 이렇게 기계적인 판단은 분명 분석적 판단일 테고 말이죠.
칸트는 수학을 분명 직관적으로 하는 것이라고 생각했고, 이를 수학이 종합적인 지식들의 집합인 근거라고 생각했어요. 그에 비해서 프레게는 수학에 일명 "학문적인 기초"를 세워야 한다고 생각했고, 이것이 수학이 분석적인 지식들의 집합인 근거라고 생각했죠. 그리고 제가 보기에 둘은 살짝 문제로 보이는 곳이 있긴 한 것 같아요.
예를 들면 칸트에게 있어서 정말로 수학을 그냥 직관적으로 하는 것이냐고 물을 수 있죠. 예를 들면, Birkar는 BAB conjecture란 엄청난 것을 증명한 바 있는데, 이런 Birkar가 BAB conjecture를 증명할 때 머리 속에 가지고 있는 의식 경험들을 생각해 보자고요. 칸트에 따르면 이런 의식 경험들이 바로 수학이고, 수학이 종합적 지식인 근거가 되겠죠. 그런데, 이런 의식 경험을 바다에서 파닼대고 있는 참치가 가지도록 우리가 참치의 뇌에 무슨 장치를 연결했다고 치죠. 그렇담, 참치는 수학을 하고 있는 것일까요? 참치는 BAB conjecture의 증명에 대응되는 것 같은 어느 의식 경험만을 가지고 있고, 이를 수식으로 표현하지도 못 하고, 심지어 더하기가 무엇인지, variety가 무엇인지에 대한 제대로 된 sense도 가지고 있지 않죠. 그 의식 경험이 Birkar가 BAB conjecture를 증명할 때 낸 의식 경험이란 것도 물론 모를 것이고요.
즉, 참치는 수학을 하는 것으로 보이지 않아요. 그리고 우리는 우리가 이렇게 판단한 근거도 꽤 잘 말해볼 수 있죠. 이는 그저 의식 경험일 뿐, 그런 의식 경험의 "의미"가 무엇인지에 대해서 참치는 전혀 가지고 있지 않고 있단 식으로 말이죠. 그리고 그 "의미"가 무엇인지에 대해서, 우리는 프레게식의 기초를 댈 수밖에 없는 것으로 보이고 말이죠. Fano variety의 정의는 어떻고, ample divisor의 정의는 어떻고,... 이런 식으로 말이죠. 그렇담 수학은 이런 정의들을 기계적으로 따라가는 행위가 될 것이니 분석적인 지식이 되겠죠.
프레게도 꽤 문제가 많아보여요. 프레게는 수학자들이 자신들이 친숙하게 다루는 자연수가 무엇인지조차 모른답시고 수학에 엄밀한 기초를 세우겠다고 말했지만, 프레게가 기초를 세우고자 하는 수학은 분명 수학자들의 직관에서 비롯된 것일 거예요. 수학자들이 자연수를 떠올리지 못 했다면, 산술의 기초를 세우겠다는 프레게의 프로젝트는 처음부터 시작할 수도 없게 되는 것이고 말이죠. 그러니 수학은 우리에게 몇몇 의식 경험을 필요로 하는 것으로 보이고, 이는 수학이 종합적이란 근거로 제시될 수 있겠죠.
아마 우리가 채택해야 할 입장은, 칸트의 입장과 프레게의 입장의 절충일 것이라고 전 생각해요. 분명 우리가 "수학적 직관" 혹은 "철학"이라고 부르곤 하는 것들을 다양하게 내는 칸트적 입장(물론 칸트는 이런 직관들의 후보로 무엇이 될 수 있는지에 대해서 꽤나 꼬장을 부렸지만 푸앵카레의 규약주의를 살짝 내비치자면)도 중요하고, 이런 직관 내지 철학들을 한 가지 플랫폼(현대 수학에선 대체로 ZFC가 쓰이곤 하는)에다가 표현하는 프레게적 작업도 분명 필요해 보이죠. 정리하자면 대충 이렇게 말할 수 있을 것 같아요.
"논리 없는 직관은 맹목적이고, 직관 없는 논리는 공허하다."
어쩌면 몇몇은 반대할 지도 모르겠지만, 우리가 수학을 할 때 "수학적 사고를 할 때는 이렇게 생각해야 한다"란 식으로 수많은 규범들을 따르려고 한단 점은 아마 부정할 수 없을 거예요. 예를 들면, 제가 리만 가설을 떠올릴 때 어느 황홀한 감정이 들었다고 "오 이래서 리만 가설은 틀렸어!"라고 곧바로 말할 수 없는 이유는,
1. 그런 황홀한 감정이 리만 가설이 거짓이란 근거가 아니기 때문이라고 말할 수 있고, 이는 실은
2. "그런 황홀한 감정으로 리만 가설이 거짓이라고 짐작하지 말아야 한다"라는 우리가 따라야 하는 규범을 제가 해치지 말아야 한단 식으로 생각할 수 있을 거예요.
이런 직관은 꽤나 강력한데, 만일 "황홀한 감정은 리만 가설의 거짓이란 근거가 아니다"가 규범의 일종이라고 볼 수 없게 된다면, 혹은 "올바른" 기술이라고 볼 수 없다고 쳐보죠. 이런 관점의 문제점은, 이런 규범의 부재때문에 누군가가 "황홀한 감정을 리만 가설이 거짓이란 근거야"라고 말해도 우리는 여기에 대해서 "그건 아니야 넌 틀렸어"라고 말할 수 없고 "... 그래" 라고만 말해야 한단 문제점이 발생한단 것이에요. 따라서 수학에서 "틀린 증명"이란 개념은 아예 존재하지 않게 되겠죠. 수학이란 것은 그저 각 수학자들이 수학적 직관에 적당한 기술을 붙인 것에 불과할 테니 말이죠. 하지만 수학에서 틀린 증명이란 개념이 분명 존재해야 하는 것으로 보인단 점에서, 이런 수학적 사고에 규범이 없단 입장은 실패하는 것으로 보이고, 따라서 수학적 사고엔 우리가 따라야 하는 규범이 있는 것으로 보이죠. 분명 앤드류 와일즈의 페르마의 마지막 정리 첫 제시된 증명은 틀린 것으로 보이고 마찬가지로 제가 international journal of mathematics에 처음 제출한 논문에도 틀린 부분이 꽤 많은 것으로 보여야 하는데, 수학적 사고에 우리가 따라야 하는 규범이 없단 입장은 이를 부정합니다!