블라디미르 보예보츠키(Vladimir Voevodsky)

블라디미르 보예보츠키는 1966년 소련 모스크바에서 태어났습니다. 모스크바 국립 대학을 학위 없이 떠난 그는 하버드 대학에서 다비드 카즈단의 지도로 1992년 박사 학위를 받았고, 서른여섯 살이던 2002년 필즈상을 받았습니다. 그런데 필즈상 뒤 그의 연구는 뜻밖의 방향으로 꺾였습니다. 가장 추상적인 수학의 한복판에서 일하던 그가, 수학자들이 쓴 증명을 컴퓨터가 확인하게 하는 일, 그리고 그 일에 알맞은 수학의 새 기초를 만드는 일에 남은 생을 걸었습니다.

나이 세 ·

그의 첫 업적은 대수 기하학에 있습니다. $x^2 + y^2 = 1$ 같은 다항 방정식의 해집합(대수다양체)은 실수⁠(real number)⁠에서는 원이라는 도형이지만, 유한체⁠(finite field)⁠나 다른 수 체계⁠(number system)⁠에서 풀면 점들이 흩어진 모임이 됩니다. 도형의 구멍이나 연결 상태 같은 성질을 재는 위상수학의 도구, 곧 연속적으로 변형해도 변하지 않는 것을 다루는 위상수학의 호모토피 이론을 이런 대상에 옮길 수 있을까요? 보예보츠키는 파비앵 모렐과 함께, 위상수학에서 변형을 재는 실수 구간 $[0, 1]$ 대신 '대수적인 직선' $\mathbb{A}^1$을 써서 변형을 정의하는 호모토피 이론을 세웠습니다. 이것으로 그로텐디크가 1960년대에 꿈꾼 '모티브', 곧 여러 코호몰로지⁠(cohomology)⁠ 이론 밑에 깔린 하나의 이론을 상당 부분 실현한 모티브 코호몰로지를 만들었고, 이차 형식⁠(quadratic form)⁠과 체의 성질에 관한 밀너 추측을 증명했습니다. 이 업적으로 필즈상을 받았고, 더 일반적인 블로흐–가토 추측의 증명은 마르쿠스 로스트 등의 결과와 함께 2011년에 마무리되었습니다.

방향을 바꾼 계기는 증명의 오류였습니다. 그는 1991년 미하일 카프라노프와 함께 공간의 모양을 ∞-준군이라는 대수 구조로 적는 정리를 발표했는데, 1998년 카를로스 심프슨이 그 주요 정리에 대한 반례를 담은 원고를 내놓았습니다. 보예보츠키의 회고에 따르면, 자신은 그 뒤로도 오랫동안 자기 논문이 맞다고 믿었고, 논문이 틀렸다고 확신하게 된 것은 2013년 가을이었습니다. 전문가들조차 한 증명이 맞는지 틀린지를 15년 동안 가리지 못할 수 있다면, 점점 길고 복잡해지는 현대 수학의 증명은 무엇으로 믿을 수 있을까요? 그는 답이 컴퓨터의 확인에 있다고 보았습니다. 그런데 기존의 증명 보조기⁠(proof assistant)⁠로 호모토피 이론 같은 수학을 적는 일은 너무 번거로웠습니다. 문제는 도구가 딛고 선 기초에 있었습니다.

그의 착상은 마르틴뢰프의 타입 이론⁠(type theory)⁠에서 '같음'을 새로 읽는 것이었습니다. 타입 이론에서 $a$와 $b$가 같다는 명제는 그 자체로 하나의 타입⁠(type)⁠이고, 그 원소⁠(element)⁠가 같음의 증명입니다. 보예보츠키는 (스티브 아워디와 마이클 워런 등의 앞선 관찰과 나란히) 타입을 공간으로, 원소를 점으로, 같음의 증명을 두 점을 잇는 경로로 읽으면 타입 이론의 규칙이 모두 맞아떨어진다는 것을 보였습니다. 경로를 거꾸로 가는 것이 대칭성, 이어 붙이는 것이 추이성⁠(transitivity)⁠이고, 두 경로 사이의 연속적인 변형이 '같음의 증명들 사이의 같음'입니다. 2009년 그는 이 해석을 단체 집합⁠(set)⁠이라는 대상으로 엄밀하게 만든 모형을 내놓았습니다. 이것이 호모토피 타입 이론⁠(homotopy type theory)⁠의 출발점입니다.

