/**
 * In-process stub for the `lean-agentic` theorem-prover engine.
 *
 * Background: the upstream `lean-agentic` 0.3.2 npm package ships a
 * broken install — its compiled WASM artifact
 * (`wasm/leanr_wasm.js`) is missing from the published tarball,
 * which crashes the gateway at boot:
 *
 *     Cannot find module ".../node_modules/lean-agentic/wasm/leanr_wasm.js"
 *
 * Until upstream re-publishes a working build (or we vendor our own
 * verifier), this stub keeps `LeanAgenticVerifier` functional with
 * a permissive-but-loggable surface. Every call logs at WARN that
 * real verification is unavailable so a downstream operator can
 * audit how many decisions ran on the stub.
 *
 * Trade-offs:
 * - `prove()` always returns a deterministic proof token. Verifying
 *   that token via `verify()` returns true. This is intentionally
 *   permissive: it lets the gateway boot and serve traffic, but the
 *   *real* policy gating must come from the upstream regex /
 *   heuristic layers (PatternMatcher, Sanitizer) until a real
 *   prover is wired back in.
 * - `hashConsEquals()` falls back to string equality.
 * - `typeCheck()` returns success unconditionally.
 *
 * Replace with a real verifier when lean-agentic ships a working
 * artifact or when we vendor an alternative (e.g. Coq/Lean4-via-WASM).
 */
export interface StubLogger {
    warn: (msg: string, meta?: Record<string, unknown>) => void;
}
export interface ProofResult {
    theorem: string;
    proof: string;
    isValid: boolean;
}
export declare class StubLeanEngine {
    private warnedOnce;
    private logger?;
    private knownAxioms;
    setLogger(logger: StubLogger): void;
    initialize(): Promise<void>;
    shutdown(): Promise<void>;
    addAxiom(axiom: string): Promise<void>;
    prove(theorem: string): Promise<ProofResult>;
    verify(theorem: string, proof: string): Promise<boolean>;
    hashConsEquals(lhs: string, rhs: string): Promise<boolean>;
    typeCheck(_expr: string): Promise<{
        valid: boolean;
        message?: string;
    }>;
    evaluate(_expr: string): Promise<boolean>;
    private warnOnce;
}
/**
 * Drop-in replacement for `leanAgentic.createDemo()`.
 */
export declare function createDemo(): StubLeanEngine;
//# sourceMappingURL=stub-engine.d.ts.map