Learning proof systems

Stream: general

[Juho Kupiainen]

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

[Andrew Ashworth]

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

[Juho Kupiainen]

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]

I doubt there are any such systems

[Mario Carneiro]

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