6 ms·
Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely o
by returningfory2 6d ago
Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.
- charcircuit 6d ago>you don't need to anything more than this You also have to check for things like sorry or defining axioms.