provably.lean4

Lean4 backend — generate and check Lean4 proofs from @verified contracts.

from provably import verify_with_lean4, export_lean4, HAS_LEAN4, LEAN4_VERSION

---

HAS_LEAN4

bool — True if the lean command is available on $PATH.

from provably import HAS_LEAN4
if HAS_LEAN4:
    print("Lean4 available")

---

LEAN4_VERSION

str — version string from lean --version, or "" if Lean4 is not installed.

---

verify_with_lean4()

Verify a function using Lean4 instead of (or in addition to) Z3. Returns a ProofCertificate with z3_version set to "lean4:<version>".

from provably import verify_with_lean4

def clamp(val: float, lo: float, hi: float) -> float:
    if val < lo: return lo
    elif val > hi: return hi
    else: return val

cert = verify_with_lean4(
    clamp,
    pre=lambda val, lo, hi: lo <= hi,
    post=lambda val, lo, hi, result: (result >= lo) & (result <= hi),
)
cert.status          # Status.VERIFIED (if Lean4 closes the proof)
cert.z3_version      # "lean4:leanprover/lean4:v4.x.0"
cert.solver_time_ms  # wall-clock ms in lean

Parameter	Type	Default	Description
func	Callable	required	The function to verify
pre	Callable \| None	None	Precondition lambda
post	Callable \| None	None	Postcondition lambda
timeout_s	float	60.0	Lean4 type-check timeout in seconds

When Lean4 is not installed, returns a SKIPPED certificate with an installation hint.

---

export_lean4()

Export a @verified function as a Lean4 theorem file. Returns the Lean4 source code as a string. Optionally writes to a file.

from provably import export_lean4

lean_code = export_lean4(
    clamp,
    pre=lambda val, lo, hi: lo <= hi,
    post=lambda val, lo, hi, result: (result >= lo) & (result <= hi),
    output_path="clamp.lean",
)
print(lean_code)
# -- Auto-generated by provably.lean4
# import Mathlib.Tactic
# noncomputable def clamp_impl ...
# theorem clamp_verified ...

Parameter	Type	Default	Description
func	Callable	required	The function to export
pre	Callable \| None	None	Precondition lambda
post	Callable \| None	None	Postcondition lambda
output_path	str \| Path \| None	None	Write Lean4 source to this path

Does not require Lean4 to be installed (generates code only).

---

Pipeline

The Lean4 backend follows the same flow as the Z3 backend:

1. Parse function AST + contracts
2. Generate Lean4 noncomputable def from the function body
3. Generate theorem ... := by unfold; split_ifs <;> nlinarith
4. Write to a temp .lean file
5. Run lean to type-check
6. Return ProofCertificate with outcome

---

Limitations

• Same arithmetic subset as Z3 translator (no recursion, no data structures)
• Transcendental functions (exp, cos, log) are axiomatized
• For-loop unrolling produces verbose Lean4 proofs
• Slower than Z3 (compiles to native code)
• Requires Lean4 + Mathlib for nlinarith tactic

---

Installation

# Install elan (Lean4 version manager)
brew install elan-init   # macOS
# or: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh

# Set stable toolchain
elan default stable

---

provably.lean4

Lean4 backend — generate and check Lean4 proofs from @verified contracts.

Translates Python functions with pre/post conditions into Lean4 theorem statements + tactic proofs. The Lean4 type checker then serves as an independent verification oracle (cross-checking Z3 results).

Pipeline

1. Parse function AST + contracts (same as Z3 backend)
2. Generate Lean4 theorem statement from pre/post
3. Generate tactic proof sketch (nlinarith/omega/simp/linarith)
4. Write to temp .lean file
5. Run lean to type-check
6. Return ProofCertificate with status and lean4 proof text

Requirements

• Lean4 installed (via elan): brew install elan-init && elan default stable
• No Mathlib needed for basic arithmetic theorems (uses Lean4 stdlib)

Limitations

• Only supports the same arithmetic subset as the Z3 translator
• Transcendental functions (exp, cos, log) are axiomatized
• For-loop unrolling produces verbose proofs
• Slower than Z3 (compiles to native code)

Classes

Functions

check_lean4_proof

check_lean4_proof(lean_code: str, timeout_s: float = 60.0) -> tuple[bool, str]

Write Lean4 code to a temp file and check it.

Returns (success, output).

Source code in src/provably/lean4.py

def check_lean4_proof(lean_code: str, timeout_s: float = 60.0) -> tuple[bool, str]:
    """Write Lean4 code to a temp file and check it.

    Returns (success, output).
    """
    if not HAS_LEAN4:
        return False, "Lean4 not installed"

    with tempfile.NamedTemporaryFile(
        mode="w", suffix=".lean", delete=False, prefix="provably_"
    ) as f:
        f.write(lean_code)
        tmp_path = f.name

    try:
        result = subprocess.run(
            ["lean", tmp_path],
            capture_output=True,
            text=True,
            timeout=timeout_s,
        )
        output = (result.stdout + result.stderr).strip()
        return result.returncode == 0, output
    except subprocess.TimeoutExpired:
        return False, f"Lean4 timed out after {timeout_s}s"
    except FileNotFoundError:
        return False, "lean command not found"
    finally:
        Path(tmp_path).unlink(missing_ok=True)

