Embed Notice

Automated theorem provers make a nice example. I heard a talk a while back about speeding up Coq by having an LLM feed it a better set of starting points for its solution search.

In that talk, the speaker referred to this as “using AI to assist a theorem prover.” Time was that a theorem prover •itself• was AI! But now •that• is just algorithms; it’s only the LLM that counts as “AI.” The line is always shifting.