Durante su segunda semana en el Recurse Center, Ben Kallus intentó formalizar en Rocq el manual de álgebra abstracta de Dummit y Foote. El primer ejercicio de demostración del libro pide probar que una función es inyectiva si y solo si tiene un inverso izquierdo. Kallus comprobó que el enunciado es falso en un caso límite: cuando el dominio A es el conjunto vacío y el codominio B contiene al menos un elemento, la función vacía es inyectiva de forma trivial, pero no puede tener un inverso izquierdo porque no existen funciones con dominio B no vacío y codominio vacío.
Este contraejemplo, ya recogido en la lista de erratas del libro, sólo apareció gracias al uso de un asistente de pruebas formales. Al intentar demostrar la proposición tal como estaba formulada, el sistema rechazaba las pruebas a menos que se asumiera que A es habitado o que B es no habitado, es decir, las hipótesis necesarias para que el enunciado fuese verdadero. Sobre el papel, ese caso límite habría pasado desapercibido; la herramienta obligó a Kallus a examinar las condiciones de verdad con el rigor que exige un verificador mecánico.
El episodio ilustra el valor de los asistentes de pruebas como Rocq para revelar errores sutiles en manuales de matemáticas y para entender exactamente qué hipótesis sostiene cada teorema. También muestra cómo el trabajo en comunidad, como el que promueve el Recurse Center, se beneficia de combinar el estudio autodirigido con herramientas que obligan a formalizar cada paso.