Z3 is very different from Coq and Lean. Coq and Lean are interactive theorem pro... | Hacker News

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

		ahelwer on April 6, 2020 \| parent \| context \| favorite \| on: Doing a math assignment with the Lean theorem prov... Z3 is very different from Coq and Lean. Coq and Lean are interactive theorem provers, while Z3 is a satisfiability modulo theories (SMT) solver which can do things like checking whether a logical formula is satisfiable or finding a solution for a system of constraints.

The_rationalist on April 6, 2020 [–]

Thanks! And what about agda and Idris?

aweinstock on April 6, 2020 | [–]

Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact