Show HN: I'm 6 months late, but I made a Natural Language theorem prover

Last year, I built a theorem prover in Ocaml for propositional logic: https://github.com/ArnavAgrawal03/ProveML. After the release of structured outputs, I thought it would be fun to see if we could turn natural language into propositional logic statements and use the theorem prover to answer queries more deterministically.

In my limited testing, this actually works really well! I feel there's a lot of potential in employing LLMs as a "frontend" for more deterministic backends (such as theorem provers). Would love to hear your thoughts - would you use something like this if deployed to production with wider support and nice APIs?

I'm also interested in thinking of this as an alternative to regular RAG or knowledge graphs - though using a resolution-refutation based theorem prover would make retrieval a lot more expensive

Your OpenAI Key is still visible in the commit history.