원문: https://x.com/getjonwithit/status/2035052237777486024

조너선 고라드 ( Jonathan Gorard )

2026년 3월 20일

수학은 많은 것이다. 그것은 우아한 문화적 인공물이다. 그것은 거대한 지적 구조물이다. 그것은 자연과학, 사회과학, 계산과학을 위한 도구들의 집합이다. 그리고 그 밖에도 많은 것이다. 그러나 내가 개인적으로 보는 수학은 더 명료하게 사고하고, 더 정확하게 추론하며, 더 모호하지 않게 언어를 사용하는 과정이다. 그리고 수학이라는 학문 분야 자체는 이것이 더 잘 일어나도록 해 주는 통찰들의 역동적이고 성장하는 집합이다. 논문, 정리, 증명 등은 언제나 수학의 진짜 산물, 즉 인간의 통찰과, 그것과 함께 오는 인간 사고를 위한 더 정제되고 더 강력한 도구들을 전달하는 다소 불완전한 메커니즘이었다(c.f. Bill Thurston). 그런데 생성형 AI의 등장과 함께, 이러한 역사적 전달 메커니즘들과 수학의 진정한 산물 사이의 상관관계는 빠르게 0으로 향하고 있다(이것은 더 큰 사회적 현상의 일부이기도 한데, 역사적 신호들이 그 역사적 실체로부터 분리되어 가는 현상, 예컨대 글쓰기가 “사유의 증거”라는 지위를 잃어가는 현상이다). 이러한 점을 염두에 둘 때, 내가 지금 이 순간 생각하고 있는 핵심 질문은 우리가 생성형 AI를 어떻게 더 분별 있게 활용하여 인간의(수학적, 과학적 등) 통찰의 생산을 가속할 수 있을까 하는 것이다.

AI는 본질적으로 마찰을 줄이는 도구다. 머지않아 어떠한 종류의 (인지적) 마찰도, 원리상, AI를 통해 0으로 줄일 수 있게 되리라는 가정 위에서 생각해 보자. 이러한 전개는 우리에게 어떤 마찰이 생산적이고 어떤 마찰이 그렇지 않은지를 매우 깊이 생각하도록 요구한다.

이를테면 당신이 트리 탐색 알고리즘을 구현하고 싶다고 하자. 자바로 하면, 필요한 온갖 보일러플레이트와 상태 처리 등 때문에 아마 100줄 정도는 들 것이다. 하스켈로 하면, 패턴 매칭과 대수적 데이터 타입 덕분에 아마 10줄 정도면 될 것이다. 코딩 에이전트를 쓰면, “트리 탐색 알고리즘을 구현해라”라는 짧은 한 문장으로 끝난다. 자바 구현이든 하스켈 구현이든, 그것을 직접 작성하는 과정은 트리 자료구조의 본성, 트리 순회 알고리즘의 재귀적 성질 등에 대해 어느 정도의 통찰을 준다. 그렇다면 자바에서 추가로 써야 하는 약 90줄이, 하스켈의 약 10줄을 통해 얻은 것 이상으로 무언가 추가적인 통찰을 주는가? 논쟁의 여지는 있겠지만, 그다지 많지는 않을 것이다. 실제로는 하스켈 구현의 더 높은 간결성이 자바 구현보다 더 많은 통찰을 준다고도 할 수 있다. 왜냐하면 하스켈에서는 관련된 데이터 구조에 훨씬 더 가까운 수준에서 사고하도록 강제되기 때문이다. 따라서 자바의 그 약 90줄의 보일러플레이트는 비생산적인 마찰로 간주될 수 있다. 즉, 작업을 통해 얻는 통찰의 수준을 유의미하게 떨어뜨리지 않으면서도 제거할 수 있으므로, 다른 표현 언어로 전환함으로써 추상화하거나 자동화해 없애는 것이 타당한 종류의 마찰이라는 뜻이다(아마도 그렇지만, 이 점은 잠시 후 다시 이야기하겠다).

