Have you ever wondered what mathematical proof assistant to use? Here
is a quick guide to their architectures.
HOL Light
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
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
perimeter fencing.
Mizar
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
Coq is built of modular components on a foundation of dependent type theory. This system has grown one PhD thesis at a time.
Isabelle
Designed for use with multiple foundational architectures, Isabelle’s early
development featured classical constructions in set theory. However,
its largest modern tower is HOL.
Metamath
Does this really work? Defying expectations, Metamath seems to function
shockingly well for those who are happy to live without plumbing.
