2 ms·
I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.
by throw567643u8 2mo ago
I'd feel so much more excited if this was done in Metamath. Tiny checker kernel, no complicated dependent types, way less to go wrong.
- Jblx2 2mo agoNot mm0?