Theorem prover seems to misleading. It seems to be an SMT solver, not a competit... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		qznc on April 13, 2012 \| parent \| context \| favorite \| on: Rise4fun - from Microsoft Research Theorem prover seems to misleading. It seems to be an SMT solver, not a competitor to Isabelle, Coq, etc.

sanxiyn on April 13, 2012 [–]

Well, SMT solvers do prove theorems, just not kind of theorems that mathematicians care about.

Wikipedia thinks the usage is OK. "Theorem prover may refer to: Automated theorem prover, or Proof assistant, an interactive theorem prover." http://en.wikipedia.org/wiki/Theorem_prover

Consider applying for YC's Summer 2026 batch! Applications are open till May 4
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact