Abstract
Formal verification strengthens agent evaluation by giving mechanical proof checks. It does not eliminate semantic interpretation. This paper studies a boundary exposed by an internal Switchboard-mediated Formal Conjectures run: a Lean kernel can accept a frozen target while the mathematical answer still fails semantic review. The internal run completed 200 counted Lean attempts over FC100OpenSet1 and FC100SolvedSet1, with 100 percent Switchboard evidence coverage and zero missing mediation records. Machine accounting produced 63 inclusive accepted rows, 26 new target proofs, 37 existing clean proofs, 137 depends_on_sorry rows, and three timeouts. Expert semantic review of the three OpenSet machine-accepted targets accepted one as a faithful frozen-target proof, rejected two as inadequate answer instantiations, and found zero novel open-problem discoveries. The contribution is a reporting pattern for formal benchmarks: kernel validity, frozen-target validity, semantic fidelity, prior-result status, and novelty must remain distinct.