Formalizing Abstract Algebra in Rocq Uncovers a Bug in Dummit and Foote

Finding a bug in Dummit and Foote's Abstract Algebra

During his second week at the Recurse Center, Ben Kallus attempted to formalize Dummit and Foote's Abstract Algebra textbook in the Rocq proof assistant. He discovered that the first proof exercise—proving a function is injective if and only if it has a left inverse—is false due to a corner case involving the empty set. The bug is already listed in the book's errata, but Kallus's experience highlights the value of formal verification in catching subtle mathematical errors.