Yeah, understanding proof assistants would be the big practical thing. I can read a short proof in Lean, but a lot of it just feels like magic right now.
It looks like I was mainly missing sequent calculus (I learned all in the Hilbert style of deduction) and the convention that gamma is the whole context. I’d see the notation and wonder if I missed something. Thank you for the effort you put in on this!
Yeah, I also only learned natural deduction, until I got to the languages course and the professor told us “this is similar to natural deduction, but different”.
Personally I don’t like lean, I prefer coq. But that’s mostly the vibes, both are actually fine. Lean doesn’t do constructive logic, it does classic logic, but you have to give up program extraction for that. That’s why mathematicians are head over heels for lean.
Yeah, understanding proof assistants would be the big practical thing. I can read a short proof in Lean, but a lot of it just feels like magic right now.
It looks like I was mainly missing sequent calculus (I learned all in the Hilbert style of deduction) and the convention that gamma is the whole context. I’d see the notation and wonder if I missed something. Thank you for the effort you put in on this!
Yeah, I also only learned natural deduction, until I got to the languages course and the professor told us “this is similar to natural deduction, but different”.
Personally I don’t like lean, I prefer coq. But that’s mostly the vibes, both are actually fine. Lean doesn’t do constructive logic, it does classic logic, but you have to give up program extraction for that. That’s why mathematicians are head over heels for lean.