페르마는 자신의 마지막 정리에 대한 증명을 노트 여백에 담기에는 너무 커서 가지고 있다고 주장했습니다. 최근 Lean 코드에서 페르마의 마지막 정리를 형식화하는 과정에서 버그가 발생했습니다. 이 버그는 코드 검토를 위한 AI 실험 중에 발견되었습니다. 이 문제는 Lean의 문자열 슬라이싱 함수가 매우 큰 위치를 처리하는 방식에 영향을 미칩니다. 논리적으로는 빈 문자열을 반환해야 하지만, 컴파일된 코드는 원본 문자열을 반환합니다. 이 불일치는 모순을 야기합니다. 정리 증명기가 빈 문자열이 비어 있지 않은 문자열과 같다고 잘못 결론 내립니다. 이는 페르마의 마지막 정리를 포함한 모든 명제를 증명할 수 있게 합니다. Lean 팀은 보고 후 놀라울 정도로 신속하게 버그를 수정했습니다. 이 수정에는 메모리 안전성과 의미론적 불일치 모두를 해결하는 것이 포함되었습니다. 기계 검증된 증명은 큰 신뢰를 제공하지만, 정리 증명기 문제로 인해 취약점이 발생할 수 있습니다. 따라서 Lean 증명의 신중한 검증이 필수적입니다.