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.