Idris is not purely a proof assistant, it is a general purpose programming that also has proving capabilities.
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.
This is developed by jetbrains (more about jetbrains on page here).
More information on the page here.
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.