"""
Adapter for running Lean 4 proofs from Python.
"""
import subprocess
import os

def run_lean4(input_file: str, lean_dir: str = "external/lean4") -> str:
    """
    Runs Lean 4 on the given input file and returns the output as a string.
    """
    exe_path = os.path.join(lean_dir, "bin", "lean")
    if not os.path.exists(exe_path):
        raise FileNotFoundError(f"Lean 4 not found at {exe_path}")
    try:
        result = subprocess.run([
            exe_path, input_file
        ], capture_output=True, text=True, check=True)
        return result.stdout
    except Exception as e:
        return f"Lean 4 error: {e}"