Have you ever wondered what mathematical proof assistant to use? Here
is a quick guide to their architectures.
HOL Light has an exquisite minimal design. It has the smallest kernel
of any system. John Harrison is the sole permanent occupant, but he
is very welcoming to guests.
Lean is ambitious, and it will be massive. Do not be fooled by the name.
“Construction area keep out” signs are prominently posted on the
Once the clear front-runner, it now shows signs of age. Do not expect
to understand the inner workings of this system unless you have been
trained in Warsaw.
Coq is built of modular components on a foundation of dependent type theory. This system has grown one PhD thesis at a time.
Designed for use with multiple foundational architectures, Isabelle’s early
development featured classical constructions in set theory. However,
its largest modern tower is HOL.
Does this really work? Defying expectations, Metamath seems to function
shockingly well for those who are happy to live without plumbing.