# jouleclaw-oracle-lean

**Scope**: `jouleclaw-oracle::Oracle` impl backed by a Lean 4
toolchain. The candidate's `content` is written to a temp file;
`lean` is invoked; exit code maps to `Verdict { Pass | Fail }`.

## Relation to `jouleclaw-formalize`

These two crates are **complementary, not duplicative**. They
gate different stages of the same proof chain:

1. **Informal claim → Lean source** (translation): the
   *faithfulness* gate. `jouleclaw-formalize::FaithfulnessChecker`
   verifies that the Lean encoding actually expresses the
   English claim the human intended. Without this, you can
   rigorously prove the wrong theorem.

2. **Lean source → exit code** (compilation): the *correctness*
   gate. This crate's `LeanOracle::verify` invokes the compiler
   and treats `exit 0` as proof acceptance.

A production proof-carrying-code pipeline runs BOTH:

```text
claim --[jouleclaw-formalize]--> Lean source --[jouleclaw-oracle-lean]--> Verdict
            ^                                          ^
       faithfulness                              compiler exit
```

If you skip `jouleclaw-formalize`, the `Verdict::Pass` from this
crate means "this Lean source compiles" — not "the Lean source
proves the claim the user actually made." That distinction is
the same distinction the AlphaProof / AlphaGeometry literature
makes: compiler feedback only rules out hallucinations *if* the
formalization is faithful.

## What ships

- `LeanOracle` (Oracle trait impl)
- `LeanOracleConfig` { toolchain, timeout, workdir, extra_flags }
- `LeanOracleError` { ToolchainMissing | Io | Timeout }
- Mock-lean test harness (no real Lean install required)