4 ms·
One of the main devs of Z3, Leonardo de Moura, is acutally working on a new, dependently typed, theorem prover called "Lean": http://leanprover.github.io/ http:
by javra 12y ago
One of the main devs of Z3, Leonardo de Moura, is acutally working on a new, dependently typed, theorem prover called "Lean": http://leanprover.github.io/ http://leanprover.github.io/
- NotableAlamode 12y agoIs Lean an LCF system or Curry-Howard based? It seems to be the latter, but if so, what's it's main advantage over the many other Curry-Howard based systems?