I don’t tend to think of lambda prolog as being persay in the same arena as Coq/Agda/Lean, although it is a possible perspective. It is a programming language like prolog, just with support for some interesting logically motivated features. Now, since these features are inspired “computation=proof search” and improve the treatment of binding forms, it can make lambda prolog a more suitable place to do interactive or automatic theorem proving like activities than regular prolog. See https://www.site.uottawa.ca/~afelty/dist/lprolog97.pdf
ELPI GitHub - LPCIC/elpi: Embeddable Lambda Prolog Interpreter is a lambda prolog interpreter that was built as a metaprogramming language for Coq.
What my blog post is trying to do is understand if it is possible to get the meat of the extra things lambda prolog brings to the table as a library in prolog.