반면 코딩 에이전트에 주는 프롬프트는 문제에 대해 정확히 0의 통찰만을 얻은 채 작성될 수 있다. 분명 당신은 하스켈 구현에 비해 마찰을 줄였다. 그러나 이제는 분명히 너무 멀리 가버린 것이다. 왜냐하면 과제 자체의 목적도 함께 파괴했기 때문이다. 다시 말해, AI를 사용함으로써 당신이 제거한 것은 생산적인 마찰이었다. 중간값 정리를 빌리자면, 대략 10줄짜리 하스켈 구현과 한 문장짜리 에이전트 프롬프트 사이 어딘가에는, 과제를 그 인지적 핵심으로 응축시키면서도 (거의) 모든 비생산적 마찰은 제거하고, 동시에 (거의) 모든 생산적 마찰은 보존하는 어떤 표현 언어가 존재한다. 내가 “거의”를 괄호로 처리한 이유는, 이런 경우에는 어느 정도의 트레이드오프가 항상 필요하리라고 생각하기 때문이다(아마 자바 구현을 직접 써 봄으로써만 얻을 수 있고 하스켈 구현만으로는 얻을 수 없는 어떤 추가적인 통찰이 있긴 할 것이다. 다만 그 추가 통찰의 수준이 작업의 지루함 증가에 비례해서 커지지는 않으므로, 그런 경우라면 그 트레이드오프를 감수할 가치가 있을 수 있다는 것이다).

커리-하워드 동형성 덕분에, 프로그램에 대해 성립하는 것은 증명에 대해서도 성립한다. √2가 무리수임을 증명하고 싶다고 해 보자. 정을 들고 그 증명을 돌판에 새길 수도 있을 것이다. 그러나 볼펜으로 종이 위에 그 증명을 적는 쪽을 택했다면, 나는 당신이 (대체로?) 비생산적인 마찰 하나를 제거한 것이라고 말하고 싶다. 하지만 에이전트에게 “√2가 무리수임을 증명해라”라고 프롬프트를 줘서 증명을 생산하도록 선택한다면, 이제는 생산적인 마찰들까지 전부 제거해 버린 셈이고, 그 결과 문제의 본성에 대한 더 깊은 통찰도 전혀 얻지 못하게 된다. 위와 같은 중간값 정리 식의 논변을 다시 적용하면, 볼펜과 완전 자율적인 “에이전트 워크플로” 사이 어딘가에는, 증명의 핵심과 그 통찰은 응축해 남기면서도 불필요한 지루함은 걷어내는 어떤 중간적 표현이 존재한다. 여기서 주목할 점은, 어느 정도의 지루함은 필요하며, 실제로 선호되기까지 한다는 것이다. 손글씨는 타이핑보다 더 번거롭지만, 뇌 활성화가 더 크고 기억의 질도 더 높다(내가 노트를 모두 손으로 쓰고 TeX로 치지 않는 데에는 이유가 있고, 코드를 쓸 때 탭 자동완성 사용을 거부하는 데에도 이유가 있다). 모든 인지적 과업에는 최적인 수준의 권태, 고역, 마찰이 있으며, 그 수준은 분명 0이 아니다.

나는 또한 겉보기에는 비생산적으로 보이는 마찰들 가운데 일부조차 실제보다 더 생산적일 수 있다는 주장에도 귀를 기울이고 있다. 소프트웨어 개발자들이 흔히 말하는 일화 가운데 하나는, 보일러플레이트 코드를 쓰는 일이 뇌를 “쉬게” 해 주면서도 동시에 당면 문제와 적어도 어느 정도는 관련된, 약간은 몰입을 요구하는 운동 과제를 계속 수행하게 해 준다는 것이다. 그리고 그런 조합이 새로운 생각과 통찰을 낳는 데 특히 비옥하다는 것이다. 나 자신도 그런 경험을 많이 했고, 감자를 깎거나 설거지를 하는 동안 떠오른 다른 많은 아이디어들도 있었다. 감자 깎기는 겉으로 보기에는 분명 비생산적인 마찰처럼 보인다(적어도 수학을 한다는 관점에서는 그렇다). 그러나 그것을 완전히 제거하는 일은 오히려 역효과를 낼 수도 있다. 우리도 이런 덜 분명한 트레이드오프들을 의식해야 한다.

