네 가지 정리 증명기 이야기: Isabelle/HOL, Lean, HOL4, Agda에 대한 (적당히) 주관적인 비교

소수의 무한성에 대한 유클리드 증명을 네 시스템으로 형식화해 사용자 경험을 비교함. 도구별 숙련도가 다른 상태에서 진행한 개인적 평가이므로, 공정한 성능 비교로 보기는 어려움 이번 구현 경험에서는 Isabelle/HOL과 HOL4의 자동화 및 정리 검색이 강점이었음. Lean은 그 뒤를 이었고, Agda는 보조정리를 직접 찾고 증명 항을 수작업으로 구성하는 부담이 컸음 상호작용성과 증명의 직접 제어는 다른 평가 축임. Lean과 Isabelle/HOL은 입력 중 상태와 중간 단계를 보기 좋았지만, Agda는 명시적인 증명 항 덕분에 원하는 조작을 정확하게 수행하고 동작을 예측하기 쉬웠음 Agda의 구성적 증명은 임의의 수보다 큰 소수를 실제로 계산할 수 있었음. 다만 이 구현에서는 입력 8에 대한 결과 19를 얻는 데 40초가 걸렸으며, 소수 판정 절차까지 직접 만드는 비용도 따랐음 개인적 종합 선택은 HOL4였음. 강력한 기능과 독특한 REPL 기반 작업 방식이 즐거웠으며, 특정 도구에 머무르기보다 논리적 기반과 상호작용 방식이 다른 증명기를 사용해 볼 것을 권함 비교 과제와 전제 네 도구 모두 수학을 컴퓨터로 형식화하는 정리 증명 시스템임 Lean과 Agda는 의존 타입과 Curry-Howard 대응을 활용해 복잡한 타입 시스템으로 정리를 증명함 Isabelle/HOL과 HOL4는 작은 증명 커널의 기본 규칙으로 모든 증명을 구성하는 LCF 방식을 사용함 공통 과제는 유클리드의 소수 무한성 증명을 형식화해, “모든 자연수 n에 대해 n보다 큰 소수가 존재한다”를 보이는 것임 증명 구조가 대체로 비슷해 사용자 경험이 주요 차이가 됨 실험 전에는 Isabelle/HOL과 Agda에 가장 익숙했고, HOL4와 Lean은 비교 과정에서 일부 학습함 평가 범주와 순위는 주관적이며, 구현한 증명도 완성도 높은 모범 답안으로 전제하지 않음 상호작용성과 편집 환경 Isabelle/HOL과 Lean은 상호작용성이 높은 편임. 입력할 때 상태가 실시간으로 갱신되고, 구조화된 증명을 커서로 따라가며 중간 단계를 확인할 수 있음 HOL4와 Agda는 완성된 증명의 내부를 살펴보려면 직접 분해해야 함. 다만 두 도구 모두 작업 중 현재 상태와 관련 정보를 확인할 수 있음 편집 환경은 도구마다 다름 Lean은 다른 편집기용 모드도 있지만 VSCode 사용을 강하게 권장하며, Isabelle/HOL은 전용 jEdit 환경을 사실상 사...