### 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/