Lean theorem prover
From Infogalactic: the planetary knowledge core
A lean theorem prover is an automated theorem prover implemented in a minimum amount of code. Lean provers are generally[citation needed] implemented in Prolog, and make proficient use of the backtracking engine and logic variables of that language. Lean provers can be as small as a few hundred bytes of source code.
Lean theorem provers
<templatestyles src="Asbox/styles.css"></templatestyles>