Zulip Chat Archive

Stream: general

Topic: Learning proof systems


Juho Kupiainen (Nov 03 2019 at 14:38):

What would be a good first proof checker to fully read through and understand?

Andrew Ashworth (Nov 03 2019 at 14:41):

It would be helpful if you also posted your background, experience, and motivation for this

Juho Kupiainen (Nov 03 2019 at 14:56):

I need to build my own proof system for my project (https://general-ai-group.com) and I would like to get to know some good system entirely. The system should have a strong axiomatic framework, good syntax, and a short implementation using primitive concepts that employs good algorithms, though the performance does not need to be hardware optimized.

Reid Barton (Nov 03 2019 at 22:13):

I doubt there are any such systems

Mario Carneiro (Nov 04 2019 at 00:06):

Metamath is the obvious choice here. HOL Light is also pretty clean and can be read in an afternoon


Last updated: Dec 20 2023 at 11:08 UTC