Örülök, hogy tetszik.

Amúgy vannak a metamath-nál kevésbé fapados szoftverek, wikipedian megtalálsz néhányat. A legfeljettebbnek tűnő a Coq.

A négyszín tétel kapcsán wikipedia ezt írja:

"In 2005 Benjamin Werner and Georges Gonthier formalized a proof of the theorem inside the Coq proof assistant. This removed the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel (Gonthier 2008)."

Nem tudom, hogy van-e azóta számítógépmentes bizonyítás, talán Gergő tud erről felfilágosítást adni.

Coq-nak tényleg szép a kezelőfelülete és leírás alapján igen sokat tud, egy hátránya számomra, hogy ha jól értelmezem a kategoriaelméletes matek-megalapozáson alapul elsődlegesen (persze biztos lehet vele szimulálni a sztenderdet is).