Hacker News 2026.03.31 25

수학 증명을 컴퓨터로 검증하는 시대, 이게 정말 좋은 걸까?

수학자들 사이에서 벌어지고 있는 조용한 논쟁

수학이라는 학문의 핵심은 "증명"이에요. 어떤 명제가 참이라는 걸 논리적으로 빈틈없이 보여주는 거죠. 수천 년 동안 수학자들은 종이와 펜으로, 그리고 동료 수학자들의 검토(피어 리뷰)를 통해 증명의 정확성을 확인해왔어요. 그런데 최근 몇 년 사이에 "형식 증명(formal proof)"이라는 새로운 흐름이 수학계를 흔들고 있어요.

형식 증명이 뭐냐면, 수학 증명을 컴퓨터가 이해할 수 있는 형식 언어로 작성하고, 소프트웨어가 한 줄 한 줄 논리적 오류가 없는지 자동으로 검증하는 거예요. 프로그래밍으로 비유하면, 수학 증명에 "컴파일러"를 도입한 셈이에요. 코드에 문법 오류가 있으면 컴파일러가 잡아주듯, 증명에 논리적 빈틈이 있으면 형식 검증 도구가 잡아주는 거죠.

이 분야에서 가장 많이 쓰이는 도구가 Lean이라는 증명 보조 언어(proof assistant)예요. 마이크로소프트 리서치에서 개발했는데, 최근 몇 년 사이에 수학계에서 폭발적으로 채택이 늘었어요. 2023년에 필즈 메달 수상자인 테렌스 타오(Terence Tao)가 자신의 논문을 Lean으로 형식화하는 프로젝트를 진행하면서 더 주목받았고요.

형식 증명이 해결하는 실제 문제

사실 형식 증명이 필요한 이유가 있어요. 수학계에는 "발표된 증명에 오류가 있었다"는 사례가 드물지 않거든요. 유명한 예로, 1999년에 토머스 헤일스(Thomas Hales)가 케플러 추측을 증명했는데, 피어 리뷰어들이 4년 동안 검토하고도 "99% 확신하지만 완전히 확인하지는 못했다"고 밝힌 일이 있어요. 증명이 300페이지에 달하는 방대한 분량이었거든요. 결국 헤일스는 Flyspeck 프로젝트를 통해 이 증명을 형식 검증으로 완전히 확인했는데, 이 작업에만 10년이 더 걸렸어요.

현대 수학은 점점 더 복잡해지고 전문화되고 있어서, 한 사람의 증명을 다른 사람이 완전히 검증하기가 갈수록 어려워지고 있어요. 분야가 너무 세분화돼서 해당 분야 전문가가 전 세계에 몇 명 없는 경우도 있고요. 이런 상황에서 컴퓨터가 형식적 검증을 대신해줄 수 있다면, 수학의 신뢰성이 한 단계 올라갈 수 있다는 주장이에요.

그런데 반대 의견도 만만치 않아요

형식 증명에 대한 비판은 크게 두 가지예요.

첫째, "증명의 본질이 검증이 아니라 이해"라는 관점이에요. 수학자들이 증명을 쓰는 이유는 단순히 "이 명제가 참이다"를 확인하려는 게 아니에요. 증명 과정에서 왜 그런지, 어떤 구조가 숨어 있는지를 이해하고, 그 통찰을 다른 수학자들과 공유하려는 거거든요. 그런데 형식 증명은 이런 직관과 통찰을 기계적 논리 단계로 분해해버리기 때문에, 정작 중요한 "이해"가 사라질 수 있다는 거예요. 마치 소설을 문법 검사기에 돌리면 문법 오류는 잡을 수 있지만, 그 소설이 좋은 소설인지는 알 수 없는 것처럼요.

