Lean으로 콜라츠 추측 반증했다는 증명, 커널 버그로 판명나며 프루프 오브젝트 논쟁 재점화

오케이 이거 OS 커널 얘기가 아니라 증명 보조도구(proof assistant) 커널 얘기임. 클릭해서 마이크로커널 논쟁 기대했는데 아니었음. 근데 비유는 맞더라, 디바이스 드라이버 버그 하나로 커널 패닉 나거나 루트 뚫리는 거랑 똑같은 상황임.

OS 커널에서 흔히 하는 '성능 때문에 다 커널에 넣어야 한다'는 변명은 증명 보조도구에는 안 통함. 여긴 성능 문제가 아니라 신뢰성 문제라서.

'커널'이라는 단어를 자기들 맘대로 정의해서 쓰는 신조어일 뿐임. 글에 나오는 '하니스'도 뭔 뜻인지 클릭도 안 했음.

커널은 절대적으로 신뢰하는 핵심부고 뭐가 증명된 사실인지 최종 결정하는 애임. 그 위에는 유저스페이스 툴링처럼 신뢰 안 해도 되는 게 잔뜩 쌓임. 커널 버그가 터지면 최악의 경우 False가 정리(theorem)로 인정되고 그럼 모든 게 다 정리가 되어버림. HOL Light 커널은 fusion.ml 파일 하나에 500줄밖에 안 되는데 Lean4 커널은 C++로 여러 파일에 퍼져 있음.

이 글의 진짜 논점은 커널에 뭘 넣냐 마냐가 아니라 고전논리 대 직관논리 논쟁이라고 봄. Isabelle은 고전논리+집합론 쓰는데, 그 방식으로 재귀함수를 'honistly toil'해서 만들면 결국 어떤 성질을 가진 쌍들의 집합이 존재한다는 걸 비구성적으로 증명한 것뿐이라 구체적으로 계산해보기 힘듦. Coq 같은 직관논리는 함수가 실제로 컴퓨터에서 돌아가는 절차라서 다름.

Lean 버그 포스트모템 링크 있음, leodemoura 블로그에 올라옴.

포스트모템 보니까 이제 Nanoda를 매일 돌려서 추적한다는데, 이번 버그는 잡았겠지만 앞으로는 어떤 모델이 증명 체커 배포판 자체를 해킹하는 게 원하는 증명 얻는 제일 쉬운 방법이라고 생각할 수도 있음. 그게 커널 건전성 버그보다 더 흔해질 수도 있다고 봄.

Metamath는 재귀 정의를 고차함수 하나로 팩터링해서 처리함, 하스켈의 fix 함수 같은 lazy fixpoint 방식임. df-rdg랑 df-seq 보면 초한재귀랑 정초재귀 둘 다 되게 좀 더 일반화되어 있음.

proof object냐 proof type이냐 논쟁 자체가 좀 상아탑스러운 얘기 아님? 결국 컴퓨터가 처리하는 데이터일 뿐인데 두 개념을 구분해놓고 뭐가 낫냐 싸우는 거임. 그리고 proof type 쓴다고 증명을 버리는 것도 아님, 이론 파일 열어보면 그대로 다 있어서 다시 체크할 수 있음.