아마 최근의 수학계에서의 화두들 중 하나는 수많은 수학적 정리들을 computer assistant로 검증하려는 것이겠죠. 예를 들면 Scholze의 condensed mathematics에서의 중요한 정리 하나가 formalizing되었단 건 꽤 유명한 것 같아요. 이 사이트를 들어가 보면 수많은 우리가 기초적이라고 생각하는 수학적 정리들이 lean으로 formalizing되어 있는 걸 발견할 수 있어요.

수학자들이 스스로의, 혹은 다른 사람의 정리를 computer assistant로 검증하려는 주된 동기는 "어느 정리가 정말로 맞는지 인간의 불확실한 검증 말고 컴퓨터로 확실히 검증하려는 것"일 거예요. Voevodsky는 다음 인터뷰에서 다음 둘을 말했지요.

1. "Cohomological Theory of Presheaves with Transfers"라는 자신의 논문의 key lemma가 사실은 틀렸고, 결국 main theorem을 좀 더 weak form의 형태로 다시 증명해야 했다. 수많은 사람들이 이미 자신의 논문을 공부하는 세미나를 열었는데, 아마 자신이 대가로 유명한 수학자라 다들 내 실수를 제대로 확인 안 하고 넘긴 것 같다.

2. 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학년때 담임선생님이기도 하셨던 수학선생님에게 수학은 직관으로 하는 거란 말을 정말로 질리도록 들었어요. 보통은 수학을 하는 법을 거의 안 말하고 그냥 교과서대로 말할 텐데, 그 선생님만큼은 수학의 직관성을 굉장히 강조했던 기억이 나네요. 예를 들면, 우리가 미분을 할 때 그냥 미분 식을 외우는 것이 아닌, 미분 식의 일종의 정신적인 그림을 그리고 이런 정신적인 그림을 통해서 미분을 해야 한단 식으로 말이죠.

이렇게 수학은 다들 직관으로 하는 걸로 보이는데, 재미있게도 수학의 이런 성질을 처음 구체적으로 말한 사람은, 제가 알기론 칸트가 처음일 거예요. 칸트는 수학에 대한 플라톤주의적 입장을 배격하고 수학은 실은 우리의 정신 활동의 일종이며, 수학의 확실성은 우리 마음 바깥의 객관적인 무언가에 의해 보장되는 것이 아닌 우리 마음(일명 "순수 직관")의 사용으로 보장된다고 주장했죠. 예를 들면 플라톤은 7+5=12인 이유로 7이라는 이데아가 있고 5라는 이데아가 있고 12라는 이데아가 있고, 이 세 이데아의 성질이 7+5=12를 만족해서 그렇다고 설명할 것이라면, 칸트에 따르면 7+5=12인 이유는 그냥 우리 마음이 7+5=12란 식으로 지시를 하기 때문에, 그러니까 우리의 "직관"이 7+5=12라고 말하고 있기 때문이라고 답할 거예요.

이렇게 칸트가 수학 실천에서 직관의 중요성을 강조한 이후로, 수많은 수학자들은 자신이 진리를 찾고 있다는 플라톤의 방식으로 말하기보단 자신이 수학을 직관으로 하고 있고, 진리는 아무래도 모른단 식으로 말하는 편을 좋아하는 것 같긴 해요. 아마 현재로선 수학자들 중에서 수학을 직관으로 한단 것을 부정하는 사람은 아무도 없겠죠. 예를 들면 우리가 두 집합의 곱을 생각할 때 직관적으로 좌표평면을 생각하고 이를 통해서 두 집합의 원소를 대응하는 것을 상상하지, 아마 아무도 {a,{a,b}}따위를 생각하진 않을 거예요. 마찬가지로, 집합론자와 같은 변태가 아닌 이상 자연수 1,2,3,4,...는 그냥 그 자체로 1,2,3,4,...지, 결코 {},{{}},{{{}}},...나 0={},1={0},2={0,1},3={0,1,2},...따위를 생각하진 않겠죠. 마찬가지로 미적분학은 변화에 대한 학문이고, 대수학은 구조에 대한 학문이고,... 우린 수학을 이렇게 상상하지, 결코 이런 수학을 매우 비직관적으로 논리같은 것으로 환원해서 생각하는 사람은 적어도 수학자 중에선 없을 것이라고 전 확신할 수 있어요.

