Architecture of proof assistants

Have you ever wondered what mathematical proof assistant to use? Here
is a quick guide to their architectures.

HOL Light

minimal_house_bed_evening_r_1500_medium

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

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.


Mizar

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

CQ-z13425607Q,Zespol-budynkow-biurowych-PIXEL-w-Poznaniu

Coq is built of modular components on a foundation of dependent type theory. This system has grown one PhD thesis at a time.


Isabelle

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.


Metamath

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:

WordPress.com Logo

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

Google photo

You are commenting using your Google 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