Fehler in Dummit und Footes „Abstract Algebra“ entdeckt

Finding a bug in Dummit and Foote's Abstract Algebra

Während seines Aufenthalts am Recurse Center versuchte Ben Kallus, das Lehrbuch „Abstract Algebra“ von Dummit und Foote mit dem Beweisassistenten Rocq zu formalisieren. Dabei stieß er auf eine falsche Aussage in der ersten Beweisübung: Die Behauptung, dass eine Funktion genau dann injektiv ist, wenn sie eine Linksinverse hat, gilt nicht für den Fall, dass die Definitionsmenge leer ist. Kallus zeigt das Gegenbeispiel und erklärt, wie die formale Verifikation ihn auf diesen Randfall aufmerksam machte.