3 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 22d 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 22d agoNot mm0?