그렇다면, 누군가는 제 고등학교 선생님에게 이렇게 질문할 수 있을 지도 몰라요. "아니, 미분은 그 식을 외우는 것이 아닌 미분에 대한 정신적인 그림, 그러니까 "직관"으로 하는 것이라고 너는 말하고 있는데, 나한텐 미분식을 외우는 것이 직관이다!! 꼭 너의 방식만 직관이냐??? 나는 미분식을 마음 속에서 그릴 수 있고, 그런 미분식을 이리저리 변형해볼 수 있다!! 심지어 이런 방식은 너가 너의 방식으로 생각해내지 못 했던 무언가를 생각할 수도 있게 해준다! 직관에 대한 편협한 시각을 멈춰라!!"

예를 들면, 칸트는 시공간에 대한 우리의 직관이 반드시 하나로 고정되어 있다고 본 바 있고, 그렇기에 유클리드 기하학이나 뉴턴 역학이 영원할 것이란 시각을 내비친 바 있죠. 하지만 우리는 비유클리드 기하학에 대한 직관도 분명 가질 수 있고, 상대성 이론에 대한 직관 역시 가질 수 있으며, 아마 칸트는 이 부분에선 틀렸다고 생각되곤 하죠. 브라우어 역시 숫자들은 우리의 구체적인 숫자에 대한 직관을 이용한 정신적 구성이어야 한답시고 선택공리를 끝끝내 부정했지만, 사실 우리는 선택공리의 사용 역시 충분히 "선택"이란 관점에서 원소를 구성하고 있다고 볼 수 있으므로 우리의 정신적인 구성이라고 생각할 수 있고, 선택공리의 부정은 그냥 브라우어의 개취라고도 볼 수 있겠죠. 심지어 이런 입장은 수학은 실은 직관으로 한단 입장을 부정하지도 않죠. 이런 입장이 요구하는 것은 수학을 할 때는 직관 외의 것이 필요하다고 말하는 것이 아닌, 우리에게 다원적인 직관이 있을 수 있음을 긍정하란 것이니 말이에요.

그럼에도 사람들이 어느 정도 수학적 직관/비직관의 구분을 유지하길 바라는 이유는, 수학이 원천이었던 직관에서 멀어진다면 더 이상의 수학 실천은 힘들어질 것이라고 보는 데에 있겠죠. 예를 들면 폰 노이만이 수학은 "경험적 원천에서 너무 멀어진 수학은 퇴화할 위험이 있다"고 본 것이 있겠네요. 만일 우리가 자연수를 그냥 1,2,3,4,...로 보지 않고 {},{{}},{{{}}},...로 본다면 우리의 자연수에 대한 수학적 실천은 크게 저하될 것이고, 미분을 제 고등학교 선생님마냥 직관적으로 변화에 대한 학문으로 보지 않는다면, 우리는 미적분학을 할 수 없게 되겠죠. 위의 어느 학생의 항변 역시 암묵적으로 미적분학에 대한 올바른 직관을 사용하고 있다고 말할 수도 있을 지도 모르겠고요. 예를 들면 해석적 정수론은 정수론에 매우 연속적인 미적분학을 사용한단 점에서 미적분학을 평소랑 다른 직관으로 바라보는 것 같지만, 결국은 이산적인 정보들을 연속적으로 다시 해석하고 이를 통해서 정수론을 연구한단 점에서 결국은 미적분학의 원래 직관과 별로 동떨어진 것은 아니라고 말할 수도 있어 보이겠죠. 제가 최근 준비하고 있는 논문도 해석적 정수론하고 비슷하게 매우 이산적이어 보이는 어느 module의 length를 계산하는데 미적분학적 직관을 이용하는데, 이 역시 module의 length를 연속적인 무언가로 해석함으로써 미적분학의 올바른 직관을 적용하고 있는 것에 불과하다고 말할 수도 있을 것 같고요. 만일 우리가 미적분학을 그르게 사용한다고 한다면, 우리의 수학 실천은 아예 불가능할 지도 모른단 것이 그들의 주장이겠죠. 칸트가 유클리드 기하학과 뉴턴 역학은 영원불멸할 것이라고 본 것은 지금 보면 그냥 비수학자의 헛소리에 불과하겠지만, 이는 칸트의 주장이 틀려서가 아닌, 칸트가 아직 스스로의 기하학에 대한 직관이 비유클리드 기하학과 상대성 이론에도 똑같이 적용 가능하단 것을 잘 몰랐기에 그렇다고 변명해볼 수 있을 것이고요.

