You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
search_for_proof semantic-lane candidates now return the clean Lean name (e.g. FirstOrder.Language.BoundedFormula.IsDelta0.bdAll) with the module field populated, instead of leaking the
downstream origin:module:declName corpus key as the name (e.g. lean-host-mcp:KanProofs.ModelTheory.Delta0.Basic:FirstOrder…bdAll). The prefixed key broke the documented key-free
contract and the search_for_proof → inspect_declaration handoff.