For natural language, reducing hallucinations is a tradeoff between utility and creativity. Not so, for theorem proving and other applications that can be formally verified and certified. Check out our LeanDojo https://
leandojo.org using LLMs including GPT4 interface that has

→ View original post on X — @animaanandkumar