수학과 Lean에 대한 여러 생각

증명 언어인 Lean을 이용해 수학 증명 데이터셋을 만들고, 궁극적으로 AI를 학습시켜 수학 문제를 풀게 만드는 흐름이 유행이 된 것 같습니다. 저는 수학 마니아이기 때문에 이것을 최근 2년간 지켜보고 있었는데, 이 움직임이 최근 가속화되었다는 인상을 받았습니다. Terrence Tao가 Lean 관련 기여를 예전부터 많이 해왔었고(GitHub에 재미있는 프로젝트들이 많습니다), 요즘은 임페리얼 칼리지 런던에서 Lean으로 페르마의 마지막 정리(Fermat’s Last Theorem, FLT)를 증명하려는 프로젝트¹를 찾아냈는데, 설계도 페이지²를 보면 FLT 증명이 실제로 어떻게 이루어지는지 구경해볼 수도 있습니다. 최근 한국에서 열린 PLDI'25에서 Leonardo de Moura의 Lean 키노트³에서 Lean 프로젝트의 소개도 좋은 자료입니다.

나중에는 Lean으로 작성된 교과서로 수학을 배우게 될지도 모를 일입니다. 다른 증명 언어인 Coq으로 논리학 등을 배울 수 있는 Software Foundations⁴ 교과서와 같은 오래된 예시가 있습니다. 옛날에 저는 그 교과서를 읽을 때 이상한 기호가 많이 등장하는 수식을 NeoVim과 같은 텍스트 에디터로 적는 진입장벽을 뚫지 못해서 중간에 그만둔 경험이 있습니다. 하지만 사람이 친숙하게 쓸 수 있도록 사용성만 개선한다면 정말 좋은 방향이라 생각합니다. 수학 지식의 공유 방법이 증명 언어 중심으로 전환된다면 수학에 대한 접근성이 훨씬 좋아질 것이기 때문입니다. 검색 엔진에서도 수식의 색인이 훨씬 잘 될 것이고, 증명의 매 단계를 하나 하나 라이브러리를 따라가듯 뜯어볼 수 있을 것이고, 잘못 작성된 증명을 증명 언어 실행을 통해 바로 확인이 가능한 부분 등 수많은 장점이 존재합니다.

한편, 증명 언어로 만든 수학 증명 데이터셋을 바탕으로 개발된 AI가 수학 문제를 사람보다 잘 풀게 된다면 어려운 수학 문제를 손으로 풀던 사람들의 즐거움을 뺏을 수도 있습니다. 이미 프로그래밍에서 AI가 많은 편리함을 제공함과 동시에 코드를 하나하나 작성하는 즐거움을 뺏어간 선례를 보면 알 수 있습니다. 동시에 AI를 잘 활용하는 즐거움도 생겨날 것이고, 던순히 패러다임 전환에 대한 반감이 아니냐 생각할 수도 있지만, 그래도 씁쓸한 것은 어쩔 수 없습니다.