3 ms·
> When I’m trying to write a proof, I think of the definitions and theorems as my standard library. I look at the conclusion of the theorem to prove as the resu
by Tainnor 1y ago
> When I’m trying to write a proof, I think of the definitions and theorems as my standard library. I look at the conclusion of the theorem to prove as the result I need to obtain and then think about how to build it using my library.
fwiw, this is exactly the thing that you when you're trying to formally prove some theorem in a language like Lean.
- chongli 1y agoI do want to learn theorem proving in Lean just for a hobby at some point. I haven't found a great resource for it though.