Lean, 정말 수학 형식화의 '정답'일까?

Lean은 훌륭한 도구와 활발한 커뮤니티를 통해 수학 형식화 분야에서 두각을 나타내고 있다. 하지만, AUTOMATH와 같은 이전 기술의 한계를 극복해야 한다. 특히, Lean은 가독성(Legibility) 측면에서 개선의 여지가 있으며, 종종 의존적 타입(Dependent Types)으로 인해 초보자가 어려움을 겪을 수 있다는 지적이 있다. 또한, Lean의 자동화 기능(Automation)은 Isabelle에 비해 부족하다는 평가도 존재한다.

Isabelle은 Lean보다 강력한 자동화 기능(Automation)을 제공하며, 특히 Sledgehammer를 통해 AI 기반 증명 도구와의 연동을 지원한다. 또한, Isabelle은 가독성(Legibility)을 중시하여 인간이 이해하기 쉬운 증명 텍스트를 제공한다. 이러한 특징은 AI가 생성한 증명을 검토하고 개선하는 데 유용하며, AI 기반 증명 도구의 발전에 따라 Isabelle의 중요성이 더욱 커질 것으로 예상된다.

프로포지션 애즈 타입(Propositions as Types)은 논리 기호와 타입 생성자를 연결하는 매력적인 이론이지만, 형식화 분야의 유일한 접근 방식은 아니다. LCF와 같은 다른 접근 방식은 증명 객체(Proof Objects)를 사용하지 않아 메모리 사용량을 줄이고, ML 언어(ML Language)를 통해 안전한 증명 검증을 가능하게 한다. 이러한 LCF의 장점은 프로포지션 애즈 타입 접근 방식에서 간과될 수 있다는 비판이 제기된다.

수학 형식화는 Lean의 등장 이전부터 다양한 시도를 거쳐 발전해 왔다. AUTOMATH는 1968년에 등장하여 Lean과 유사한 기능을 제공했지만, 표기법과 자동화 부족으로 인해 널리 사용되지 못했다. HOL Light와 Isabelle은 다양한 수학적 결과를 형식화하는 데 성공했으며, Mizar는 방대한 수학 라이브러리를 구축했다. 이러한 역사적 맥락을 이해하는 것은 Lean의 현재 위치를 정확하게 평가하는 데 중요하다.