@johncarlosbaez asked:
> how long would it take?
I just noticed I didn't answer your question. An hour is fine. More is more.
R
refurioanachro@mathstodon.xyz
@refurioanachro@mathstodon.xyz
Posts
-
I don't want to formalize any of my work on mathematics. -
I don't want to formalize any of my work on mathematics.Have a look at these Lean games:
It's good to work a few examples to see how they spell out in a proof assistant. It's not difficult! It's fun!
I see proof assistants as a sort of calculator for assumptions. They really shine when you throw lots of stuff at them, like verifying computer programs. Which involves lots of boring stuff, and a proof assistant can help with that! If it's a burden then don't use a proof assistant.