z3py interface backed by grind + managed project support

[kiranandcode]

Philip tried lean.py, bounced off the setup friction. Loading Batteries/Mathlib means creating a Lake project with the right deps wired up — lakefile, moreLinkObjs, the whole dance. He also wanted a programmatic interface to grind that looks like z3py. This branch ships both.

lean_py.z3 — z3py vocabulary backed by grind

Same Int, Bools, ForAll, Solver, prove. Expressions build Lean syntax under the hood; free variables are tracked and universally quantified at proof time. The solver tries grind → omega → decide → simp_all in order.

Covers the z3py surface that knuckledragger uses: propositional logic, integer/nat/real arithmetic, bit-vectors (BitVec n with &&&/|||/^^^/<<</>>>), arrays (function types + if-then-else store), algebraic datatypes (uninterpreted sorts + constructor functions), quantifiers, uninterpreted sorts and functions, Solver with push/pop.

Lean is a proof checker, not an SMT solver. check() returns unsat (negation proved) or unknown — never sat. No model extraction.

from lean_py.z3 import *
x, y = Ints('x y')
prove(Implies(And(x > 0, y > 0), x + y > 0))  # proved

lean_py.project.ManagedProject — zero-config Lake projects

Creates and caches a Lake project under ~/.lean_py/managed/ so users can import Batteries or import Mathlib without touching a lakefile. Deps pinned to the active toolchain version (batteries@v4.29.1 for leanprover/lean4:v4.29.1). Tested end-to-end with Batteries — 126k decls loaded, proofs discharged through the managed kernel.

from lean_py.project import ManagedProject
from lean_py.z3 import *
mp = ManagedProject.get(deps=("batteries",))
set_kernel(mp.kernel())
prove(Int('x') + 0 == Int('x'))

What ships

New files:

• lean_py/z3/core.py — expression AST, sorts, operators, quantifiers, bitvecs, arrays, datatypes
• lean_py/z3/solver.py — Solver, prove(), solve(), simplify()
• lean_py/project.py — ManagedProject
• tests/test_z3_compat.py — 51 tests
• examples/07_z3py_drop_in/ — worked example

Modified: lean_py/utils.py (toolchain version helper), README.md (z3py + managed project docs)

Tests

182 total (175 passed, 7 skipped for optional deps). 51 new z3 tests covering: expression building, goal string construction, arithmetic/boolean/quantifier proofs, solver UNSAT, push/pop/context manager, Socrates syllogism, 2-queens, bitvec idempotence, array store-select, constant arrays, datatype constructors.