Architecture of proof assistants

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.


tower-cranes-airport-istanbulLean 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.


Moscow ministry of foreign affairsOnce 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.


Is-Hearst-Tower_619X313Designed for use with multiple foundational architectures, Isabelle’s early
development featured classical constructions in set theory. However,
its largest modern tower is HOL.


Squatters in Venezuela

Does this really work? Defying expectations, Metamath seems to function
shockingly well for those who are happy to live without plumbing.



Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s