fix: Address review feedback on Lean prover status and witness inference

- LeanProver: use ProofStatus.default_for_solver_result() for failed
  proofs instead of hardcoding REFUTED — a tactic insufficiency is
  INCONCLUSIVE, not a definitive disproof
- LeanTranslator._exists: infer witness from property bounds (x > 5 → 6,
  x >= 10 → 10, x = 3 → 3) instead of hardcoding 1
- Add test for witness inference

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: haasonsaas

formal_verification/lean_prover.py

@@ -168,6 +168,9 @@ def _run_lean(
                 spec.spec_text,
                 stderr[:100],
             )
+            status = ProofStatus.default_for_solver_result(
+                proven=False, prover_name="lean", counter_example=None,
+            )
             return ProofResult(
                 spec=spec,
                 proven=False,
@@ -176,5 +179,5 @@ def _run_lean(
                 counter_example=None,
                 proof_output=stdout,
                 prover_name="lean",
-                solver_status=ProofStatus.REFUTED.value,
+                solver_status=status.value,
             )

formal_verification/lean_translator.py

@@ -244,9 +244,10 @@ def _exists(
         self, claim: Claim, variable: str, prop: str
     ) -> FormalSpec:
         prop_lean = self._to_lean_expr(prop)
+        witness = self._infer_witness(variable, prop_lean)
         lean = (
             f"theorem exists_claim : ∃ {variable} : Nat, "
-            f"{prop_lean} := ⟨1, by omega⟩"
+            f"{prop_lean} := ⟨{witness}, by omega⟩"
         )
         return FormalSpec(
             claim=claim,
@@ -256,6 +257,35 @@ def _exists(
             claim_ir=claim.claim_ir,
         )
 
+    @staticmethod
+    def _infer_witness(variable: str, prop: str) -> str:
+        """Extract a plausible witness from a Lean property expression.
+
+        Handles patterns like ``x > 5`` (witness 6), ``x = 3`` (witness 3),
+        ``x >= 10`` (witness 10).  Falls back to ``0`` when no bound is found.
+        """
+        # "x > N" → N + 1
+        m = re.search(rf"\b{re.escape(variable)}\s*>\s*(\d+)", prop)
+        if m:
+            return str(int(m[1]) + 1)
+        # "x >= N" or "x ≥ N" → N
+        m = re.search(rf"\b{re.escape(variable)}\s*(?:>=|≥)\s*(\d+)", prop)
+        if m:
+            return m[1]
+        # "x = N" → N
+        m = re.search(rf"\b{re.escape(variable)}\s*=\s*(\d+)", prop)
+        if m:
+            return m[1]
+        # "N < x" → N + 1
+        m = re.search(rf"(\d+)\s*<\s*{re.escape(variable)}\b", prop)
+        if m:
+            return str(int(m[1]) + 1)
+        # "N <= x" or "N ≤ x" → N
+        m = re.search(rf"(\d+)\s*(?:<=|≤)\s*{re.escape(variable)}\b", prop)
+        if m:
+            return m[1]
+        return "0"
+
     @staticmethod
     def _to_lean_expr(text: str) -> str:
         """Convert natural language fragments to Lean syntax."""

tests/test_formal_verification.py

@@ -702,6 +702,25 @@ def test_translate_gcd(self):
         assert spec is not None
         assert "Nat.gcd 12 8 = 4" in spec.coq_code
 
+    def test_exists_infers_witness_from_bound(self):
+        """Existential witness is derived from the property, not hardcoded."""
+        translator = LeanTranslator()
+        ir = build_claim_ir("exists x, x > 5")
+        if ir is None:
+            # If IR parsing doesn't handle this, test regex path
+            claim = Claim(
+                "a", "exists x such that x > 5",
+                PropertyType.CORRECTNESS, 1.0, 0,
+            )
+        else:
+            claim = Claim(
+                "a", "exists x, x > 5",
+                PropertyType.CORRECTNESS, 1.0, 0, claim_ir=ir,
+            )
+        spec = translator.translate(claim)
+        if spec is not None:
+            assert "⟨6," in spec.coq_code
+
     def test_untranslatable_returns_none(self):
         """Return None for claims that cannot be translated."""
         translator = LeanTranslator()
@@ -775,7 +794,7 @@ def test_successful_proof(self, mock_run):
 
     @patch("subprocess.run")
     def test_failed_proof(self, mock_run):
-        """Failed lean invocation returns refuted."""
+        """Failed lean invocation returns inconclusive."""
         mock_run.return_value = Mock(
             returncode=1, stdout=b"", stderr=b"type mismatch"
         )
@@ -789,7 +808,7 @@ def test_failed_proof(self, mock_run):
             result = prover.prove_specification(spec)
 
             assert result.proven is False
-            assert result.solver_status == "refuted"
+            assert result.solver_status == "inconclusive"
             assert "type mismatch" in result.error_message
 
     @patch("subprocess.run")
@@ -836,7 +855,7 @@ def test_lean_failure_falls_back_to_coq(self):
         resolver = HybridLeanCoqResolver(prefer_lean=True, use_fallback=True)
         lean_fail = ProofResult(
             None, False, 10.0, "failed", None, prover_name="lean",
-            solver_status="refuted",
+            solver_status="inconclusive",
         )
         coq_ok = ProofResult(
             None, True, 20.0, None, None, prover_name="coq",
@@ -859,7 +878,7 @@ def test_no_fallback_returns_first_failure(self):
         resolver = HybridLeanCoqResolver(prefer_lean=True, use_fallback=False)
         lean_fail = ProofResult(
             None, False, 5.0, "failed", None, prover_name="lean",
-            solver_status="refuted",
+            solver_status="inconclusive",
         )
 
         with (