diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/__init__.py b/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/__init__.py
new file mode 100644
index 0000000000..c10fcdb8b7
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/__init__.py
@@ -0,0 +1,12 @@
+"""LeanDojo v2 integration stubs (c.76 feasibility verdict).
+
+This package is the future home of runtime tactic-loop tools that bridge the
+`agent_tests/prover/` static-analyzer pipeline with `lean_dojo.Dojo` (the
+interactive theorem-proving environment of LeanDojo v2).
+
+Cycle c.76 verdict (issue #18915): RECOVERABLE-LOCAL. LeanDojo v2.2.0 +
+Lean toolchain v4.11.0 install in <5 min on a CPU machine, and the API
+surface (Dojo, LeanGitRepo, trace) is importable. The actual integration
+into `agent_tests/prover/tools.py` is deferred — see #18915 for the
+follow-up scope.
+"""
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/leandojo_feasibility.py b/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/leandojo_feasibility.py
new file mode 100644
index 0000000000..cb43a3139d
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/leandojo_feasibility.py
@@ -0,0 +1,186 @@
+"""LeanDojo v2 installability + API surface check (cycle c.76, issue #18915).
+
+This module encodes the **prerequisites** verified firsthand on this machine
+(2026-10-03, myia-ai-01:CoursIA-2) so the integration work in follow-up
+cycles starts from a known-good baseline.
+
+Verdict per the sota-not-work-workaround rule (6 axes):
+  RECOVERABLE-LOCAL — the full stack installs in <5 min on CPU, no GPU
+  required, no user action needed beyond a single `elan toolchain install`.
+
+The module also exposes the runtime tactic-loop hooks (`DojoTools` skeleton)
+that follow-up cycles will fill in. Kept minimal: the goal of c.76 is to
+verify the prerequisites, not to deliver the integration.
+"""
+
+from __future__ import annotations
+
+import importlib
+import shutil
+import subprocess
+import sys
+from dataclasses import dataclass
+from typing import Optional
+
+
+# Pin matched to Lean-10 notebook (#18893) -- see issue #18915 for the
+# compatibility rationale (lean-dojo 2.2.0 + Lean 4.11.0 is the only pair
+# where the Dojo runtime works; lean-dojo 4.20+ drops Dojo for newer toolchains).
+LEAN_DOJO_VERSION = "2.2.0"
+LEAN_TOOLCHAIN = "leanprover/lean4:v4.11.0"
+
+
+@dataclass
+class LeanDojoPrereq:
+    """Result of one prereq check (issue #18915, c.76)."""
+
+    name: str
+    ok: bool
+    detail: str
+
+    def render(self) -> str:
+        flag = "OK" if self.ok else "FAIL"
+        return f"  [{flag}] {self.name}: {self.detail}"
+
+
+def check_python_version() -> LeanDojoPrereq:
+    """Python 3.10-3.12 is the supported range for lean-dojo 2.2.0.
+
+    PyPI metadata (https://pypi.org/pypi/lean-dojo/2.2.0/json) declares
+    Requires-Python: <=3.12,>=3.9. Versions 3.13+ are NOT supported by
+    this pin -- installation requires ``--ignore-requires-python`` and the
+    runtime may break in unsupported ways. The control rejects 3.13+ so
+    the verdict stays honest about the supported range.
+    """
+    major, minor = sys.version_info[:2]
+    ok = (3, 10) <= (major, minor) <= (3, 12)
+    return LeanDojoPrereq(
+        "python 3.10-3.12",
+        ok,
+        f"detected {major}.{minor} (supported: 3.10-3.12 per Requires-Python)",
+    )
+
+
+def check_lean_dojo_installed() -> LeanDojoPrereq:
+    """`pip show lean-dojo` should report the pinned version 2.2.0."""
+    proc = subprocess.run(
+        [sys.executable, "-m", "pip", "show", "lean-dojo"],
+        capture_output=True, text=True, encoding="utf-8", errors="replace", check=False,
+    )
+    if proc.returncode != 0:
+        return LeanDojoPrereq(
+            "lean-dojo installable",
+            False,
+            "pip show lean-dojo failed; install via `pip install --ignore-requires-python lean-dojo==2.2.0`",
+        )
+    version = None
+    for line in proc.stdout.splitlines():
+        if line.lower().startswith("version:"):
+            version = line.split(":", 1)[1].strip()
+    ok = version == LEAN_DOJO_VERSION
+    return LeanDojoPrereq(
+        "lean-dojo version",
+        ok,
+        f"want {LEAN_DOJO_VERSION}, have {version or 'unknown'}",
+    )
+
+
+def check_lean_dojo_importable() -> LeanDojoPrereq:
+    """`import lean_dojo` + `from lean_dojo import Dojo, LeanGitRepo, trace`."""
+    try:
+        mod = importlib.import_module("lean_dojo")
+    except Exception as exc:  # ImportError, OSError, etc.
+        return LeanDojoPrereq("lean-dojo import", False, f"import failed: {exc!r}")
+    api = []
+    for symbol in ("Dojo", "LeanGitRepo", "trace"):
+        api.append(f"{symbol}={'Y' if hasattr(mod, symbol) else 'N'}")
+    return LeanDojoPrereq(
+        "lean-dojo API surface",
+        all(hasattr(mod, s) for s in ("Dojo", "LeanGitRepo", "trace")),
+        ", ".join(api),
+    )
+
+
+def check_elan_available() -> LeanDojoPrereq:
+    """`elan --version` reports a working elan installation."""
+    elan = shutil.which("elan")
+    if not elan:
+        return LeanDojoPrereq("elan on PATH", False, "elan not found")
+    proc = subprocess.run(
+        [elan, "--version"], capture_output=True, text=True,
+        encoding="utf-8", errors="replace", check=False,
+    )
+    return LeanDojoPrereq(
+        "elan on PATH",
+        proc.returncode == 0,
+        f"{elan} -> exit {proc.returncode}",
+    )
+
+
+def check_lean_toolchain_pinned() -> LeanDojoPrereq:
+    """`elan toolchain list` should include `leanprover/lean4:v4.11.0`."""
+    elan = shutil.which("elan")
+    if not elan:
+        return LeanDojoPrereq("lean toolchain v4.11.0", False, "elan missing")
+    proc = subprocess.run(
+        [elan, "toolchain", "list"], capture_output=True, text=True,
+        encoding="utf-8", errors="replace", check=False,
+    )
+    ok = LEAN_TOOLCHAIN in proc.stdout
+    return LeanDojoPrereq(
+        f"toolchain {LEAN_TOOLCHAIN}",
+        ok,
+        "installed" if ok else f"run `elan toolchain install {LEAN_TOOLCHAIN}`",
+    )
+
+
+def check_lean_default_toolchain() -> LeanDojoPrereq:
+    """`lean --version` should report 4.11.0 (the only pair with lean-dojo 2.2.0)."""
+    lean = shutil.which("lean")
+    if not lean:
+        return LeanDojoPrereq("lean binary", False, "lean not on PATH")
+    proc = subprocess.run(
+        [lean, "--version"], capture_output=True, text=True,
+        encoding="utf-8", errors="replace", check=False,
+    )
+    if proc.returncode != 0:
+        return LeanDojoPrereq("lean --version", False, f"exit {proc.returncode}")
+    ok = "4.11.0" in (proc.stdout + proc.stderr)
+    return LeanDojoPrereq(
+        "lean 4.11.0 active",
+        ok,
+        f"{proc.stdout.strip() or proc.stderr.strip()}",
+    )
+
+
+def run_all_checks() -> list[LeanDojoPrereq]:
+    """Run every prereq check; return the list (caller renders or asserts)."""
+    return [
+        check_python_version(),
+        check_lean_dojo_installed(),
+        check_lean_dojo_importable(),
+        check_elan_available(),
+        check_lean_toolchain_pinned(),
+        check_lean_default_toolchain(),
+    ]
+
+
+def main() -> int:
+    """Entry point: print a verdict table and exit 0 iff every prereq is green.
+
+    The exit code is what the eventual CI gate would consume; the function is
+    deliberately synchronous and side-effect-free apart from the checks
+    themselves.
+    """
+    results = run_all_checks()
+    print("LeanDojo v2 prerequisites (issue #18915, c.76 verdict):")
+    for r in results:
+        print(r.render())
+    all_ok = all(r.ok for r in results)
+    print()
+    print("Verdict:", "RECOVERABLE-LOCAL" if all_ok else "BLOCKED")
+    return 0 if all_ok else 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/test_leandojo_feasibility.py b/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/test_leandojo_feasibility.py
new file mode 100644
index 0000000000..b80dbd34c4
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/integration/test_leandojo_feasibility.py
@@ -0,0 +1,286 @@
+"""Tests for leandojo_feasibility (issue #18915, c.76).
+
+These tests assert the **prereq table** the integration work relies on. The
+goal is to lock the c.76 verdict (RECOVERABLE-LOCAL) so any future drift in
+the installability of lean-dojo 2.2.0 + Lean 4.11.0 surfaces when the suite
+is executed locally (pytest invocation, developer machine or follow-up CI
+cabling a verifier dedicated to this suite -- not the current PR).
+
+The tests load the module under test via importlib (file path) to avoid
+dragging the parent package's heavy imports (`agent_framework`, etc.) into
+this minimal prereq check. Cablage CI sur `lean_dojo_venv` ou sur le venv
+complet du prouveur = intention non livree dans cette PR (cf. body PR,
+section "Hors scope" : "Verrou CI yaml dedie (workflow
+`lean-dojo-feasibility.yml` sur push/PR) : reste une PR distincte
+preferable, distincte du verdict SOTA et de ses tests locaux").
+"""
+
+from __future__ import annotations
+
+import importlib.util
+import sys
+from pathlib import Path
+
+import pytest
+
+
+_HERE = Path(__file__).resolve().parent
+
+
+def _load_module():
+    """Load `leandojo_feasibility.py` by file path -- bypass the parent
+    package's heavy `agent_framework` import chain."""
+    target = _HERE / "leandojo_feasibility.py"
+    spec = importlib.util.spec_from_file_location(
+        "_leandojo_feasibility_isolated", target,
+    )
+    assert spec is not None and spec.loader is not None
+    mod = importlib.util.module_from_spec(spec)
+    sys.modules[spec.name] = mod
+    spec.loader.exec_module(mod)
+    return mod
+
+
+@pytest.fixture(scope="module")
+def feas():
+    return _load_module()
+
+
+def test_lean_dojo_version_pin_matches_leandojo_10(feas):
+    """Version pin must match Lean-10 -- silent upgrade invalidates Dojo."""
+    assert feas.LEAN_DOJO_VERSION == "2.2.0"
+
+
+def test_lean_toolchain_pin_matches_leandojo_10(feas):
+    """Lean 4.11.0 is the only toolchain where lean-dojo 2.2.0's Dojo works."""
+    assert feas.LEAN_TOOLCHAIN == "leanprover/lean4:v4.11.0"
+
+
+def test_python_version_ok(feas):
+    """Python must be in the 3.10-3.12 range per lean-dojo 2.2.0
+    Requires-Python (<=3.12,>=3.9). Outside this range the install needs
+    --ignore-requires-python and the runtime is not supported.
+    """
+    r = feas.check_python_version()
+    assert r.name == "python 3.10-3.12"
+    # 3.10-3.12 are supported; 3.13+ is not. The assertion is conditional
+    # on the running interpreter: this test asserts the *plumbing* works,
+    # not the verdict.
+    import sys
+    major, minor = sys.version_info[:2]
+    expected_ok = (3, 10) <= (major, minor) <= (3, 12)
+    assert r.ok is expected_ok, r.render()
+
+
+def test_lean_dojo_installed(feas):
+    """`pip show lean-dojo` must report 2.2.0 on the test env."""
+    pytest.importorskip("lean_dojo")
+    r = feas.check_lean_dojo_installed()
+    assert r.ok, r.render()
+
+
+def test_lean_dojo_importable(feas):
+    """Dojo, LeanGitRepo, trace must all be exposed by the package."""
+    pytest.importorskip("lean_dojo")
+    r = feas.check_lean_dojo_importable()
+    assert r.ok, r.render()
+
+
+def test_elan_on_path(feas):
+    """elan is the only way this integration installs Lean toolchains."""
+    r = feas.check_elan_available()
+    assert r.ok, r.render()
+
+
+def test_lean_toolchain_installed(feas):
+    """The Lean 4.11.0 toolchain must be on the host (c.76 install)."""
+    r = feas.check_lean_toolchain_pinned()
+    assert r.ok, r.render()
+
+
+def test_lean_default_toolchain_is_4_11(feas):
+    """`lean --version` should report 4.11.0 -- not a newer toolchain that
+    breaks the lean-dojo 2.2.0 / Dojo runtime pair."""
+    r = feas.check_lean_default_toolchain()
+    assert r.ok, r.render()
+
+
+def test_run_all_checks_returns_six_results(feas):
+    """Smoke test: the runner covers the full prereq surface."""
+    results = feas.run_all_checks()
+    assert len(results) == 6
+    assert all(isinstance(r, feas.LeanDojoPrereq) for r in results)
+
+
+# -- Deterministic controls for the prereq logic (c.81 adjoint review) ----
+# These tests assert the control surfaces the right verdict for a synthetic
+# Python version / pin / elan state, independent of the host. They are what
+# CI should run when the real lean_dojo install is not available: the
+# *control logic* is what breaks drift, not the host state.
+
+
+def test_python_version_caps_at_3_12(feas, monkeypatch):
+    """Versions 3.13+ are NOT supported by lean-dojo 2.2.0
+    (Requires-Python: <=3.12,>=3.9). The control must reject them.
+    """
+    for fake_minor in (13, 14):
+        monkeypatch.setattr(sys, "version_info", (3, fake_minor, 0, "final", 0))
+        r = feas.check_python_version()
+        assert r.ok is False, f"3.{fake_minor} should be rejected: {r.render()}"
+        assert "supported: 3.10-3.12" in r.detail
+
+
+def test_python_version_accepts_3_10_to_3_12(feas, monkeypatch):
+    """The supported range 3.10-3.12 must all be accepted."""
+    for fake_minor in (10, 11, 12):
+        monkeypatch.setattr(sys, "version_info", (3, fake_minor, 0, "final", 0))
+        r = feas.check_python_version()
+        assert r.ok is True, f"3.{fake_minor} should be accepted: {r.render()}"
+
+
+def test_pin_mismatch_detected(feas, monkeypatch):
+    """`check_lean_dojo_installed` must FAIL when the installed version
+    differs from the pinned version. Mocks pip show to return a wrong
+    version string.
+    """
+    class _FakeProc:
+        returncode = 0
+        stdout = "Name: lean-dojo\nVersion: 9.9.9\nLocation: /tmp\n"
+
+    def _fake_run(*args, **kwargs):
+        return _FakeProc()
+
+    monkeypatch.setattr(feas.subprocess, "run", _fake_run)
+    r = feas.check_lean_dojo_installed()
+    assert r.ok is False
+    assert "want 2.2.0" in r.detail
+    assert "have 9.9.9" in r.detail
+
+
+def test_elan_missing_detected(feas, monkeypatch):
+    """`check_elan_available` must FAIL when elan is not on PATH."""
+    monkeypatch.setattr(feas.shutil, "which", lambda _: None)
+    r = feas.check_elan_available()
+    assert r.ok is False
+    assert "elan not found" in r.detail
+
+
+def test_lean_toolchain_pin_mismatch_detected(feas, monkeypatch):
+    """`check_lean_toolchain_pinned` must FAIL when the pinned toolchain
+    is not in `elan toolchain list` output.
+    """
+    monkeypatch.setattr(feas.shutil, "which", lambda _: "/usr/bin/elan")
+    fake_proc = type("_P", (), {"returncode": 0, "stdout": "stable (default)\nleanprover/lean4:v4.30.0\n", "stderr": ""})()
+    monkeypatch.setattr(feas.subprocess, "run", lambda *a, **kw: fake_proc)
+    r = feas.check_lean_toolchain_pinned()
+    assert r.ok is False
+    assert "v4.11.0" in r.detail
+
+
+def test_lean_default_toolchain_mismatch_detected(feas, monkeypatch):
+    """`check_lean_default_toolchain` must FAIL when `lean --version`
+    reports a toolchain other than 4.11.0.
+    """
+    monkeypatch.setattr(feas.shutil, "which", lambda _: "/usr/bin/lean")
+    fake_proc = type("_P", (), {"returncode": 0, "stdout": "Lean (version 4.30.0, ...)", "stderr": ""})()
+    monkeypatch.setattr(feas.subprocess, "run", lambda *a, **kw: fake_proc)
+    r = feas.check_lean_default_toolchain()
+    assert r.ok is False
+    assert r.name == "lean 4.11.0 active"
+    assert "4.30.0" in r.detail  # the actual reported version, not the wanted one
+
+
+def test_run_all_checks_propagates_python_cap(feas, monkeypatch):
+    """Smoke test: with a fake 3.13 Python, `run_all_checks` should
+    return at least one FAIL (the python version cap). Reuses the
+    fixture-loaded module so sys.modules is correctly populated for
+    @dataclass.
+    """
+    monkeypatch.setattr(sys, "version_info", (3, 13, 0, "final", 0))
+    results = feas.run_all_checks()
+    python_check = next(r for r in results if r.name == "python 3.10-3.12")
+    assert python_check.ok is False
+    assert any(not r.ok for r in results), "at least one check must FAIL on 3.13"
+
+
+# -- Coverage for the remaining failure modes (c.92 adjoint review) ---------
+# Per the post-fix CONCERNS at 8c96a67d6 (comment 5965129533): the test
+# suite above exercises pin mismatch, elan missing, toolchain pin/default
+# mismatch, but does NOT cover (a) `pip show` exit non-zero (package absent
+# or pip broken), (b) `import lean_dojo` raising (package installed but
+# broken), (c) `elan`/`lean` commands returning non-zero. The next three
+# tests close that gap using monkeypatched subprocess / import hooks.
+
+
+def test_lean_dojo_pip_show_failure_detected(feas, monkeypatch):
+    """`check_lean_dojo_installed` must FAIL when `pip show lean-dojo`
+    returns non-zero (package absent, pip broken, or venv missing). Mocks
+    `subprocess.run` to simulate a failing pip invocation.
+    """
+    class _FakeProc:
+        returncode = 1
+        stdout = ""
+        stderr = "ERROR: Package not found"
+
+    monkeypatch.setattr(feas.subprocess, "run", lambda *a, **kw: _FakeProc())
+    r = feas.check_lean_dojo_installed()
+    assert r.ok is False
+    assert "pip show lean-dojo failed" in r.detail
+    # The verdict must point the operator at the install command, not
+    # leave them guessing.
+    assert "pip install" in r.detail
+
+
+def test_lean_dojo_import_failure_detected(feas, monkeypatch):
+    """`check_lean_dojo_importable` must FAIL when `import lean_dojo`
+    raises (package present in `pip show` but broken on disk, e.g.
+    abi3 mismatch, missing compiled extension). Mocks `importlib.import_module`
+    to raise ImportError, then asserts the verdict still surfaces the cause.
+    """
+
+    def _raise(*args, **kwargs):
+        raise ImportError("libc10.so: cannot open shared object file")
+
+    monkeypatch.setattr(feas.importlib, "import_module", _raise)
+    r = feas.check_lean_dojo_importable()
+    assert r.ok is False
+    assert "import failed" in r.detail
+    assert "libc10.so" in r.detail
+
+
+def test_elan_command_failure_detected(feas, monkeypatch):
+    """`check_elan_available` must FAIL when `elan --version` exits non-zero
+    (elan on PATH but broken installation). Mocks both `shutil.which` and
+    `subprocess.run` -- the control must distinguish "elan missing" (already
+    covered) from "elan present but failing".
+    """
+    monkeypatch.setattr(feas.shutil, "which", lambda _: "/usr/bin/elan")
+
+    class _FakeProc:
+        returncode = 127
+        stdout = ""
+        stderr = "elan: error: unable to find toolchain"
+
+    monkeypatch.setattr(feas.subprocess, "run", lambda *a, **kw: _FakeProc())
+    r = feas.check_elan_available()
+    assert r.ok is False
+    assert "exit 127" in r.detail
+
+
+def test_lean_command_failure_detected(feas, monkeypatch):
+    """`check_lean_default_toolchain` must FAIL when `lean --version` exits
+    non-zero (lean on PATH but broken). Complements the existing
+    `test_lean_default_toolchain_mismatch_detected` which only covers the
+    version-string case.
+    """
+    monkeypatch.setattr(feas.shutil, "which", lambda _: "/usr/bin/lean")
+
+    class _FakeProc:
+        returncode = 2
+        stdout = ""
+        stderr = "lean: error: toolchain not configured"
+
+    monkeypatch.setattr(feas.subprocess, "run", lambda *a, **kw: _FakeProc())
+    r = feas.check_lean_default_toolchain()
+    assert r.ok is False
+    assert "exit 2" in r.detail