Leonardo de Moura

@valeriadepaiva Many thanks!

@valeriadepaiva I agree, I'm sorry about that. At least, J. Otten's provers have suffixes: LeanCoP, LeanTAP, etc.

@valeriadepaiva @arademaker We have an web tutorial goo.gl/rdeCId, you are very welcome to join the list goo.gl/CayRvu

@valeriadepaiva @arademaker We call it Lean because the kernel is small and minimalist. It was not our intention to offend J. Otten.

@valeriadepaiva @arademaker Lean is not related to Z3. Lean is much closer to Coq than automated FO provers like LeanCoP.

Lean is not related to Z3. Lean is much closer to Coq than automated FO provers like LeanCoP. We call it lean because the kernel is small.

@killerswan Thanks... I guess it is safe now: 667

testing tweet button research.microsoft.com/en-us/um/peopl…

Releasing the Z3 source code

Testing tweet button

@RolfRolles regarding division by zero in Z3, see rise4fun.com/Z3Py/pur

@pa_kt @elvanderb This is not a bug. See rise4fun.com/Z3Py/pur