Self-hostable paraconsistent HoTT LLM-to-Lean acceptance gateway. Runs proof attempts through security preflight, Lean checks, theorem-fingerprint locks, and ShadowHoTT bilattice routing for accept/repair/reject/human-review decisions.
proof-assistant lean formal-methods hott mathlib proof-repair automated-theorem-proving llm llm-tools paraconsistent-logic bilattice shadowhott
-
Updated
May 26, 2026 - Python