내가 약 10년 전 자동 정리 증명에 처음으로 관심을 가졌을 때, 형식 정리 증명 시스템들이 사용하는 저수준 표현들은 대부분의 수학자들이 굳이 쓸 만큼의 것이 아니고 지나치게 번거롭다는 점이 매우 분명했다. 앞의 자바 구현이나 돌판 사례와 마찬가지로, 미자르(Mizar), 린(Lean), 혹은 로크(Rocq) 같은 언어로 증명을 형식화하는 과정에서 어떤 추가적인 통찰이 분명히 생기긴 했다. 그러나 많은 경우, 아니 대부분의 경우에 그 통찰의 수준은 과업의 노력 증가에 비례해 커지지 않았고, 따라서 대부분의 수학자들은 비형식 수학을 추구하면서 더 깊은 통찰을 얻는 데 시간을 쓰는 편이 낫다고 정당하게 결론 내렸다. 생성형 AI는 이러한 도구들에 대한 진입 장벽을 크게 낮춰 주었다. 그러나 위의 예들에서와 마찬가지로, 과업의 지루함을 지나치게 많이 줄임으로써 목표 자체를 완전히 놓쳐 버리기도 너무 쉬워지게 만들었다. 그 과정에서 생산적인 마찰은 모두 사라진다. 비형식적 수학 결과를 처음부터 끝까지 자동 형식화하는 일은 어떤 의미에서 이 현상의 가장 극단적인 극한 사례다. 우리는 계속해서 다음과 같은 실존적 질문을 던져야 한다. “도대체 우리는 왜 이 모든 일을 하고 있는가?”

Dan Dennett는 “I’ve Been Thinking”에서 자신이 상상력의 보철물이라 부르는 것에 대해 노틸러스 머신 대 불도저라는 구도를 제시한다. 무거운 물건을 들어 올리고 싶다면, 노틸러스 머신을 사용해 스스로를 더 강하게 만든 다음 그 강화된 힘으로 물건을 들 수도 있고, 불도저를 사용해서 물리적 힘 자체의 필요를 우회할 수도 있다. 수학적 형식화의 목표 가운데 일부는 언제나 인식론적인 것이었다. 즉, 어떤 결과가 참이라는 점을 우리에게 납득시키는 것이다. 자율 AI 에이전트에 의한 처음부터 끝까지의 자동 형식화라는 불도저는 그 목표를 엄청나게 가속할 것이 분명하다(실제로 이미 그렇게 하고 있다). 그러나 목표의 훨씬 더 큰 부분은 교육적이기도 했다. 즉, 어떤 결과가 왜 참인지를 우리에게 설명하는 것이다. 그 목표를 위해서는, 내 주장은 오직 노틸러스 머신만이 충분하다는 것이다. 그리고 지금 이 순간 AI 기업들(그리고 연구자들)의 관심은 노틸러스 머신보다는 불도저 개발 쪽에 훨씬 더 쏠려 있다.

분명 어떤 계열의 반쯤 자연어적이고 반쯤 형식적인 중간 표현 언어들이 존재한다. 그것들은 “리만 가설을 증명해라”라고 한 번 던져서 끝내는 AI 에이전트의 무통찰적 불도저와, 500쪽짜리 비형식적 증명을 저수준으로 손수 형식화하는 최대 통찰적이지만 동시에 최대한 고된 작업 사이 어딘가에 놓여 있다. 그러한 표현 언어를 구현하려면, 고전적/결정론적 상호작용과 완전 자동 정리 증명, 그리고 현대적/비결정론적 에이전트 하네스를 결합해야 할 가능성이 크다. 그러나 그 설계에는 더 분명한 수학적, 계산적, 언어학적 통찰뿐 아니라 인간의 심리학적·신경과학적 통찰도 함께 필요할 것이다. 어떤 의미에서 이것은 보다 최적화된 수학적 표기법을 개발하려는 역사적 탐구의 자연스러운 연장선이다(c.f. Ken Iverson). 그리고 표기법이 그렇듯이, 최적의 선택은 적어도 어느 정도는 수학자/실천가에 따라 달라질 것이다.

적어도 단기적으로는, 그러한 표현 언어가 어떤 모습일 수 있는지, 그리고 그것을 어떻게 현실로 가져올 수 있을지를 규명하는 데 우리 시간의 상당 부분을 바치는 것이 중요하다고 나는 생각한다. 그것은 수학만이 아니라 더 넓게는 과학 전반을 위해서도 그렇다. 나 역시 앞으로 몇 달 동안 내 시간의 상당 부분을 여기에 대해 생각하고 작업하는 데 바칠 생각이다.