ArghDA M6: Lean4 backend + honest cross-backend check verdicts#38
Merged
Conversation
The sixth backend, and a soundness-honesty fix it exposed. ## Lean4 backend (src/prover/lean.rs) `lean <file>` elaboration. The subtlety Lean forces us to be honest about: a green exit does NOT mean proven — `sorry` is only a *warning* and still exits 0. So the verdict is parsed from output, not the bare exit code: - exit non-zero → Error (elaboration failed) - exit 0 + `sorry` in output → Admitted (a hole rode along) - exit 0 clean → Unknown — elaborated, but arghda refuses to claim Proven without a `#print axioms` audit (it could still use native_decide / sorryAx). This is exactly the plan's "honest Unknown when the audit is absent". Dotted modules reuse `graph::module_name_of`; `.lean` `module_to_path`; import parser for top-level `import Mod` (`open` is a namespace directive, NOT an edge — deliberately ignored); `Main.lean` root discovery. `src/lint/lean.rs`: `LeanEscapeHatch` (sorry/admit/native_decide/unsafe), named `escape-hatch` to reuse the reasoning-graph amber cap. Wired via `--backend lean4`. Ground-truthed against Lean 4.13.0. ## Honesty fix exposed by M6 (applies to ALL backends) `check`'s verdict was collapsing to proven-eligible/rejected, which mislabelled a *clean, correct* Lean file as "rejected" and an SMT `sat` as "rejected". It now reports the real verdict word — proven-eligible / refuted / unknown / admitted / postulated / rejected — and the human line drops the assistant-centric ok/FAILED. ## Verified (ran, not inferred) - `cargo test` → 119 passing, 0 failed (+5 lean unit, +4 lean-escape unit, +2 lean integration). - clippy -D warnings, fmt, SPDX clean. - Dogfooded REAL lean: clean proof → `unknown`, `sorry` → `admitted`; re-dogfooded z3 `sat` → `refuted`, `unsat` → `proven-eligible`, agda → `proven-eligible`. `arghda doctor` → 6 backends. - STATE.a2ml records M6 = 85% (lake-env multi-file resolution + the #print axioms audit to promote Unknown→Proven are the follow-on 15%). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
hyperpolymath
marked this pull request as ready for review
July 1, 2026 09:31
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What & why
The sixth backend — Lean4 — plus a soundness-honesty fix it exposed.
Lean4 backend
lean <file>elaboration. The subtlety Lean forces us to be honest about: a green exit does not mean proven —sorryis only a warning and still exits 0. So the verdict is parsed from output, not the bare exit code:sorryin output → Admitted (a hole rode along)Provenwithout a#print axiomsaudit (it could still usenative_decide/sorryAx). Exactly the plan's "honest Unknown when the audit is absent".Dotted modules reuse
graph::module_name_of;.leanmodule_to_path; import parser for top-levelimport Mod(openis a namespace directive, not an edge — deliberately ignored);Main.leanroot discovery.LeanEscapeHatch(sorry/admit/native_decide/unsafe), namedescape-hatchto reuse the amber cap. Wired via--backend lean4. Ground-truthed against Lean 4.13.0.Honesty fix exposed by M6 (all backends)
check's verdict was collapsing to proven-eligible/rejected — which mislabelled a clean, correct Lean file asrejected, and an SMTsatasrejected. It now reports the real verdict word (proven-eligible / refuted / unknown / admitted / postulated / rejected), and the human line drops the assistant-centric ok/FAILED.Verified (ran, not inferred)
cargo test→ 119 passing, 0 failed (+5 lean unit, +4 lean-escape unit, +2 lean integration).unknown,sorry→admitted; re-dogfoodedz3 sat→refuted,z3 unsat→proven-eligible,agda→proven-eligible.arghda doctor→ 6 backends runnable.Honest scope
M6 = ~85%. Follow-on 15%: lake-env/
LEAN_PATHfor project-wide multi-file resolution, and the per-declaration#print axiomsaudit to promoteUnknown→Proven.Milestone status
Six backends across both interaction models. Next: M11 (studio JSON freeze + Groove manifest — the last open v0.1 milestone), M7 (Echidna seam).
Generated by Claude Code