export_lean4

export_lean4(func: Any, pre: Any | None = None, post: Any | None = None, output_path: str | Path | None = None) -> str

Export a @verified function as a Lean4 theorem file.

Returns the Lean4 source code. Optionally writes to output_path.

Source code in src/provably/lean4.py

def export_lean4(
    func: Any,
    pre: Any | None = None,
    post: Any | None = None,
    output_path: str | Path | None = None,
) -> str:
    """Export a @verified function as a Lean4 theorem file.

    Returns the Lean4 source code. Optionally writes to output_path.
    """
    import z3 as _z3

    from .types import extract_refinements, make_z3_var

    fname = getattr(func, "__name__", str(func))
    source = textwrap.dedent(inspect.getsource(func))

    tree = ast.parse(source)
    func_ast = tree.body[0]
    if not isinstance(func_ast, ast.FunctionDef):
        return "-- Error: not a function definition\n"

    try:
        from typing import get_type_hints

        hints = get_type_hints(func, include_extras=True)
    except Exception:
        hints = {}

    param_names = [arg.arg for arg in func_ast.args.args]
    param_types: dict[str, type] = {}
    param_vars: dict[str, Any] = {}
    for name in param_names:
        typ = hints.get(name, float)
        param_types[name] = typ
        param_vars[name] = make_z3_var(name, typ)

    param_list = [param_vars[n] for n in param_names]
    pre_strs: list[str] = []
    post_strs: list[str] = []

    if pre is not None:
        try:
            pre_z3 = pre(*param_list)
            if isinstance(pre_z3, _z3.BoolRef):
                pre_strs.append(str(pre_z3))
        except Exception:
            pass

    for name, var in param_vars.items():
        typ = hints.get(name)
        if typ is not None:
            for constraint in extract_refinements(typ, var):
                pre_strs.append(str(constraint))

    if post is not None:
        result_var = _z3.Real("result")
        try:
            post_z3 = post(*param_list, result_var)
            if isinstance(post_z3, _z3.BoolRef):
                post_strs.append(str(post_z3))
        except Exception:
            pass

    pre_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in pre_strs) if pre_strs else None
    )
    post_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in post_strs)
        if post_strs
        else None
    )

    if post_lean:
        post_lean = post_lean.replace("result", f"({fname}_impl {' '.join(param_names)})")

    lean_code = generate_lean4_theorem(
        func_name=fname,
        param_names=param_names,
        param_types=param_types,
        pre_str=pre_lean,
        post_str=post_lean,
        source=source,
    )

    if output_path is not None:
        Path(output_path).write_text(lean_code)

    return lean_code

generate_lean4_theorem

generate_lean4_theorem(func_name: str, param_names: list[str], param_types: dict[str, type], pre_str: str | None, post_str: str | None, source: str) -> str

Generate a complete Lean4 file with theorem statement + proof attempt.

Uses the Z3 string representations of pre/post conditions translated to Lean4 syntax.

Source code in src/provably/lean4.py

def generate_lean4_theorem(
    func_name: str,
    param_names: list[str],
    param_types: dict[str, type],
    pre_str: str | None,
    post_str: str | None,
    source: str,
) -> str:
    """Generate a complete Lean4 file with theorem statement + proof attempt.

    Uses the Z3 string representations of pre/post conditions translated
    to Lean4 syntax.
    """
    # Parse to get AST
    tree = ast.parse(source)
    func_ast = tree.body[0]
    if not isinstance(func_ast, ast.FunctionDef):
        return "-- Error: not a function definition\nsorry"

    # Build parameter declarations
    params = []
    for name in param_names:
        typ = param_types.get(name, float)
        lean_type = _py_type_to_lean(typ)
        # For proofs, use ℝ instead of Float (Float lacks algebraic properties)
        if lean_type == "Float":
            lean_type = "ℝ"
        params.append(f"({name} : {lean_type})")
    param_decl = " ".join(params)

    # Build Lean definition (function body)
    env = {n: n for n in param_names}
    body = _func_body_to_lean(func_ast, env)

    # Build the theorem
    lean_lines = [
        "-- Auto-generated by provably.lean4",
        f"-- Source: @verified function '{func_name}'",
        "",
        "import Mathlib.Tactic",
        "",
        f"noncomputable def {func_name}_impl {param_decl} : ℝ :=",
        f"  {body}",
        "",
    ]

    # Generate theorem from pre/post strings
    if pre_str and post_str:
        lean_lines.extend(
            [
                f"theorem {func_name}_verified {param_decl}",
                f"  (h_pre : {pre_str})",
                f"  : {post_str} := by",
                f"  unfold {func_name}_impl",
                "  split_ifs <;> nlinarith",
            ]
        )
    elif post_str:
        lean_lines.extend(
            [
                f"theorem {func_name}_verified {param_decl}",
                f"  : {post_str} := by",
                f"  unfold {func_name}_impl",
                "  split_ifs <;> nlinarith",
            ]
        )
    else:
        lean_lines.append(f"-- No postcondition to prove for {func_name}")

    return "\n".join(lean_lines)