둘째, 비용 대비 효과 문제예요. 현재 기준으로, 일반적인 수학 증명을 Lean 같은 도구로 형식화하는 데는 원래 증명을 쓰는 것보다 몇 배에서 수십 배 더 많은 시간이 걸려요. 연구자의 시간은 한정돼 있는데, 이미 높은 확신이 있는 증명을 형식화하는 데 그 시간을 쏟는 게 과연 합리적인가 하는 의문이죠. 새로운 정리를 발견하는 데 쓰는 게 더 가치 있지 않겠냐는 거예요.

개발자의 눈으로 보면

이 논쟁이 개발자에게 흥미로운 이유는, 우리 업계에서도 비슷한 논쟁이 있기 때문이에요.

타입 시스템을 생각해보세요. JavaScript에서 TypeScript로의 전환이 딱 이 논쟁과 닮았어요. "타입 없이도 잘 돌아가는 코드인데 왜 타입을 일일이 달아야 하나"라는 반발과, "타입이 있어야 대규모 프로젝트에서 안전하다"는 주장이 부딪혔잖아요. 결국 업계는 "필요한 곳에 적절히" 쓰는 방향으로 수렴했고요.

형식 검증(formal verification)도 소프트웨어 분야에서는 이미 쓰이고 있어요. AWS는 S3와 DynamoDB의 핵심 알고리즘을 TLA+로 형식 검증하고 있고, CompCert이라는 형식 검증된 C 컴파일러도 있어요. 하지만 모든 코드를 형식 검증하지는 않죠. 안전이 극도로 중요한 핵심 부분에만 적용해요. 비행기 제어 소프트웨어나 암호화 라이브러리처럼요.

수학도 결국 비슷한 방향으로 갈 가능성이 높아요. 모든 증명을 형식화하는 게 아니라, 특히 복잡하거나 논쟁이 있는 증명, 다른 많은 결과의 기반이 되는 핵심 정리에 형식 검증을 적용하는 방식으로요.

Lean과 증명 보조 도구 생태계

개발자 관점에서 Lean은 그 자체로 흥미로운 프로그래밍 언어이기도 해요. Lean 4는 범용 함수형 프로그래밍 언어로도 쓸 수 있도록 설계됐거든요. 의존 타입(dependent type)이라는 강력한 타입 시스템을 가지고 있어서, "이 함수가 반환하는 리스트의 길이는 입력 리스트의 길이와 같다"는 것까지 타입으로 표현하고 컴파일 타임에 검증할 수 있어요.

Lean 외에도 Coq, Agda, Isabelle 같은 증명 보조 도구들이 있어요. 각각 장단점이 있는데, 최근에는 Lean의 사용자 친화적인 문법과 활발한 커뮤니티(Mathlib 프로젝트) 덕분에 Lean이 가장 빠르게 성장하고 있어요.

최근에는 AI를 활용해 형식 증명을 자동으로 생성하려는 연구도 활발해요. Google DeepMind의 AlphaProof가 국제 수학 올림피아드 문제를 Lean으로 풀어낸 사례가 있었죠. AI가 증명의 "지루한 부분"을 자동화해줄 수 있다면, 형식 증명의 비용 문제가 크게 완화될 수 있어요.

한국 개발자에게 주는 시사점

당장 실무에 Lean을 도입할 일은 없겠지만, 이 논쟁에서 배울 수 있는 건 있어요. "얼마나 엄밀하게 검증할 것인가"는 소프트웨어 개발에서도 매일 마주하는 질문이거든요. 테스트를 어디까지 작성할 것인가, 타입을 얼마나 엄격하게 쓸 것인가, 코드 리뷰를 얼마나 꼼꼼하게 할 것인가. 이런 질문들의 답은 항상 "상황에 따라" 다르고, 비용과 이점 사이의 균형을 찾는 게 중요하다는 점에서 수학계의 이 논쟁과 본질이 같아요.

함수형 프로그래밍이나 타입 이론에 관심이 있는 분이라면, Lean 4를 한번 들여다보는 것도 추천해요. 프로그래밍 언어가 "코드의 정확성"을 보장하기 위해 얼마나 멀리 갈 수 있는지를 보여주는 극단적인 사례거든요.