2. 힐베르트는 일명 "형식주의"라는 것을 주장했는데, 이는 수학의 엄밀함을 보장하기 위해서 제시한 거예요. 좀 더 정확히 말하면, 힐베르트는 수학적 직관들을 유한개의 기호를 이용해서 나타내길 바랬고, 이런 기호들의 일관적인 법칙이 있길 바란 것이겠죠. 이런 바람은 괴델이 (적어도 2차 산술을 포함하는 공리계에선) 그런 일관적인 법칙이 있단 것을 증명하는 것부터 스스로 증명할 수 없음을 증명해낸 이후로 대체로 실패한 프로젝트로 여겨지곤 하지만, 그래도 형식주의는 수많은 수학적 직관들을 한 가지 보편 언어로 표현하려고 노력했단 점에서 노력점수 정도는 얻을 수 있겠죠.

형식주의적 입장에선 우리가 지닐 수 있는 수많은 수학적 직관들은 한 가지 일관적인 언어에 의해 표현될 수 있어야 해요. 예를 들면 미적분학과 현대대수학은 그냥 서로 동떨어진 완전 쌩판 다른 두 수학이 아닌, 서로 한 가지의, 집합론이 되었든 type theory가 되었든 뭐가 되었든 한 가지 언어로 표현될 수 있어야 하죠. 그래야 서로 다른 두 수학이 그냥 완전히 다른 것이 아닌 한 가지 "수학"이라는 이름 아래에 뭉칠 수 있을 것 아니겠어요? 물론 이 과정에서 우리가 각 분야에 가지고 있었던 수학적 직관은 퇴화할 수도 있겠지만, 적어도 힐베르트의 입장에서 이런 리스크는 수학을 정말로 통일된 하나의 학문으로 만드는 것, 혹은 수학을 엄밀한 학문으로 만드는 것에 비하면 별 거 아니라고 판단한 것 같죠.

하지만 칸트와 브라우어를 비롯한 직관주의자들이 보기엔 수학을 엄밀한 학문으로 만들어야 하는 이유는 딱히 없을 거예요. 수학은 기본적으로 수학적 직관의 발휘고, 수학을 엄밀한 학문으로 만드는 것이 직관 발휘에 방해가 된다면 수학의 엄밀성 정도는 그냥 갖다 버릴 수 있는 거겠죠. 미적분학과 현대대수학이 하나의 수학이라고 불릴 수 있는 이유는 그들 사이를 잇는 한 가지 보편 언어가 있어서가 아니라, 둘 다 "수학적 직관"이라고 명명할 수 있는 적절한 내적 경험을 비슷비슷하게 제공하기 때문이겠죠.

다만 형식주의라고 해서 수학을 직관으로 한다는 것을 부정하는 것은 결코 아니예요. 힐베르트는 대놓고 수학은 "칸트적 직관"으로 하는 행위라고 말한 바 있고, 형식주의가 주장하는 바는 브라우어가 힐베르트에게 뻥친 것과 같이 우리에게 소중한 수학적 직관을 내팽겨치고 수학을 그저 기호 게임으로 만들어버리는 것이 아닌, 그저 수많은 수학들이 공유할 수 있는 한 가지 보편 언어를 만들고, 모든 수학자들이 이런 보편 언어에 충실하길 바란 것 뿐이죠.

도덕철학에 이런 입장들을 대비시켜보면 나름 재미있을 것 같아요. 예를 들면 형식주의는 한 사람의 삶과 한 사람의 일명 "행위자성"을 분리한 다음에 우리는 우리의 삶을 한 발짝 물러서서 보면서 그런 삶들이 공존할 수 있게 하는 어느 법칙을 언제나 입법한다는 칸트적 구성주의에 해당될 것이고(웃기게도 수학철학에서의 칸트의 입장하곤 정 반대인 셈이죠), 직관주의는 우리의 삶 내지 정체성이 우리의 전부고 우리는 이런 정체성에 충실하면서 살아야 한다는 입장이 되겠죠. 이건 상당히 생철학 비슷하고, 브라우어부터 쇼펜하우어 덕후였음을 생각하면 굉장히 자연스러운 대응일 거예요.

도덕철학에서 칸트적 구성주의는 우리(수학으로 따지면 "수학")를 행위자성을 발휘하는 행위자로 정체화하길 바라고 있고, 생철학 비스무리한 것은 우리의 정체성을 우리의 삶 그 자체로 바라보는 것을 요구하고 있죠.

