Fix CI lint failures from Lean formalization PR

Addresses ruff violations introduced in #1: trailing/blank-line whitespace
(W291/W293), unused variables (F841), open() vs Path.open() (PTH123),
nested with statements (SIM117), and missing test docstrings (D102).

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

Author: haasonsaas

formal_verification/hybrid_lean_coq_resolver.py

@@ -4,16 +4,17 @@
 for maximum theorem proving coverage when resolving cognitive dissonance.
 """
 
+import logging
 import time
-from typing import Any, Optional, Dict, List, Tuple
 from dataclasses import dataclass
 from enum import Enum
-import logging
+from typing import Any
 
-from .lean_translator import LeanTranslator, LeanStatement
-from .lean_prover import LeanProver, ProofResult as LeanProofResult
-from .translator import ClaimTranslator
+from .lean_prover import LeanProver
+from .lean_prover import ProofResult as LeanProofResult
+from .lean_translator import LeanTranslator
 from .prover import CoqProver
+from .translator import ClaimTranslator
 from .types import Claim, PropertyType
 
 logger = logging.getLogger(__name__)
@@ -31,8 +32,8 @@ class HybridProofResult:
     """Result from hybrid Lean/Coq prover."""
     proven: bool
     prover_used: ProverBackend
-    primary_result: Optional[object] = None
-    fallback_result: Optional[object] = None
+    primary_result: object | None = None
+    fallback_result: object | None = None
     combined_confidence: float = 0.0
 
 
@@ -48,13 +49,13 @@ def __init__(self, prefer_lean: bool = True, use_fallback: bool = True):
         self.coq_prover = CoqProver()
 
     def resolve_conflict(
-        self, claims: List[Tuple[str, str, str]]
+        self, claims: list[tuple[str, str, str]]
     ) -> HybridProofResult:
         """Resolve a conflict between claims using hybrid approach.
-        
+
         Args:
             claims: List of (agent_id, claim_text, claim_type) tuples
-            
+
         Returns:
             HybridProofResult with proof status and prover backend used
         """
@@ -68,7 +69,7 @@ def resolve_conflict(
                     primary_result=lean_result,
                     combined_confidence=0.95,
                 )
-            
+
             # Fallback to Coq
             if self.use_fallback:
                 coq_result = self._try_coq_proof(claims)
@@ -89,7 +90,7 @@ def resolve_conflict(
                     primary_result=coq_result,
                     combined_confidence=0.90,
                 )
-            
+
             # Fallback to Lean
             if self.use_fallback:
                 lean_result = self._try_lean_proof(claims)
@@ -100,23 +101,23 @@ def resolve_conflict(
                         fallback_result=lean_result,
                         combined_confidence=0.85,
                     )
-        
+
         return HybridProofResult(proven=False, prover_used=ProverBackend.HYBRID)
 
-    def _try_lean_proof(self, claims: List[Tuple[str, str, str]]) -> LeanProofResult:
+    def _try_lean_proof(self, claims: list[tuple[str, str, str]]) -> LeanProofResult:
         """Attempt proof using Lean/LeanDojo."""
         try:
             # Translate first claim to Lean
             claim_text = claims[0][1]
             claim_type = claims[0][2]
-            
+
             lean_stmt = self.lean_translator.translate_claim(claim_text, claim_type)
             lean_code = self.lean_translator.to_lean_code(lean_stmt)
-            
+
             # Attempt proof
             proof_result = self.lean_prover.prove(lean_code, lean_stmt.name)
             logger.info(f"Lean proof attempt: {proof_result}")
-            
+
             return proof_result
         except Exception as e:
             logger.error(f"Lean proof failed: {e}")
@@ -127,7 +128,7 @@ def _try_lean_proof(self, claims: List[Tuple[str, str, str]]) -> LeanProofResult
                 error_message=str(e),
             )
 
-    def _try_coq_proof(self, claims: List[Tuple[str, str, str]]) -> Dict[str, Any]:
+    def _try_coq_proof(self, claims: list[tuple[str, str, str]]) -> dict[str, Any]:
         """Attempt proof using Coq (existing implementation)."""
         try:
             agent_id, claim_text, claim_type = claims[0]

formal_verification/lean_prover.py

@@ -4,12 +4,12 @@
 and verification of cognitive dissonance resolutions.
 """
 
