|
|
|
|
|
|
by hackermailman
1103 days ago
|
|
|
Some universities now have a Lean proof assistant logic course that teaches natural deduction http://leanprover.github.io/logic_and_proof/ Whenever I have asked professors in the past how they first learned proofs the answer was always from doing Euclid in highschool which is no longer taught |
|
|
(A small downside is, in my opinion, that is uses trees instead of a more classical sequential presentation in the style of Suppes and Kleene.
https://en.wikipedia.org/wiki/Natural_deduction#Different_pr...
Trees may be more elegant, but actual, informal proofs in mathematics are written sequentially. So I think trees defeat the purpose of "natural" deduction a bit. But that's complaining on a high level.)