Z3! You're on WATCH!
Latest update to lean.py is a drop in replacement for Z3!
Everyone's trying to put SMT solvers in their theorem prover, how about putting a theorem prover in your SMT solver?
and here's the crazy thing: One click install, if you know Z3, you KNOW lean.py.
You are not ready.
Kiran
ML researchers know Python. Proof engineers know Lean. Never the two should meet..
Until now! Announcing Lean.py, effortless Lean to Python and Python to Lean bindings!
- Write Lean tactics in Python
- Access the Python ecosystem in Lean
github.com/kiranandcode...
Kiran
Python and lean are the same language right? (this is lean code that is manipulating Python numpy objects)
