Dummit and Foote의 추상대수 교과서에서 버그를 찾다

Finding a bug in Dummit and Foote's Abstract Algebra

Recurse Center에서의 두 번째 주에, 저자는 Dummit and Foote의 'Abstract Algebra' 교과서를 Rocq로 형식화하려고 시도했습니다. 첫 번째 증명 연습 문제에서 명제가 실제로는 거짓임을 발견했습니다. 공집합 도메인과 비어 있지 않은 공역을 가진 함수는 단사적이지만 왼쪽 역함수를 가질 수 없다는 반례를 제시합니다. 이는 종이로 연습할 때는 놓치기 쉬운 경계 사례로, 형식적 증명 도구를 사용함으로써 드러났습니다. 저자는 이 오류가 이미 교과서의 정오표에 등재되어 있음을 확인했습니다.