Claude/fix prover wiring epy ir (#21)

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

src/rust/proof_encoding.rs

@@ -154,8 +154,8 @@ mod tests {
             hypotheses: vec![],
         };
 
-        let id1 = proof_identity("my_theorem", &goal, ProverKind::Lean4);
-        let id2 = proof_identity("my_theorem", &goal, ProverKind::Lean4);
+        let id1 = proof_identity("my_theorem", &goal, ProverKind::Lean);
+        let id2 = proof_identity("my_theorem", &goal, ProverKind::Lean);
         assert_eq!(id1, id2, "Same inputs must produce same identity");
     }
 
@@ -167,7 +167,7 @@ mod tests {
             hypotheses: vec![],
         };
 
-        let lean = proof_identity("thm", &goal, ProverKind::Lean4);
+        let lean = proof_identity("thm", &goal, ProverKind::Lean);
         let coq = proof_identity("thm", &goal, ProverKind::Coq);
         assert_ne!(
             lean, coq,

src/rust/verification/mod.rs

@@ -16,6 +16,8 @@ pub mod confidence;
 pub mod mutation;
 pub mod pareto;
 pub mod portfolio;
+#[cfg(feature = "verisim")]
+pub mod proof;
 pub mod statistics;
 
 pub use axiom_tracker::{AxiomPolicy, AxiomTracker, AxiomUsage, DangerLevel};
@@ -24,4 +26,8 @@ pub use confidence::TrustLevel;
 pub use mutation::{MutationKind, MutationResult, MutationTester};
 pub use pareto::{ParetoFrontier, ProofCandidate, ProofObjective};
 pub use portfolio::{PortfolioConfig, PortfolioResult, PortfolioSolver};
+#[cfg(feature = "verisim")]
+pub use proof::{
+    theorem_identity, Proof, ProofStateRecord, ProofVersion, TacticApplication, TacticStatus,
+};
 pub use statistics::StatisticsTracker;