Lab initiative · live

Formal-proof lane

End-to-end pipeline pairing Leanstral-2603 GGUF with a Lean 4 + Mathlib4 verifier. Math-verified outputs for trading and research callers — no hallucinated proofs.

Components

• Leanstral-2603 GGUF (Q4_K_M) — LRU member of the unified 96GB swap-pool tier, 32K context. LaTeX → Lean 4 translation.
• lean-checker — CPU service running Lean 4 + Mathlib4. Endpoints: /check (typecheck), /translate (LaTeX → Lean 4).

Allowlisted callers

• trading_formal_proof — pre-commit gate, fail-closed.
• autoresearch_formal_proof — paper math-verify stage (researchclaw + finance variant), fail-open.