Probably a silly question, but what is the difference between a theorem prover and a proof assistant? Is it that a theorem prover will do more of proof automation or something?

Somebody will correct me but AFAIK, an *interactive* theorem prover (such as Coq) seems the same thing. Automated theorem provers are things like SMT solvers, and often they don't let you write proof scripts: they'll just do the proof (or not) and maybe accept hints (theorem statements), but typically support weaker logics...

yeah as Paolo says, "theorem prover" is usually a catchall for both interactive and fully automated systems that claim to verify logical statements (or "equivalently", check fancy types)

isn’t “equivalently” just about dependent types, Karl? I recall you also use the HOL family…

indeed the quotation marks in "equivalently" are meant to convey that there are a bunch of caveats, such as that you need dependent types to reduce proof checking to type checking. The HOL family has proof checking for statements that are typed terms, but their proof checkers are not type checkers.

Thanks folks.

Julin S has marked this topic as resolved.

Last updated: Jun 24 2024 at 01:01 UTC