在Dummit and Foote抽象代数中发现一个Bug

Finding a bug in Dummit and Foote's Abstract Algebra

我在Recurse Center的第二周，尝试用Rocq形式化Dummit and Foote的《Abstract Algebra》教材。第一个证明练习就让我卡住了——命题本身是错的。这让我既沮丧又兴奋。书中声称“函数是单射当且仅当它有左逆”，但在空集A到非空集B的情况下，函数是单射的，却不存在从B到A的函数，因此没有左逆。用Rocq推导时，我不断碰壁，最终意识到命题不成立。后来查勘误表，发现这个问题早已被指出。这次经历让我体会到形式化验证如何帮助发现传统笔算中容易忽略的边界情况。