hyperpolymath
diff --git a/‎src/rust/ffi/mod.rs‎
Lines changed: 18 additions & 3 deletions b/‎src/rust/ffi/mod.rs‎
Lines changed: 18 additions & 3 deletions
diff --git a/‎src/rust/provers/connection_method.rs‎
Lines changed: 128 additions & 0 deletions b/‎src/rust/provers/connection_method.rs‎
Lines changed: 128 additions & 0 deletions
diff --git a/‎src/rust/provers/ileancop.rs‎
Lines changed: 216 additions & 0 deletions b/‎src/rust/provers/ileancop.rs‎
Lines changed: 216 additions & 0 deletions
@@ -530,6 +530,12 @@ pub fn kind_from_u8(kind: u8) -> Option<ProverKind> {
         126 => Some(ProverKind::Stainless),
         127 => Some(ProverKind::LiquidHaskell),
         128 => Some(ProverKind::KeYmaeraX),
+        129 => Some(ProverKind::Qepcad),
+        130 => Some(ProverKind::Redlog),
+        131 => Some(ProverKind::MleanCoP),
+        132 => Some(ProverKind::IleanCoP),
+        133 => Some(ProverKind::NanoCoP),
+        134 => Some(ProverKind::MetTeL2),
         _ => None,
     }
 }
@@ -1272,6 +1278,12 @@ pub fn kind_to_u8(kind: ProverKind) -> u8 {
         ProverKind::Stainless => 126,
         ProverKind::LiquidHaskell => 127,
         ProverKind::KeYmaeraX => 128,
+        ProverKind::Qepcad => 129,
+        ProverKind::Redlog => 130,
+        ProverKind::MleanCoP => 131,
+        ProverKind::IleanCoP => 132,
+        ProverKind::NanoCoP => 133,
+        ProverKind::MetTeL2 => 134,
     }
 }
 
