CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

🧊 Модальний гомотопічний верифікатор математики

Anders: Cubical Type Checker

Castle Bravo: Experimental HoTT Implementation

silly automated prover for minimal propositional logic

A toy theorem prover

Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory

Castle Romeo: Experimental Theorem Prover for Category Theory

🧊 Metamath система

A simple first order logic theorem prover using tableaux

Principia: Metamath-like Logician Language

A kernel using inference rules in order to compute the three of proves.

Hurricane: HoTT-I Type System

Propositional theorem prover using the tableaux method and FOL theorem prover using resolution