Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests Projects Releases 17 Packages Wiki Activity Actions 153
open-standards/jouleclaw/jouleclaw-rs/crates/jouleclaw-oracle-lean/README.md
Transaction Science 08faf05ff0 docs: drop vanity test-counts (no-vanity-metrics policy) 
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]>
2026-06-07 19:00:28 -04:00

1.6 KiB
Raw Permalink Blame History

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:

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)