If you want to mess with this at home, I've been vibe coding https://github.com/kig/formalanswer to plug theorem provers into an LLM call loop. It's pretty early dev but it does have a logic rap battle mode.

This is pretty interesting!