이 모형에서 참이 되는 새 공리⁠(axiom)⁠가 일가성 공리입니다(위의 식). 타입들의 모임인 우주 $\mathcal{U}$ 안에서 두 타입 $A$, $B$가 같다는 것과 둘 사이에 동치(서로 되돌릴 수 있는 대응)가 있다는 것이 동치라는 말입니다. 수학자들은 늘 구조가 같은 두 대상을 같은 것처럼 다룹니다. 원소에 이름표만 달리 붙인 두 군은 같은 군으로 여기지요. 전통적인 집합론⁠(set theory)⁠에서 이것은 말버릇일 뿐 정리가 아닙니다. 일가성 공리 아래에서는 그것이 정리가 됩니다. 동치인 두 타입은 같으므로, 한쪽에서 증명한 모든 성질이 다른 쪽으로 자동으로 옮겨 갑니다. 대가도 있습니다. 참과 거짓 두 원소만 가진 타입 $\mathbf{2}$는 자기 자신과의 동치가 두 개(그대로 두기와 서로 바꾸기)이므로, $\mathbf{2} = \mathbf{2}$의 증명도 서로 다른 것이 두 개 있습니다. 그래서 '같음의 증명은 많아야 하나'라는, 타입 이론에 흔히 덧붙이던 원리는 이 공리와 함께 쓸 수 없습니다.

그는 타입을 '같음의 복잡도'로 층을 나누었습니다. 원소가 있고 모든 원소가 서로 같은(축약 가능한) 타입이 맨 아래에 있고, 원소가 많아야 하나인 타입이 '명제', 두 원소 사이의 같음이 명제인 타입이 '집합', 그 위로 준군, 2-준군이 이어집니다. 전통적인 수학은 대부분 명제와 집합의 층에서 일어나고, 호모토피 이론은 그 위층들을 다룹니다. 이렇게 보면 논리(명제), 집합론(집합), 호모토피 이론(준군과 그 위)이 한 틀 안의 서로 다른 층이 됩니다. 함수⁠(function)⁠의 같음이 모든 점에서의 값이 같다는 것과 동치라는 외연성도 일가성 공리에서 정리로 따라 나온다는 것을 그가 증명했습니다.

2010년 그는 증명 보조기 Coq로 이 기초 위의 수학 라이브러리를 직접 쓰기 시작했고, 2012–13년 프린스턴 고등연구소에서 티에리 코캉, 스티브 아워디와 함께 일가 기초론 특별 연도를 열었습니다. 모인 수학자와 컴퓨터 과학자들이 몇 달 동안 함께 쓴 책 『호모토피 타입 이론』(2013)은 저자 이름 대신 '일가 기초론 프로그램'을 내걸었습니다. 일가성 공리가 계산으로 어떤 뜻을 갖는지는 한동안 열린 문제였는데, 2010년대 중반 코캉 등이 입방 타입 이론으로 이 공리가 계산되는 체계를 내놓았습니다. 그는 2017년 프린스턴에서 51세로 세상을 떠났습니다. 오늘날 수학자들의 대규모 형식화 작업은 대부분 일가성 공리 없이 린 같은 도구 위에서 이루어지고 있어, 그의 기초론이 수학의 일상 도구가 될지는 아직 지켜보아야 합니다. 그러나 수학의 증명을 기계로 확인하는 일을 주류 수학자들의 관심사로 끌어낸 것은 그의 분명한 공헌입니다.

이어지는 곳. 같음을 경로로 읽는 해석과 일가성 공리의 결과들은 호모토피 타입 이론에서, 그 바탕인 같음 타입⁠(identity type)⁠과 의존 타입⁠(dependent type)⁠은 의존 타입과 마르틴뢰프에서 볼 수 있습니다. 구조가 같으면 같은 것으로 다룬다는 생각의 범주론⁠(category theory)⁠ 쪽 표현은 범주론과 요네다 보조정리⁠(Yoneda lemma)⁠에 있고, 모티브의 뿌리는 그로텐디크에 있습니다. 컴퓨터가 증명을 확인하는 실제 도구는 증명 보조기에서, 공간의 모양을 재는 기본 개념은 위상수학에서 출발합니다.

관계.

• 영향을 받음 알렉산더 그로텐디크 — 그로텐디크가 1960년대에 구상한 '모티브', 곧 여러 코호몰로지 이론 밑에 깔린 하나의 이론을 모티브 코호몰로지로 상당 부분 실현했습니다.
• 영향을 받음 페르 마르틴뢰프 — 마르틴뢰프 타입 이론의 같음 타입을 공간의 경로로 해석하는 모형을 만들고, 거기에 일가성 공리를 더해 새 기초론을 제안했습니다.

연표.

• 1991년 카프라노프와 ∞-준군과 호모토피 타입에 관한 논문을 내다
• 1992년 하버드 대학에서 카즈단의 지도로 박사 학위를 받다
• 1996년 밀너 추측의 증명을 발표하다
• 1998년 심프슨이 카프라노프와 쓴 논문의 주요 정리에 반례를 내놓다
• 1999년 모렐과 대수다양체의 호모토피 이론(𝔸¹-호모토피 이론)을 발표하다
• 2002년 필즈상을 받고 프린스턴 고등연구소 교수가 되다
• 2009년 마르틴뢰프 타입 이론을 단체 집합으로 해석하는 일가 모형을 만들다
• 2010년 증명 보조기 Coq로 일가 기초론 라이브러리를 쓰기 시작하다
• 2011년 블로흐–가토 추측의 증명을 마무리해 발표하다
• 2012년 고등연구소에서 일가 기초론 특별 연도(2012–13)를 열다
• 2013년 참가자들이 함께 쓴 『호모토피 타입 이론』 책이 나오다