08faf05ff0
Replace drift-prone test/crate counts with shape descriptions in map/ROADMAP.md and three jouleclaw crate READMEs so the repo passes scripts/check-no-vanity-metrics.sh (the "describe the shape, not the size" rule). No content meaning lost — "green / zero warnings" signals retained. Co-Authored-By: Claude Opus 4.8 <[email protected]>
42 lines
1.6 KiB
Markdown
42 lines
1.6 KiB
Markdown
# 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)
|