-import subprocess
 import json
+import logging
 import os
-from typing import Optional, Dict, Any, List
+import subprocess
 from dataclasses import dataclass
-import logging
+from pathlib import Path
 
 logger = logging.getLogger(__name__)
 
@@ -19,26 +19,26 @@ class ProofResult:
     """Result of a proof attempt."""
     statement_name: str
     proven: bool
-    proof_term: Optional[str] = None
-    error_message: Optional[str] = None
+    proof_term: str | None = None
+    error_message: str | None = None
     proof_time_ms: float = 0.0
 
 
 class LeanProver:
     """Proves Lean 4 theorems using LeanDojo."""
 
-    def __init__(self, leandojo_path: Optional[str] = None, timeout_ms: int = 30000):
+    def __init__(self, leandojo_path: str | None = None, timeout_ms: int = 30000):
         self.leandojo_path = leandojo_path or "leandojo"
         self.timeout_ms = timeout_ms
-        self.proof_cache: Dict[str, ProofResult] = {}
+        self.proof_cache: dict[str, ProofResult] = {}
 
     def prove(self, lean_code: str, statement_name: str) -> ProofResult:
         """Prove a Lean theorem.
-        
+
         Args:
             lean_code: Complete Lean 4 code including theorem
             statement_name: Name of the theorem to prove
-            
+
         Returns:
             ProofResult with proof status and details
         """
@@ -55,7 +55,7 @@ def _attempt_proof(self, lean_code: str, statement_name: str) -> ProofResult:
         try:
             # Write code to temporary file
             temp_file = f"/tmp/lean_{statement_name}.lean"
-            with open(temp_file, "w") as f:
+            with Path(temp_file).open("w") as f:
                 f.write(lean_code)
 
             # Call LeanDojo
@@ -109,13 +109,13 @@ def _attempt_proof(self, lean_code: str, statement_name: str) -> ProofResult:
                 os.remove(temp_file)
 
     def batch_prove(
-        self, theorems: List[tuple[str, str]]
-    ) -> List[ProofResult]:
+        self, theorems: list[tuple[str, str]]
+    ) -> list[ProofResult]:
         """Prove multiple theorems.
-        
+
         Args:
             theorems: List of (lean_code, statement_name) tuples
-            
+
         Returns:
             List of ProofResults
         """
@@ -125,7 +125,7 @@ def verify_proof(self, lean_code: str) -> bool:
         """Verify that Lean code type-checks."""
         try:
             temp_file = "/tmp/lean_verify.lean"
