네 가지 정리 증명기의 이야기 — Isabelle/HOL, Lean, HOL4, Agda 비교
저자는 네 정리 증명기에서 유클리드 방식으로 소수의 무한성을 증명하고, 자동화·증명 과정 확인·정리 검색·사용 경험을 비교합니다. Isabelle/HOL과 HOL4는 자동화가 강하고, Agda는 증명 과정을 명시적으로 드러내지만 수작업이 많다는 평가입니다.
저자는 네 정리 증명기에서 유클리드 방식으로 소수의 무한성을 증명하고, 자동화·증명 과정 확인·정리 검색·사용 경험을 비교합니다. Isabelle/HOL과 HOL4는 자동화가 강하고, Agda는 증명 과정을 명시적으로 드러내지만 수작업이 많다는 평가입니다.