A mathematical error in the widely used textbook Dummit and Foote's Abstract Algebra has been discovered using Rocq, an interactive formal proof assistant. The theorem prover identified the flaw by formally verifying the text's proofs, catching a mistake that had previously gone unnoticed by mathematicians. This achievement highlights the growing capability of automated verification tools to validate and correct complex mathematical literature.