약간의 배경을 덧붙이면, 리만 제타 함수의 홀수 값들이 무리수인지 여부는 정수론에서 오랜 미해결 문제였다. 아페리(Apéry)는 거의 50년 전에 제타(3)가 무리수임을 증명했다. 다른 값들이 무리수인지는 여전히 열린 질문으로 남아 있다. 그런데 일주일 전, 이름 없는 석사 과정 학생이 제타(5)가 무리수라고 주장하는 논문 예판을 Zenodo에 올렸다. 주목할 점은 다음과 같다. 첫째, 저자는 완전히 알려지지 않은 인물로 박사 학위가 없고 석사 학위는 있지만 수학 분야가 아니다. 둘째, arXiv보다 업로드 규정이 더 느슨한 Zenodo에 올라왔다. 셋째, 누군가 그의 증명을 형식 검증용 프로그래밍 언어인 Lean으로 형식화했다.

저자는 완전히 알려지지 않은 인물이다. 박사 학위가 없고, 석사 학위는 있지만 수학 분야가 아니다. arXiv보다 업로드 규정이 더 느슨한 Zenodo에 올라왔다. 누군가 그의 증명을 형식 검증용 프로그래밍 언어인 Lean으로 형식화했고 커뮤니티가 빠르게 검증했다. 그의 LinkedIn 프로필을 확인해 보니 석사 학위는 수학 분야인 것으로 보인다.

Lean 커널에는 어떤 버그가 존재하는가? 그리고 그 버그들이 알려져 있다면 왜 빠르게 수정되지 않는가?

얼마 전 콜라츠 추측의 증명이 주장됐고 Lean에서 검증됐지만, 알고 보니 Lean 자체의 버그를 악용한 것이었다. 세부 사항은 잘 모르지만 버그는 수정된 것으로 알며, 물론 다른 버그가 더 있을 수 있다.

참고로 Lean의 건전성(soundness) 버그는 사실상 어떤 명제든 증명하는 데 쓰일 수 있다. 버그를 보고한 사람은 콜라츠에 쓰는 것이 재미있을 것이라 생각했지만, 사실 1=0 같은 명백한 터무니없는 명제를 포함해 참이든 거짓이든 어떤 명제의 증명에도 사용될 수 있었을 것이다.