Lean을 사용한 증명이 잘못될 위험은 매우 적음. 그러나 Lean의 버그와 무관하게, 소프트웨어 검증 및 수학에서 알려진 문제인 결론을 주의 깊게 읽고 실제로 증명된 것이 맞는지 확인해야 함.
이번 사례는 어려운 증명의 상태를 해결하기 위해 증명 도우미를 사용한 첫 번째 사례로 보임. 이전에는 신뢰할 수 없는 소프트웨어로 처리된 대규모 계산 요소가 포함된 기존 증명을 검증한 프로젝트가 있었지만, 이번 사례는 결과의 인식론적 지위가 수학계에서 불확실했던 첫 번째 사례임.
Coq와 Lean의 근본적인 차이점과 동일한 종류의 논리에서 작동하는지 여부에 대해 궁금증이 제기됨. 관련 토론에서는 이해하기 어려운 내용들이 언급됨.
Lean 지지자들은 Lean이 우수한 증명 방법이라는 점을 너무 강하게 사용하는 경향이 있음. Lean은 대안적인 증명 방법일 뿐이며, 프로그래밍 언어 및 시스템으로서 자체 버그가 있고 다른 사람이 작성한 다양한 라이브러리 스택에 크게 의존함.
Lean이 증명이 좋다고 말했다는 표현보다는, 작성된 증명이 인간 수학자에 의해 검증되었고 증명이 Lean으로 변환되어 거기서도 검증되었다는 표현이 더 정확하고 솔직할 것임. Lean이 유일하고 황금같은 검증을 제공한다는 설명은 정확하지 않거나 그렇게 말하는 설명을 보지 못했음.
"New Foundations" 집합론 공식화가 다른 공식화에 비해 특별하거나 새로운 점에 대한 대략적인 설명을 수학 학부생이나 엔지니어링 전문가가 읽을 수 있는 형태로 요청함.
이러한 접근이 결국 협업 증명과 '버그 수정'으로 이어져 수학을 GitHub의 코드와 유사한 프로세스로 만들지 궁금해 함.
괴델의 정리에 따르면 충분히 강력한 모든 시스템은 자신의 일관성을 보여줄 수 없다고 하는데, 이에 대해 질문함.
mathlib 프로젝트를 계속 따라가고 싶지만 시간이 없음. 매우 소극적인 방식으로 참여할 수 있는 방법이 있는지 궁금해 함.
Hacker News 의견