I'm not sure I can answer that question. I don't know enough about Prolog. I can say that your example could be encoded in Lean as a type and the definition wou

I'm not sure I can answer that question. I don't know enough about Prolog. I can say that your example could be encoded in Lean as a type and the definition would probably be much shorter. Does Prolog automate some of the work involved in writing a proof?