> > The book he is using is: > > https://plfa.github.io/ > > Metamath has a formalization of simply typed lambda calculus by Mario > Carneiro. > > http://us.metamath.org/holuni/mmhol.html > > You can use Philip Wadler's book to catch what it is all about before > delving into Carneiro's code. >
Thanks for the pointers. It's always good to have companion books to a proof assistant ecpesially if it can be applied to one of Metamath's databases. I almost finished "Theorem Proving in Lean" and there is "Logic and Proof" which used Lean as a foundation: https://leanprover.github.io/logic_and_proof/ There are many useful pointers in Metamath's bibliography. I've also read Richard Bornat's book "Proof and Disproof" which might serve mostly as a practical guide to natural deduction in Jape (which has a nice UI for beginners implemented using tactics language, BTW), but also has some information about software verification: http://www.eis.mdx.ac.uk/staffpages/r_bornat/ But honestly, for starters it should not matter as much about logical foundations as it's about assistant, UI, practical workflow and database organization, oriented towards non-mathematicians or undergraduates. Careful selection of theorems from a proof database with good explanations could make a wonderful tutorial in logic, arithmetic and using a proof assistant. That's how natural number game looks like and I enjoyed it as such: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ David asked what others think about extending mmj2's tutorial. And that's what I thought. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/37639c82-2bd2-460a-b637-ee1df1a9b750%40googlegroups.com.
