Recurse Center में अपने दूसरे सप्ताह के दौरान Rocq में Dummit और Foote की एब्स्ट्रैक्ट बीजगणित को औपचारिक बनाते समय, मैंने पहले प्रमाण अभ्यास का लक्ष्य गलत पाया। प्रस्ताव दावा करता है कि एक फलन इंजेक्टिव है यदि और केवल यदि उसका बायाँ व्युत्क्रम है। लेकिन एक प्रतिउदाहरण मौजूद है: मान लीजिए A खाली है और B = {1}। खाली फलन f: A -> B वैक्यूअसली इंजेक्टिव है, फिर भी कोई फलन g: B -> A मौजूद नहीं है क्योंकि B गैर-खाली है और A खाली है। यह कोना मामला कागज पर आसानी से छूट सकता है, लेकिन Rocq ने मुझे इसका सामना करने के लिए मजबूर किया। संघर्ष के बाद, मैंने पुस्तक की errata जाँची और उसमें यह सूचीबद्ध पाया। यह निराशाजनक था लेकिन स्वतंत्र रूप से खोजना रोमांचक था।