Dummit & Foote『Abstract Algebra』にバグを発見
Finding a bug in Dummit and Foote's Abstract Algebra
Recurse Centerでの2週目、Ben Kallus氏はRocqでDummit & Footeの『Abstract Algebra』の形式化に挑戦。最初の証明演習で、命題が偽であることに気づく。Aが空集合でBが非空の場合、関数は単射だが左逆写像を持たない。紙上では気づきにくいコーナーケースを、証明支援系が明らかにした。書籍の正誤表に既に記載されていた。
Rocqを使っていたからこそ、このコーナーケースを思いついたでしょう。紙でこの演習をしていたら、おそらく気づかなかったはずです。