lake build fails with 'no such file or directory (error code: 2)' on Apple Silicon

## Description

`lake build` fails for any module target with a generic "no such file or directory" error. This is reproducible across multiple files (tested with both existing `522.lean` and new `524.lean`), so it is an environmental issue rather than a file-specific one.

## Steps to Reproduce

```bash
git clone https://github.com/google-deepmind/formal-conjectures.git
cd formal-conjectures
lake build FormalConjectures.ErdosProblems.522
```

## Expected Behavior

Build succeeds (or fails with Lean compilation errors).

## Actual Behavior

```
✔ [0/2] Ran job computation
✔ [1/2] Ran formal_conjectures:extraDep
✖ [2/2] Running FormalConjectures.ErdosProblems.522
error: no such file or directory (error code: 2)
file:
Some required targets logged failures:
- FormalConjectures.ErdosProblems.522
error: build failed
```

Note that `lake env lean FormalConjectures/ErdosProblems/522.lean` succeeds — only `lake build` fails.

The same failure occurs for any module target (e.g., `FormalConjectures.ErdosProblems.524`).

## Environment

- **Platform:** macOS (Darwin 25.4.0), Apple Silicon (arm64)
- **Lean toolchain:** leanprover/lean4:v4.27.0 (from `lean-toolchain`)
- **Lake:** version 5.0.0-src+db93fe1 (Lean version 4.27.0)
- **elan installed toolchains:** v4.27.0, v4.28.0, v4.29.0, v4.29.0-rc8, v4.29.1 (stable)

## Verbose trace (`lake build -v`)

```
✔ [0/2] Ran job computation
✔ [1/2] Ran formal_conjectures:extraDep
✖ [2/2] Running FormalConjectures.ErdosProblems.524
error: no such file or directory (error code: 2)
file:
```

The `file:` field is empty, suggesting Lake is attempting to invoke a binary or path that doesn't resolve on this platform.

## Suspected Cause

Likely a Lake/elan toolchain resolution issue specific to Apple Silicon (arm64-apple-darwin). The `extraDep` step succeeds but the subsequent module compilation step fails to locate a required binary or path.