@@ -1456,9 +1468,12 @@ mod tests {
 
     #[test]
     fn test_kind_from_u8_out_of_range() {
-        // 0–127 are valid; 128+ are out of range.
-        // (Boundary moved to 127 on 2026-04-26 adding Phase 1a/1b ATPs and Phase 5 backends.)
-        assert!(kind_from_u8(128).is_none());
+        // 0–134 are valid; 135+ are out of range.
+        // (Boundary moved to 134 on 2026-04-27 adding Phase 3
+        // backends — KeYmaeraX (128), Qepcad (129), Redlog (130),
+        // MleanCoP (131), IleanCoP (132), NanoCoP (133), MetTeL2 (134).
+        // Previous boundary was 127 — Phase 1a/1b ATPs + Phase 5.)
+        assert!(kind_from_u8(135).is_none());
         assert!(kind_from_u8(200).is_none());
         assert!(kind_from_u8(255).is_none());
     }
 
@@ -0,0 +1,128 @@
+// SPDX-FileCopyrightText: 2026 ECHIDNA Project Team
+// SPDX-License-Identifier: PMPL-1.0-or-later
+
+//! Shared helpers for the connection-method prover family
+//! (MleanCoP / ileanCoP / nanoCoP).
+//!
+//! These three Prolog-based backends share TPTP-shaped input,
+//! SZS-marker output, and the same SWI-Prolog spawn pattern.  This
+//! module factors out the common pieces so each backend file is a
+//! thin wrapper.
+
+#![allow(dead_code)]
+
+use anyhow::Result;
+use crate::core::ProofState;
+
+/// Convert a `ProofState` into a TPTP fof-formatted input.
+///
+/// Same shape as `metitarski::to_tptp` but factored here so the
+/// connection-method trio share a single serialiser.
+pub(crate) fn to_tptp(state: &ProofState) -> String {
+    let mut tptp = String::new();
+    for (i, axiom) in state.context.axioms.iter().enumerate() {
+        tptp.push_str(&format!("fof(axiom_{}, axiom, {}).\n", i, axiom));
+    }
+    for (i, def) in state.context.definitions.iter().enumerate() {
+        tptp.push_str(&format!("fof(definition_{}, axiom, {}).\n", i, def));
+    }
+    if let Some(goal) = state.goals.first() {
+        tptp.push_str(&format!("fof(conjecture, conjecture, {}).\n", goal.target));
+    }
+    tptp
+}
+
+/// Parse a connection-method prover's stdout for SZS markers and the
+/// native "matrix proof found" signal that the leanCoP family emits.
+///
+/// Returns `Ok(true)` for theorem-status outputs, `Ok(false)` for
+/// counter-satisfiable / refuted, and `Err` for inconclusive
+/// (`GaveUp`, timeout, parse error).
+pub(crate) fn parse_szs_or_native(output: &str) -> Result<bool> {
+    let lower = output.to_ascii_lowercase();
+
+    // SZS markers (TPTP convention).
+    if lower.contains("szs status theorem") {
+        return Ok(true);
+    }
+    if lower.contains("szs status countersatisfiable")
+        || lower.contains("szs status counter-satisfiable")
+        || lower.contains("szs status unsatisfiable")
+    {
+        return Ok(false);
+    }
+    if lower.contains("szs status gaveup") || lower.contains("szs status gave up") {
+        return Err(anyhow::anyhow!(
+            "Connection-method prover gave up: {}",
+            output.lines().take(10).collect::<Vec<_>>().join("\n")
+        ));
+    }
+
+    // Native leanCoP-family signals.
+    if lower.contains("matrix proof found") || lower.contains("proof found") {
+        return Ok(true);
+    }
+    if lower.contains("no proof") || lower.contains("not a theorem") {
+        return Ok(false);
+    }
+    if lower.contains("error") || lower.contains("exception") {
+        return Err(anyhow::anyhow!(
+            "Connection-method prover error: {}",
+            output.lines().take(10).collect::<Vec<_>>().join("\n")
+        ));
+    }
+
+    Err(anyhow::anyhow!(
+        "Connection-method prover output inconclusive: {}",
+        output.lines().take(10).collect::<Vec<_>>().join("\n")
+    ))
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::core::{Goal, Term};
+
+    #[test]
+    fn test_to_tptp_emits_axioms_and_conjecture() {
+        let mut state = ProofState::default();
+        state.context.axioms.push("p | ~ p".to_string());
+        state.goals.push(Goal {
+            id: "g0".to_string(),
+            target: Term::Const("p".to_string()),
+            hypotheses: vec![],
+        });
+        let tptp = to_tptp(&state);
+        assert!(tptp.contains("fof(axiom_0, axiom, p | ~ p)."));
+        assert!(tptp.contains("fof(conjecture, conjecture, p)."));
+    }
+
+    #[test]
+    fn test_parse_szs_theorem() {
+        let r = parse_szs_or_native("% SZS status Theorem\n").expect("expected Ok");
+        assert!(r);
+    }
+
+    #[test]
+    fn test_parse_szs_countersatisfiable() {
+        let r = parse_szs_or_native("% SZS status CounterSatisfiable\n").expect("expected Ok");
+        assert!(!r);
+    }
+
+    #[test]
+    fn test_parse_szs_gaveup_is_err() {
+        assert!(parse_szs_or_native("% SZS status GaveUp\n").is_err());
+    }
+
+    #[test]
+    fn test_parse_native_proof_found() {
+        let r = parse_szs_or_native("Matrix proof found").expect("expected Ok");
+        assert!(r);
+    }
+
+    #[test]
+    fn test_parse_native_no_proof() {
+        let r = parse_szs_or_native("No proof.\n").expect("expected Ok");
+        assert!(!r);
+    }
+}
@@ -0,0 +1,216 @@
+// SPDX-FileCopyrightText: 2026 ECHIDNA Project Team
+// SPDX-License-Identifier: PMPL-1.0-or-later
+
+//! ileanCoP backend — connection-method prover for intuitionistic
+//! first-order logic.
+//!
+//! ileanCoP is the intuitionistic-logic member of the leanCoP family.
+//! It uses the *intuitionistic* connection method (with
+//! prefix-checking to enforce constructive validity) rather than the
+//! classical version used by MleanCoP.
+//!
+//! ## Why this backend exists
+//!
+//! Constructive provers (Coq, Agda, Lean, Idris2) live in
+//! intuitionistic logic.  ileanCoP gives ECHIDNA a *fully automated*
+//! intuitionistic ATP that complements those interactive provers —
+//! useful for offloading the trivial-but-tedious lemmas that arise
+//! during constructive proof development.
+//!
+//! ## Input format
+//!
+//! TPTP fof, same as MleanCoP.  The "intuitionistic" interpretation
+//! is enforced by the prover — the input syntax is unchanged.
+//!
+//! ## CLI invocation
+//!
+//! `swipl -g "ileancop:prove(...)"` or via stdin like MleanCoP.
+//!
+//! ## Output parsing
+//!
+//! Same SZS / native markers as MleanCoP — see
+//! `connection_method::parse_szs_or_native`.
+//!
+//! ## Integration tier
+//!
+//! Tier-5d / Phase-3.  Trust tier 3 (intuitionistic kernel is *small*
+//! and well-studied — connection-method gives a checkable matrix
+//! proof object with a 30-line core).  Complexity 3.
+
+#![allow(dead_code)]
+
+use anyhow::{Context, Result};
+use async_trait::async_trait;
+use std::path::PathBuf;
+use std::process::Stdio;
+use tokio::io::AsyncWriteExt;
+use tokio::process::Command;
+
+use super::connection_method;
+use super::{ProverBackend, ProverConfig, ProverKind};
+use crate::core::{Goal, ProofState, Tactic, TacticResult, Term};
+
+/// ileanCoP backend.
+pub struct IleanCopBackend {
+    config: ProverConfig,
+}
+
+impl IleanCopBackend {
+    pub fn new(config: ProverConfig) -> Self {
+        IleanCopBackend { config }
+    }
+}
+
+#[async_trait]
+impl ProverBackend for IleanCopBackend {
+    fn kind(&self) -> ProverKind {
+        ProverKind::IleanCoP
+    }
+
+    async fn version(&self) -> Result<String> {
+        let output = Command::new(&self.config.executable)
+            .arg("--version")
+            .output()
+            .await
+            .context("Failed to run ileancop --version")?;
+        let stdout = String::from_utf8_lossy(&output.stdout);
+        Ok(stdout.lines().next().unwrap_or("ileancop").trim().to_string())
+    }
+
+    async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
+        let content = super::bounded_read_proof_file(&path)
+            .await
+            .context("Failed to read TPTP input")?;
+        let mut state = self.parse_string(&content).await?;
+        state.metadata.insert(
+            "source_path".to_string(),
+            serde_json::Value::String(path.to_string_lossy().into_owned()),
+        );
+        Ok(state)
+    }
+
+    async fn parse_string(&self, content: &str) -> Result<ProofState> {
+        let mut state = ProofState::default();
+        state.metadata.insert(
+            "tptp_source".to_string(),
+            serde_json::Value::String(content.to_string()),
+        );
+        for line in content.lines() {
+            let line = line.trim();
+            if line.is_empty() || line.starts_with('%') {
+                continue;
+            }
+            if line.starts_with("fof(") {
+                if let Some(formula) = line.split(',').nth(2) {
+                    let formula = formula.trim_end_matches(").").trim();
+                    if line.contains(", axiom,") {
+                        state.context.axioms.push(formula.to_string());
+                    } else if line.contains(", conjecture,") {
+                        state.goals.push(Goal {
+                            id: format!("goal_{}", state.goals.len()),
+                            target: Term::Const(formula.to_string()),
+                            hypotheses: vec![],
+                        });
+                    }
+                }
+            }
+        }
+        Ok(state)
+    }
+
+    async fn apply_tactic(&self, _state: &ProofState, _tactic: &Tactic) -> Result<TacticResult> {
+        Err(anyhow::anyhow!(
+            "ileanCoP is fully automated — interactive tactics not supported"
+        ))
+    }
+
+    async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
+        let tptp = connection_method::to_tptp(state);
+        let mut child = Command::new(&self.config.executable)
+            .stdin(Stdio::piped())
+            .stdout(Stdio::piped())
+            .stderr(Stdio::piped())
+            .spawn()
+            .context("Failed to spawn ileancop")?;
+        {
+            let stdin = child
+                .stdin
+                .as_mut()
+                .ok_or_else(|| anyhow::anyhow!("Failed to open ileancop stdin"))?;
+            stdin
+                .write_all(tptp.as_bytes())
+                .await
+                .context("Failed to write to ileancop stdin")?;
+        }
+        let output = child
+            .wait_with_output()
+            .await
+            .context("Failed to wait for ileancop")?;
+        let combined = format!(
+            "{}\n{}",
+            String::from_utf8_lossy(&output.stdout),
+            String::from_utf8_lossy(&output.stderr)
+        );
+        connection_method::parse_szs_or_native(&combined)
+    }
+
+    async fn export(&self, state: &ProofState) -> Result<String> {
+        Ok(connection_method::to_tptp(state))
+    }
+
+    async fn suggest_tactics(
+        &self,
+        _state: &ProofState,
+        _limit: usize,
+    ) -> Result<Vec<Tactic>> {
+        Ok(vec![])
+    }
+
+    async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {
+        Ok(vec![])
+    }
+
+    fn config(&self) -> &ProverConfig {
+        &self.config
+    }
+
+    fn set_config(&mut self, config: ProverConfig) {
+        self.config = config;
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_ileancop_kind() {
+        let config = ProverConfig::default();
+        let backend = IleanCopBackend::new(config);
+        assert_eq!(backend.kind(), ProverKind::IleanCoP);
+    }
+
+    #[tokio::test]
+    async fn test_ileancop_parse_string_extracts_axioms_and_goal() {
+        let config = ProverConfig::default();
+        let backend = IleanCopBackend::new(config);
+        let tptp = "fof(a1, axiom, p => p).\nfof(conj, conjecture, p => p).\n";
+        let state = backend.parse_string(tptp).await.expect("parse_string failed");
+        assert_eq!(state.context.axioms.len(), 1);
+        assert_eq!(state.goals.len(), 1);
+    }
+
+    #[test]
+    fn test_ileancop_export_emits_conjecture() {
+        let config = ProverConfig::default();
+        let _backend = IleanCopBackend::new(config);
+        let mut state = ProofState::default();
+        state.goals.push(Goal {
+            id: "g0".to_string(),
+            target: Term::Const("p => p".to_string()),
+            hypotheses: vec![],
+        });
+        let tptp = connection_method::to_tptp(&state);
+        assert!(tptp.contains("fof(conjecture, conjecture, p => p)."));
+    }
+}