diff --git a/docs/runtimes.md b/docs/runtimes.md
index 3c69db09..5b08e027 100644
--- a/docs/runtimes.md
+++ b/docs/runtimes.md
@@ -28,8 +28,8 @@ When enabled, the compiler:
 - Defaults to the `stable` toolchain; if a `lean-toolchain` file exists in the repo, elan overrides to that version automatically
 - Auto-adds `lean`, `lake`, and `elan` to the bash command allow-list
 - Adds Lean-specific domains to the network allowlist: `elan.lean-lang.org`, `leanprover.github.io`, `lean-lang.org`
-- Symlinks lean tools into `/tmp/awf-tools/` for AWF chroot compatibility
-- Appends a prompt supplement informing the agent about Lean 4 availability and basic commands
+- Installs elan into the default `$HOME/.elan` location and prepends `$HOME/.elan/bin` to the pipeline `PATH` via `##vso[task.prependpath]`. AWF captures the host `PATH` into `AWF_HOST_PATH` and re-exports it inside the chroot, so `lean`/`lake`/`elan` are reachable from the agent sandbox without further configuration
+- Appends a prompt supplement informing the agent that Lean 4 is available on `PATH`
 - Emits a compile-time warning if `tools.bash` is empty (Lean requires bash access)
 
 **Note:** In the 1ES target, the bash command allow-list is updated but elan installation must be done manually via `steps:` front matter. The 1ES target handles network isolation separately.
diff --git a/src/runtimes/lean/extension.rs b/src/runtimes/lean/extension.rs
index f510c19e..2ce1081a 100644
--- a/src/runtimes/lean/extension.rs
+++ b/src/runtimes/lean/extension.rs
@@ -45,9 +45,9 @@ impl CompilerExtension for LeanExtension {
 \n\
 ## Lean 4 Formal Verification\n\
 \n\
-Lean 4 is installed and available. Use `lean` to typecheck `.lean` files, \
-`lake build` to build Lake projects, and `lake env printPaths` to inspect \
-the toolchain. Lean files use the `.lean` extension.\n"
+Lean 4 is installed and available on `PATH`. Use `lean` to typecheck `.lean` \
+files, `lake build` to build Lake projects, and `lake env printPaths` to \
+inspect the toolchain. Lean files use the `.lean` extension.\n"
                 .to_string(),
         )
     }
diff --git a/src/runtimes/lean/mod.rs b/src/runtimes/lean/mod.rs
index 9c37e62c..a61ed9fa 100644
--- a/src/runtimes/lean/mod.rs
+++ b/src/runtimes/lean/mod.rs
@@ -5,8 +5,13 @@
 //! allowlist, extends the bash command allow-list, and appends a prompt
 //! supplement informing the agent that Lean is available.
 //!
-//! Lean is installed via elan (the Lean toolchain manager) into `$HOME/.elan/bin`,
-//! then symlinked into `/tmp/awf-tools/` for AWF chroot compatibility.
+//! Lean is installed via elan (the Lean toolchain manager) into the default
+//! `$HOME/.elan` location, and `$HOME/.elan/bin` is added to the pipeline `PATH`
+//! via `##vso[task.prependpath]`. AWF captures the host runner's `PATH` (and
+//! any entries written to `$GITHUB_PATH`) into `AWF_HOST_PATH`, which the AWF
+//! agent entrypoint exports as `PATH` inside the chroot — so the lean/lake
+//! wrappers and the toolchain they re-exec into are reachable from the agent
+//! sandbox without any extra mounting or symlinking.
 
 pub mod extension;
 
@@ -81,27 +86,29 @@ pub const LEAN_BASH_COMMANDS: &[&str] = &["lean", "lake", "elan"];
 
 /// Generate the elan installation step for Lean 4.
 ///
-/// Installs elan (Lean toolchain manager) and the specified toolchain.
+/// Installs elan (Lean toolchain manager) and the specified toolchain into
+/// the default `$HOME/.elan` location, then prepends `$HOME/.elan/bin` to the
+/// pipeline `PATH` via `##vso[task.prependpath]`. AWF captures the host
+/// runner's `PATH` (and `$GITHUB_PATH` entries) into `AWF_HOST_PATH` and
+/// re-exports it as `PATH` inside the chroot, so `lean`/`lake`/`elan` are
+/// reachable from inside the agent sandbox without further configuration.
+///
 /// Defaults to "stable" if no toolchain is specified in the front matter.
-/// Symlinks lean tools into `/tmp/awf-tools/` for AWF chroot compatibility.
 pub fn generate_lean_install(config: &LeanRuntimeConfig) -> String {
     let toolchain = config.toolchain().unwrap_or("stable");
     let script = format!(
         "\
-curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain {toolchain}
+# Install elan (Lean toolchain manager) into the default $HOME/.elan location.
+# Prepending $HOME/.elan/bin to the pipeline PATH via ##vso[task.prependpath]
+# is enough — AWF captures the host PATH into AWF_HOST_PATH and re-exports it
+# as PATH inside the agent chroot, so lean/lake/elan are reachable in the
+# sandbox without any extra mounting.
+curl https://elan.lean-lang.org/elan-init.sh -sSf \\
+  | sh -s -- -y --default-toolchain {toolchain}
 echo \"##vso[task.prependpath]$HOME/.elan/bin\"
 export PATH=\"$HOME/.elan/bin:$PATH\"
 lean --version || echo \"Lean installed via elan\"
-lake --version || echo \"Lake installed via elan\"
-# Symlink lean tools into /tmp/awf-tools/ so they are accessible
-# inside the AWF chroot (AWF mounts /tmp but reconstructs PATH
-# from standard system locations, excluding $HOME/.elan/bin).
-for cmd in lean lake elan; do
-  if command -v \"$cmd\" >/dev/null 2>&1; then
-    ln -sf \"$(command -v \"$cmd\")\" \"/tmp/awf-tools/$cmd\"
-  fi
-done
-echo \"Lean tools symlinked to /tmp/awf-tools/\""
+lake --version || echo \"Lake installed via elan\""
     );
     // Indent each line of the script body by 4 spaces for YAML block scalar
     let indented: String = script