verify_with_lean4

verify_with_lean4(func: Any, pre: Any | None = None, post: Any | None = None, timeout_s: float = 60.0) -> ProofCertificate

Verify a function using Lean4 instead of (or in addition to) Z3.

Same interface as verify_function but uses Lean4 type checker.

Source code in src/provably/lean4.py

def verify_with_lean4(
    func: Any,
    pre: Any | None = None,
    post: Any | None = None,
    timeout_s: float = 60.0,
) -> ProofCertificate:
    """Verify a function using Lean4 instead of (or in addition to) Z3.

    Same interface as verify_function but uses Lean4 type checker.
    """
    import z3 as _z3

    from .types import extract_refinements, make_z3_var

    fname = getattr(func, "__name__", str(func))

    if not HAS_LEAN4:
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.SKIPPED,
            preconditions=(),
            postconditions=(),
            message="Lean4 not installed (install via: brew install elan-init && elan default stable)",
        )

    # Get source
    try:
        source = textwrap.dedent(inspect.getsource(func))
    except (OSError, TypeError) as e:
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.SKIPPED,
            preconditions=(),
            postconditions=(),
            message=f"Cannot get source: {e}",
        )

    # Parse
    tree = ast.parse(source)
    func_ast_raw = tree.body[0]
    if not isinstance(func_ast_raw, ast.FunctionDef):
        return ProofCertificate(
            function_name=fname,
            source_hash="",
            status=Status.TRANSLATION_ERROR,
            preconditions=(),
            postconditions=(),
            message="Not a function definition",
        )
    func_ast: ast.FunctionDef = func_ast_raw

    # Extract param info
    try:
        from typing import get_type_hints

        hints = get_type_hints(func, include_extras=True)
    except Exception:
        hints = {}

    param_names = [arg.arg for arg in func_ast.args.args]
    param_types: dict[str, type] = {}
    param_vars: dict[str, Any] = {}
    for name in param_names:
        typ = hints.get(name, float)
        param_types[name] = typ
        param_vars[name] = make_z3_var(name, typ)

    # Build Z3 string representations of pre/post
    pre_strs: list[str] = []
    post_strs: list[str] = []
    param_list = [param_vars[n] for n in param_names]

    if pre is not None:
        try:
            pre_z3 = pre(*param_list)
            if isinstance(pre_z3, _z3.BoolRef):
                pre_strs.append(str(pre_z3))
        except Exception:
            pass

    # Add refinement constraints
    for name, var in param_vars.items():
        typ = hints.get(name)
        if typ is not None:
            for constraint in extract_refinements(typ, var):
                pre_strs.append(str(constraint))

    if post is not None:
        # Create a result variable for postcondition
        result_var = _z3.Real("result")
        try:
            post_z3 = post(*param_list, result_var)
            if isinstance(post_z3, _z3.BoolRef):
                post_strs.append(str(post_z3))
        except Exception:
            pass

    # Convert to Lean4 syntax
    pre_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in pre_strs) if pre_strs else None
    )
    post_lean = (
        " ∧ ".join(f"({_z3_str_to_lean(s, param_names)})" for s in post_strs)
        if post_strs
        else None
    )

    # Replace 'result' with the actual function definition body
    if post_lean:
        post_lean = post_lean.replace("result", f"({fname}_impl {' '.join(param_names)})")

    # Generate Lean4 code
    lean_code = generate_lean4_theorem(
        func_name=fname,
        param_names=param_names,
        param_types=param_types,
        pre_str=pre_lean,
        post_str=post_lean,
        source=source,
    )

    # Check with Lean4
    t0 = time.monotonic()
    success, output = check_lean4_proof(lean_code, timeout_s=timeout_s)
    elapsed = (time.monotonic() - t0) * 1000

    source_hash = hashlib.sha256(source.encode()).hexdigest()[:16]

    if success:
        return ProofCertificate(
            function_name=fname,
            source_hash=source_hash,
            status=Status.VERIFIED,
            preconditions=tuple(pre_strs),
            postconditions=tuple(post_strs),
            solver_time_ms=elapsed,
            z3_version=f"lean4:{LEAN4_VERSION}",
            message="Lean4 type-checked successfully",
        )
    else:
        return ProofCertificate(
            function_name=fname,
            source_hash=source_hash,
            status=Status.UNKNOWN,
            preconditions=tuple(pre_strs),
            postconditions=tuple(post_strs),
            solver_time_ms=elapsed,
            z3_version=f"lean4:{LEAN4_VERSION}",
            message=f"Lean4 proof failed: {output[:500]}",
        )