이 두 관점은 서로 장단점이 뚜렷한 것 같죠. 예를 들면 칸트주의가 시도때도 없이 먹고 있는 욕은 칸트주의가 과도하게 우리의 삶을 그저 관조하는 것으로 바라보고 있지만, 실은 이런 관조 자체가 우리의 삶의 일종에 불과하다는 것이고, 제가 기억하기론 헤겔부터 칸트에게 이런 욕을 시전한 걸로 알고 있어요. 이들은 "삶"과 "행위자성"을 구분하려다가 행위자성 역시 한 가지 삶에 불과함을 간과하는 자가당착적 모습을 보이는 셈이죠. 생철학 비스무리한 것 역시 우리가 우리의 삶들을 경험하고 이를 표현할 수 있는 것 자체가 이미 우리의 삶들을 언어화하고 하나의 통합적인 무언가로 바라보는 것에 불과하다는 반론이 가능하죠. 만일 이런 언어화 내지 통합적인 무언가로 바라보는 것 없이 그저 경험 원툴이라면, 니체가 원하는 힘에의 의지들의 경합도 불가능하고, 브라우어가 바라는 수학적 직관의 발휘는 그저 마약을 하는 것하고 하등 다를 바 없는 내적 체험에 불과한 것 같으니 말이죠. 이들은 언어 없이 수많은 삶 내지 직관들을 향유하는 것이 가능하다고 생각하고 싶어하는 모양이지만, 실은 수학적 직관을 발휘해서 무언가를 해내는 것 자체가 그런 직관을 일종의 언어로 쓰는 것에 불과하단 점에서 (셀라스의 용어로 우리는 언제나 "이성의 공간" 안에 들어와 있을 수밖에 없단 점에서), 예를 들면 미적분학을 하는 것 자체가 미적분학에 대한 직관 자체를 하나의 언어로 보고 그 언어의 룰에 맞게 우리가 풀고자 하는 수학 문제를 나타내는 것에 불과하단 점에서 그들은 자가당착적이라는 비판을 피할 수 없을 테죠. 이렇게 쓰고 보니 둘 다 자가당착적이네요?? 그럼 두 입장 다 틀린 거고 플라톤주의가 맞는 건가? 하하...

3. 저로선 두 입장 모두 틀렸다고 보진 않고, 둘 다 어느 정도의 진실을 말하고 있다고 생각해요. 예를 들면 도덕철학의 눈으로 바라보는 형식주의에 의하면, 우리는 수학 실천을 할 때 그 어느 경우에도 수학을 형식화하는 것을 절대로 멈출 수 없죠. 고대 이집트 때부터 이미 수학자들은 기하학을 할 때 어느 정도의 형식화는 반드시 했고, 그 형식화 하에서 기하학과 대수학을 통합해서 토지를 측량한 셈이죠. 힐베르트는 그저 이를 최대한 밀어 붙히려다가 괴델한테 한 방 먹은 것에 불과하고 말이에요. 하지만 힐베르트가 아마 틀린 점은, 수학은 칸트적 직관으로 함을 인정했으면서도 

3.1. "칸트적 직관"과 "직관의 형식화"를 은밀히 계속해서 구분하려고 했던 태도고, 

3.2. 우리는 직관의 형식화에 충실해야지 칸트적 직관에는 (도덕철학에서의) 칸트를 빌려서 "한 발짝 물러서서 보려고 했단" 점에서

직관주의자들의 반발을 불러 일으켰겠죠. 직관주의자들이 틀린 점은, 위에서 봤듯 수학은 결코 비언어적인 것이 될 수 없고, 우리는 암묵적으로나마 언제나 수학을 반드시 형식화할 수밖에 없단 점을 들 수 있겠죠.

그렇다면 이 둘을 어떻게 융합시켜야 할까요? 저로선 수학적 구조주의가 이 둘을 융합한 가장 적절한 형태의 입장이라고 생각합니다. 수학적 구조주의는

(ㄱ) 형식주의마냥 우리의 칸트적 직관과 우리의 형식화를 과도하게 구분하지 않고 이 둘을 똑같이 "구조"라고 칭하고 있고,

(ㄴ) 직관주의마냥 수학은 비언어적이라는 꽤나 황당해보이는 입장을 견지하지 않고 구조는 반드시 언어의 특성을 띄고 있음을 인정하고 있죠.

즉, 형식주의가 직관주의에게 주장했던 바하고 직관주의가 형식주의에게 주장했던 바를 모두 포함하고 있는 주장이 수학 적 구조주의라고 볼 수 있겠죠. 이 주장은 나름 만족스러워 보이고, 저는 그래서 수학적 구조주의자입니다. 아마 힐베르트와 브라우어도 그들이 살았던 시기에 이 입장이 명시적으로 있었담 이를 받아들였을 것 같고, 아마 compositio mathematica는 영원히 생기지 않았겠죠