- 소수의 무한성에 대한 유클리드 증명을 네 시스템으로 형식화해 사용자 경험을 비교함. 도구별 숙련도가 다른 상태에서 진행한 개인적 평가이므로, 공정한 성능 비교로 보기는 어려움
- 이번 구현 경험에서는 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 환경을 사실상 사용하게 함
- HOL4는 Emacs 또는 Vim 모드에서 실행 중인 REPL로 텍스트를 보내고 결과를 가져오는 방식이며, 이번 경험에서는 의외로 잘 작동함
- Agda는 Emacs 모드에서 파일 안의 상태를 갱신하고 증명 목표를 추가하는 방식으로 작업함
- 이번 경험에서 자동화 수준은 Isabelle/HOL과 HOL4가 높고, Lean은 중간, Agda는 낮았음
- Isabelle/HOL의 sledgehammer 는 SAT/SMT 및 여러 1차 논리 솔버 등 외부 증명 생성 방법을 호출함
- 풀 수는 있지만 번거로운 목표를 해결해 수작업을 줄여 주는 경우가 많음
- 생성된 증명은 해독하기 어려울 수 있음
- HOL4에도 대응 도구인 HolyHammer가 있지만, 비교를 작성하던 중 뒤늦게 알게 되어 실험에서는 활용하지 못함
- Isabelle/HOL과 HOL4는 자동 단순화와 증명 방법도 강력했음. 복잡한 가정을 작은 형태로 정리해 주지 않으면 다음 단계를 찾기 어려운 경우에 특히 유용함
- Lean의 simp와 grind 는 유용하지만 이번 경험에서는 일관성이 아쉬웠음
- simp는 Isabelle/HOL이나 HOL4만큼 생산적이지 않았음
- grind는 때때로 sledgehammer에 견줄 만큼 강력했지만, 단순해 보이는 목표를 해결하지 못하는 경우도 있었음
- 완전 해결과 부분 진행은 구분해야 함
- sledgehammer와 grind는 목표를 해결하지 못하면 진행 결과를 남기지 않는 방식임
- 세 도구의 simp, Isabelle/HOL의 auto, HOL4의 gvs는 일부만 처리하고 더 정리된 문맥을 남길 수 있음
- 이번 평가에서는 이런 부분 자동화가 더 중요했으며, Lean의 지원이 상대적으로 아쉬웠음
- 여러 방법을 시험하는 기능도 차이가 있음
- Isabelle/HOL은 try와 try0로 sledgehammer 포함 여부를 달리해 시도할 수 있음
- Lean은 try?, exact?, rw?를 제공함
- HOL4에서는 이에 대응하는 기능을 찾지 못함
- Agda는 자동화가 사실상 없었음. 함수 입력으로 계산할 수 있는 단순화 외에는 수작업으로 조정할 부분이 많아 작업 부담이 컸음
- Isabelle/HOL과 HOL4는 고전 논리에 기반하며, 배중률과 Hilbert의 엡실론을 공리로 채택해 선택 공리도 따름
- 배중률과 동치인 이중 부정 제거 같은 법칙을 자동 솔버가 자주 활용하므로, 이번 평가에서는 이런 기반이 자동화에 유리하게 느껴졌음
- Lean은 이론적으로 구성적이지만, 유용한 자동화 일부는 배중률을 요구함
- 고전적으로 사용하는 것이 일반적인 것으로 보고 이번 증명도 그 방식으로 작성함
- grind도 고전 논리 사용을 전제하며, 이번 경험에서는 존재 명제 등을 다루는 능력이 아쉬웠음
- Agda는 기본적으로 구성적이며, 이번 구현도 그 방식을 유지함
- 배중률로 소수 여부를 나누는 대신, 이를 결정할 소수 판정 알고리듬을 작성해야 했음
- 대신 완성된 증명에 수를 넣으면 그보다 큰 소수를 실제로 반환함
- Agda 증명의 실행 결과는 계산 가능성과 속도의 차이를 보여 줌
- 입력 0, 1, 2, 3에는 각각 2, 3, 7, 5를 즉시 반환함
- 입력 4와 5에는 각각 11과 7을 약 0.25초 만에 반환함
- 입력 6, 7, 8에는 각각 71, 61, 19를 반환했으며, 3초, 10초, 40초가 걸림
- 구성 과정에서 (n + 1)! + 1을 고려하므로 입력 8에서는 약 36만 규모의 수에 대해 소수 여부를 확인하게 됨
- 이 구성은 속도를 목표로 하지 않음. 계산 가능한 증명을 얻기 위해 배중률과 강력한 자동화를 포기할 가치가 있는지는 선택의 문제임
- 이번 비교의 개인적 선호는 LCF 방식임. 자동화에 더 잘 맞는다고 느꼈고, 고전 논리의 유용성을 고려하면 증명 항을 유지해야 할 필요성을 크게 느끼지 못함
- Isabelle/HOL과 HOL4는 이름뿐 아니라 명제의 형태로도 정리를 찾을 수 있어 편리했음
- Isabelle/HOL은 편집기 패널과 find_theorems를 제공함
- HOL4는 DB.find와 DB.match를 제공함
- 보조정리 이름을 몰라도 _ < SUC _ 같은 패턴으로 검색할 수 있음
- Lean의 leansearch와 loogle은 내장 기능이 아니며, 이번 경험에서는 앞선 두 도구보다 만족도가 낮았음
- exact?와 rw?가 가능한 해결책을 제안하지만, 패턴 기반 탐색만큼 유연하지는 않았음
- Agda에서는 대응 검색 기능 없이 표준 라이브러리의 적절한 부분을 직접 찾아야 했음
- 구현 규모는 다음과 같지만 동일 조건의 직접 비교는 아님
- Isabelle/HOL은 117줄, 증명 19개임
- Lean은 155줄, 증명 12개임
- HOL4는 190줄, 증명 16개임
- Agda는 264줄, 증명 45개이며 where 블록을 제외하면 29개임
- 나눗셈 관계는 네 도구 모두 어떤 몫을 곱하면 대상 수가 된다는 형태로 정의함
- Isabelle/HOL, Lean, HOL4에서는 존재 명제를 사용함
- Agda에서는 몫과 등식 증명을 필드로 가진 레코드를 사용하며, 약수 계산 관련 증명을 재작성하지 않기 위해 표준 라이브러리 정의를 활용함
- 대표 보조정리는 같은 수가 두 수를 나누면 그 차도 나눈다는 성질임
- Isabelle/HOL의 metis와 HOL4의 metis_tac는 나눗셈 정의와 곱셈의 뺄셈 분배 법칙을 주면 대부분을 해결함
- Lean은 두 존재 명제를 풀어 몫을 꺼내고, 새 몫을 q1 - q2로 지정한 뒤 grind [Nat.mul_sub]로 마무리함
- Agda도 몫의 차를 직접 지정하고 분배 법칙의 등식 증명을 구성함
- 이번에는 Lean 구현에 가장 많은 노력이 들었음. 보조정리 검색뿐 아니라 아직 문법을 익히는 중이었다는 조건도 영향을 줌
- 리스트 곱은 네 도구 모두 빈 리스트에서 1, 나머지는 첫 원소와 꼬리 리스트 곱의 곱으로 정의함
- Lean의 @[simp, grind] 표시는 자동 증명 방법이 정의를 활용하는 데 도움이 됨
- HOL4의 정의는 그 재귀 방정식 자체를 담은 prod_list_def 정리를 생성함
- 다음 핵심 성질은 리스트의 원소가 전체 리스트의 곱을 나눈다는 것임
- 네 증명 모두 원소가 리스트의 맨 앞에 있는지, 뒤쪽에 있는지를 나누어 처리함
- Isabelle/HOL은 귀납법, 경우 분리, 단순화로 짧게 처리하지만 구체적인 흐름이 암묵적임
- Lean은 원소 포함 관계를 직접 분해해야 해 비교적 길어짐
- HOL4도 귀납법과 단순화를 사용하지만, 주석 없이는 구조를 읽기 쉽지 않음
- Agda는 포함 관계를 패턴 매칭해 명시적이면서도 간결하게 작성할 수 있었고, Emacs의 C-c C-c 경우 분리 기능이 유용했음
- HOL4 증명은 SML 항이며, 전술을 함수로 조합함
- >>는 앞 전술이 만든 모든 하위 목표에 뒤 전술을 적용함
- >-는 하위 목표 하나에 적용함
- REPL에서 동적으로 증명을 구성한 뒤, 최종적으로 함수 조합을 맞춰 완성해야 함
- 증명에는 양수 리스트의 곱이 양수라는 성질과 각 원소가 전체 곱 이하라는 보조정리도 필요함
- 네 구현 모두 1보다 크고 약수가 1과 자기 자신뿐인 수로 소수를 정의함
- Agda는 이 두 조건의 증명을 레코드 필드로 보관함
- 0과 1은 소수가 아니고 2는 소수라는 기본 성질도 준비함
- Agda의 합성수 정의는 단순히 “소수가 아님”이 아니라, 더 작은 소인수와 그 증거를 포함하도록 구성함
- 이후 소인수가 필요할 때 바로 꺼내 쓸 수 있어 다루기 쉬움
- 소수 또는 합성수임을 결정하는 절차에는 유한 범위의 판정과 재귀가 필요함
- 다른 세 도구에서는 1보다 큰 비소수에 소인수가 존재한다는 보조정리를 강한 귀납법 계열의 방법으로 증명함
- Isabelle/HOL은 마지막 단계를 metis로 해결하며, 해당 단계는 sledgehammer로 찾음
- Lean은 비소수 조건의 중첩된 존재 명제와 논리곱을 풀고, 더 작은 약수에 귀납 가정을 적용함
- HOL4는 0 < k'에서 1 < k', k' ≤ k에서 k' < k로 넘어가는 단계를 각각 처리해야 해 번거로웠음
- 마지막 핵심 구성은 리스트 원소의 곱에 1을 더한 수를 이용해 리스트 밖의 소수를 찾는 것임
- 그 수가 소수라면 기존 원소들보다 크므로 리스트 밖에 있음
- 소수가 아니라면 소인수를 구함
- 그 소인수가 기존 리스트에 있었다면 리스트 곱과 곱에 1을 더한 수를 모두 나누므로, 두 수의 차인 1도 나누게 되어 모순임
- 이 단계에서 Isabelle/HOL의 증명은 가장 짧았지만 가장 읽기 어려웠음
- Lean과 HOL4는 더 장황하며, HOL4는 중첩 구조가 특히 복잡해짐
- grind와 1차 논리 솔버인 metis_tac가 많은 작업을 처리함
- Isabelle/HOL의 metis는 HOL4에서 이식된 도구임
- Agda는 이후 범위 리스트를 직접 구성해야 하는 사정에 맞춰 조금 다른 형태로 증명함
- 리스트 원소에 대해 1보다 큼이 아니라 양수 조건을 사용함
- 리스트 곱이 2보다 작은 경우를 별도로 처리하고, 소수 여부와 리스트 포함 여부를 결정 절차로 나눔
- 최종적으로 주어진 상한까지의 수를 담은 리스트 밖의 소수가 상한보다 크다는 것을 보임
- Isabelle/HOL, Lean, HOL4는 각자의 범위 리스트 기능을 활용함
- Agda는 리스트 생성 함수와 원소 포함 성질을 직접 증명하고, 판정 가능한 부등식에 대한 이중 부정 제거도 사용함
- 네 구현의 전체 코드도 공개되어 있어, 앞선 정의와 보조정리부터 최종 infinite_primes까지 확인할 수 있음
- 증명 발견의 용이성은 Isabelle/HOL, HOL4, Lean, Agda 순이었음
- sledgehammer와 두 LCF 도구의 정리 검색 기능이 강점임
- Lean의 try?도 관련 보조정리로 목표를 해결해 주는 경우가 많았음
- Agda는 온라인 .agda 파일을 뒤져 보조정리를 찾는 일이 불편했음
- 증명 조작의 용이성은 Agda, Lean, HOL4, Isabelle/HOL 순이었음
- Agda는 증명 항을 직접 작성하므로 지시한 대로 동작함
- Lean은 조작이 보수적이고 이름이 명시적이라 제어하기 좋았음
- HOL4는 qpat_assum 같은 패턴 기반 가정 선택 기능을 익힌 뒤에는 다루기 괜찮았음
- Isabelle/HOL은 단순화기가 정확히 원하는 것만 펼치도록 제어하기 어려웠음
- 즐거움은 HOL4, Lean, Isabelle/HOL, Agda 순이었음
- HOL4는 독특한 상호작용 방식과 강력한 기능이 함께 있어 가장 즐거웠음
- Lean을 배우는 과정도 즐거웠지만 불편한 순간이 있었음
- Isabelle/HOL은 이미 익숙해 신선함이 적었고, Agda는 소수 판정 절차와 타입 관련 조정이 부담스러웠음
- 짜증의 정도는 낮을수록 좋으며, 이번 경험에서는 Agda가 가장 높고 HOL4와 Lean이 공동 중간, Isabelle/HOL이 가장 낮았음
- Agda는 수동 증명 탐색과 반복적인 조정이 번거로웠음
- HOL4는 가정 조작과 단순화의 학습 부담, Lean은 까다로운 자동화가 불편했음
- Isabelle/HOL에 대한 평가는 기존 숙련도의 영향을 받음
- 예상 밖 동작으로 당황한 정도도 낮을수록 좋으며, 높은 쪽부터 HOL4, Lean, Isabelle/HOL, Agda 순이었음
- HOL4는 전술이 예상과 다르게 목표를 바꾸는 경우가 많았음
- Lean의 grind는 어려운 목표를 풀다가도 쉬운 목표를 놓쳐 납득하기 어려웠음
- Isabelle/HOL에서도 비슷한 일이 있었지만 대체로 괜찮았으며, Agda는 매우 예측 가능했음
- 개인적 종합 선택은 HOL4임. 학습 과정이 즐거웠고 시스템 자체가 흥미로웠음
- Lean도 즐거웠지만 이상하게 느껴지는 동작이 있어 약간 경계하게 됨. 가장 능숙한 도구는 업무에서도 사용하는 Isabelle/HOL임
- 가능하면 네 도구 모두, 적어도 기존과 다른 방식을 하나는 사용해 볼 것을 권함
- 의존 타입 기반 도구만 사용했다면 Isabelle/HOL이나 HOL4를, LCF 방식만 사용했다면 반대편을 시도할 수 있음
- Lean처럼 완전히 대화형으로 작업하는 도구만 사용했다면 HOL4나 Agda가 다른 경험을 제공함