So although lean4 is a programming language that people can use to write “normal” programs, when you use it as a proof assistant this is what you are doing - stating propositions and then using a combination of a (very extensive) library of previous results, your own ingenuity using the builtins of the language and (in my experience anyway) a bunch of brute force to instantiate the type thus proving the proposition.
https://github.com/teorth/analysis
He also has blogged about how he uses lean for his research.
Edit to add: Looking at that repo, one thing I like (but others may find infuriating idk) is that where in the text he leaves certain proofs as exercises for the reader, in the repo he turns those into “sorry”s, so you can fork the repo and have a go at proving those things in lean yourself.
If you have some proposition which you need to use as the basis of further work but you haven’t completed a formal proof of yet, in lean, you can just state the proposition with the proof being “sorry”. Lean will then proceed as though that proposition had been proved except that it will give you a warning saying that you have a sorry. For something to be proved in lean you have to have it done without any “sorry”s. https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tac...
Python and C though have enough nasal demons and undefined behavior that it's a huge pain to verify things about them, since some random other thread can drive by and modify memory in another thread.
Prolog is an efficient programming language because it is a very stupid theorem prover."
Who am I to overrule the author of The Craft of Prolog?
Some would say that SLDNF resolution qualifies as theorem proving, some would disagree and say that a theorem prover also needs such and such capability. Anyway, as Triska shows above you can implement software that is quite a lot like a theorem prover in about thirty lines of Prolog, i.e. not "a dependently typed functional programming language".
The descendants of Milner's work, notably ML and the Edinburgh LCF theorem prover, have been quite successful, though.
It is a strict requirement that all theorem provers have a notion of type. This is by contradiction. Suppose you had a weakly typed theorem language L. Suppose you have a definition D of set in this weakly typed theorem language. Then say x is a set by D. Now suppose y is the set in D of all sets in D that do not contain themselves (Russell...). If this construction were allowed then the theorem prover is not a theorem prover. If this construction is rejected then the theorem prover has a strict notion of kinds of sets which means it's not weakly typed.
Mizar and such do not require constructive definitions a la coq but it has to stratify its universes.