수학적 증명을 컴퓨터로 형식화하고 검증하는 '정리 증명 시스템(Theorem Proving System)' 분야에서 대표적인 네 가지 도구인 Isabelle/HOL, Lean, HOL4, Agda의 사용자 경험을 비교한 보고서가 발표되었습니다. 유클리드의 소수 무한성 증명을 공통 과제로 삼아 각 시스템의 특징과 장단점을 분석했으며, 특히 자동화 수준과 상호작용 방식에서 뚜렷한 차이를 보였습니다.
이번 비교에서는 Isabelle/HOL과 HOL4가 높은 자동화 수준과 강력한 정리 검색 기능을 강점으로 내세웠습니다. Isabelle/HOL의 'sledgehammer'와 HOL4의 'HolyHammer'는 외부 솔버를 활용해 복잡한 증명 단계를 자동 처리하며 수작업 부담을 줄여주었습니다. 반면 Lean은 중간 정도의 자동화를, Agda는 수작업에 가까운 증명 구성 방식을 요구했습니다. 상호작용성 측면에서는 Isabelle/HOL과 Lean이 실시간 상태 갱신과 중간 단계 확인이 용이해 높은 평가를 받았고, HOL4는 REPL 기반의 독특한 작업 방식이 인상적이었다는 평가입니다. Agda는 명시적인 증명 항 덕분에 원하는 조작을 정확히 수행할 수 있었지만, 자동화 부족으로 인한 작업 부담이 컸습니다. 특히 Agda의 구성적 증명(constructive proof)은 단순히 존재를 증명하는 것을 넘어, 주어진 수보다 큰 소수를 실제로 계산해 반환하는 등 계산 가능성을 보여주었지만, 계산 속도는 느렸습니다.
이러한 정리 증명 시스템은 소프트웨어의 정확성 검증, 암호학, 인공지능(AI) 등 고신뢰성이 요구되는 분야에서 오류를 줄이고 신뢰도를 높이는 데 필수적인 도구로 자리 잡고 있습니다. 각 시스템이 제공하는 자동화 수준, 논리적 기반(고전 논리 vs. 구성적 논리), 그리고 사용자 인터페이스의 차이는 개발자가 어떤 종류의 증명을 다루고 어떤 작업 흐름을 선호하는지에 따라 선택의 폭을 넓혀줍니다. 특히 Agda처럼 계산 가능한 증명을 제공하는 방식은 이론적 증명을 실제 실행 가능한 코드로 연결하는 가능성을 제시하며, 이는 향후 더욱 안전하고 검증 가능한 시스템 개발에 중요한 시사점을 제공할 것입니다.