-            with open(temp_file, "w") as f:
+            with Path(temp_file).open("w") as f:
                 f.write(lean_code)
 
             result = subprocess.run(

formal_verification/lean_translator.py

@@ -1,15 +1,13 @@
 """Lean Formalization Translator via LeanDojo.
 
-Translates natural language claims to Lean 4 proofs leveraging the 
+Translates natural language claims to Lean 4 proofs leveraging the
 LeanDojo framework for advanced theorem proving capabilities.
 """
 
+import logging
 import re
-import json
-from typing import Optional, Dict, Any
 from dataclasses import dataclass
-import subprocess
-import logging
+from typing import Any
 
 logger = logging.getLogger(__name__)
 
@@ -19,24 +17,24 @@ class LeanStatement:
     """Lean theorem/lemma statement."""
     name: str
     statement: str
-    proof: Optional[str] = None
-    namespace: Optional[str] = "CognitiveDissonance"
+    proof: str | None = None
+    namespace: str | None = "CognitiveDissonance"
 
 
 class LeanTranslator:
     """Translates natural language claims to Lean 4 formalization."""
 
     def __init__(self, use_leandojo: bool = True):
         self.use_leandojo = use_leandojo
-        self.translation_cache: Dict[str, LeanStatement] = {}
+        self.translation_cache: dict[str, LeanStatement] = {}
 
     def translate_claim(self, claim: str, claim_type: str = "arithmetic") -> LeanStatement:
         """Translate a natural language claim to Lean.
-        
+
         Args:
             claim: Natural language statement
             claim_type: Category of claim (arithmetic, algorithm, invariant, etc.)
-            
+
         Returns:
             LeanStatement with Lean 4 formalization
         """
@@ -69,8 +67,6 @@ def _translate_arithmetic(self, claim: str) -> LeanStatement:
 
         if match:
             a, op, b, result = match.groups()
-            op_map = {"+": "HAdd.hAdd", "-": "HSub.hSub", "*": "HMul.hMul", "/": "HDiv.hDiv"}
-            lean_op = op_map.get(op, "HAdd.hAdd")
 
             statement = f"({a} {op} {b} : Nat) = {result}"
             proof = "by omega"
@@ -129,13 +125,13 @@ def to_lean_code(self, statement: LeanStatement) -> str:
 """.strip()
         return code
 
-    def verify_with_leandojo(self, statement: LeanStatement) -> Dict[str, Any]:
+    def verify_with_leandojo(self, statement: LeanStatement) -> dict[str, Any]:
         """Verify using LeanDojo (requires leandojo installation)."""
         if not self.use_leandojo:
             return {"status": "skipped", "reason": "LeanDojo disabled"}
 
         try:
-            lean_code = self.to_lean_code(statement)
+            self.to_lean_code(statement)
             # LeanDojo API call would go here
             result = {
                 "status": "verified",

tests/test_formal_verification.py

@@ -14,7 +14,10 @@
     PropertyType,
     build_claim_ir,
 )
-from formal_verification.hybrid_lean_coq_resolver import HybridLeanCoqResolver, ProverBackend
+from formal_verification.hybrid_lean_coq_resolver import (
+    HybridLeanCoqResolver,
+    ProverBackend,
+)
 from formal_verification.structured_models import PreservationAudit, PreservationLabel
 
 
@@ -608,26 +611,32 @@ class TestHybridLeanCoqResolver:
     """Tests for the hybrid Lean/Coq fallback resolver."""
 
     def test_try_coq_proof_wraps_proof_result_in_dict(self):
+        """Verify _try_coq_proof returns a dict wrapper around ProofResult."""
         resolver = HybridLeanCoqResolver()
         proof_result = ProofResult(None, True, 12.0, None, None, prover_name="coq")
 
-        with patch.object(resolver.coq_translator, "translate", return_value=Mock()) as mock_translate:
-            with patch.object(resolver.coq_prover, "prove_specification", return_value=proof_result):
-                result = resolver._try_coq_proof([("alice", "2 + 2 = 4", "correctness")])
+        with (
+            patch.object(resolver.coq_translator, "translate", return_value=Mock()) as mock_translate,
+            patch.object(resolver.coq_prover, "prove_specification", return_value=proof_result),
+        ):
+            result = resolver._try_coq_proof([("alice", "2 + 2 = 4", "correctness")])
 
         assert result["proven"] is True
         assert result["result"] is proof_result
         assert result["error"] is None
         mock_translate.assert_called_once()
 
     def test_resolve_conflict_uses_coq_fallback_without_dataclass_get(self):
+        """Verify Coq fallback when Lean proof fails."""
         resolver = HybridLeanCoqResolver(prefer_lean=True, use_fallback=True)
         failed_lean = Mock(proven=False)
         coq_result = {"proven": True, "result": ProofResult(None, True, 1.0, None, None)}
 
-        with patch.object(resolver, "_try_lean_proof", return_value=failed_lean):
-            with patch.object(resolver, "_try_coq_proof", return_value=coq_result):
-                result = resolver.resolve_conflict([("alice", "2 + 2 = 4", "correctness")])
+        with (
+            patch.object(resolver, "_try_lean_proof", return_value=failed_lean),
+            patch.object(resolver, "_try_coq_proof", return_value=coq_result),
+        ):
+            result = resolver.resolve_conflict([("alice", "2 + 2 = 4", "correctness")])
 
         assert result.proven is True
         assert result.prover_used == ProverBackend.COQ