Lab initiative · live

Formal-proof lane

End-to-end pipeline pairing the Mac fleet formal-prover lane with a Lean 4 + Mathlib4 verifier. Math-verified outputs for trading and research callers — no hallucinated proofs.

Components

• Mac fleet formal-prover lane — always-on LaTeX → Lean 4 translation served from the Mac stack.
• 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.