"""
lean_proof — Lean proof automation package.

Backends:
  - deepseek_prover: DeepSeek-Prover-V2-7B via HuggingFace or Ollama
  - alphaproof: existing AlphaProof loop (re-exported from alphaproof_loop.py)
  - language_proof_server: remote proof server (re-exported from lean_trace_bridge.py)

Usage:
    from lean_proof import DeepSeekProver, ProverEngine

    prover = DeepSeekProver(backend="ollama")  # or "huggingface"
    engine = ProverEngine(prover)
    result = engine.prove(theorem_statement, context=lean_module)
"""

from __future__ import annotations

from .deepseek_prover import DeepSeekProver
from .prover_engine import ProverEngine, ProofResult

__all__ = ["DeepSeekProver", "ProverEngine", "ProofResult"]