Or expect the LLM to only output Prolog, with the assumptions and knowledge as clauses?

Vlad Tenev's new startup apparently does exactly this, but with Lean4. So what's not to expect here? Last two years saw so many neural-symbolic systems released that its very hard to not see where this all goes...