Lean을 사용한 페르마의 마지막 정리 형식화: 협업 오픈소스 프로젝트

케빈 버자드가 이끄는 국제적 협업 프로젝트는 Lean 정리 증명기를 사용하여 페르마의 마지막 정리를 공식적으로 증명하는 야심찬 작업을 수행하고 있습니다. 영국 공학 및 물리 과학 연구위원회의 지원을 받고 임페리얼 칼리지 런던에서 주관하는 이 프로젝트는 컴퓨터를 이용한 증명 검증을 통해 수학에서의 형식화 및 자동 검증의 가능성을 탐구하며 미래 연구에 영향을 미칩니다.