Idris
Idris is not purely a proof assistant, it is a general purpose programming that also has proving capabilities.
Agda
Similar to Idris but specialised for proofs.
- Agda code for mathematical structures and proofs.
- A very good introduction to Agda on this site.
- Introduction to HoTT using Agda.
Arend
A dependently typed language based on homotopy type theory (HoTT) and Cubical type theory.
This is developed by jetbrains (more about jetbrains on page here).
More information on the page here.
Prolog
Prolog is described as a logic programming language. So can it do proofs?
from ref :
Is Prolog a theorem prover? Richard O'Keefe said: "Prolog is an efficient programming language because it is a very stupid theorem prover".
Thus, there is a connection between Prolog and theorem proving. In fact, execution of a Prolog program can be regarded as a special case of resolution, called SLDNF resolution.
However, Prolog is not a full-fledged theorem prover. In particular, Prolog is logically incomplete due to its depth-first search strategy: Prolog may be unable to find a resolution refutation even if one exists.
Lean
https://leanprover.github.io/functional_programming_in_lean/
