feat: Lean 4 + mathlib portfolio backend#549
Conversation
|
Warning Rate limit exceeded
You’ve run out of usage credits. Purchase more in the billing tab. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (18)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ba684683a2
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| Term::Let { bindings, body } => { | ||
| for binding in bindings { | ||
| collect_term(&binding.bound_term, ctx, bound, None)?; | ||
| bound.insert(lean_ident(&binding.name), "Int".to_string()); |
There was a problem hiding this comment.
The collector hard-codes every let binding to Int, which corrupts signature inference for non-Int bindings used later in predicates/functions. For example, let b := true; P b will register P as Int -> Prop even though b is Bool, causing Lean type errors and turning otherwise solvable obligations into Undecidable. This affects any obligation that uses Term::Let with non-integer values.
Useful? React with 👍 / 👎.
| } | ||
|
|
||
| pub fn uses_sorry_or_sorry_ax(source: &str, output: &str) -> bool { | ||
| source.contains("sorry") |
There was a problem hiding this comment.
sorry as a token, not any substring
The discharge check marks proofs as undecidable when the generated source merely contains the substring "sorry", even if Lean succeeded and no sorry/sorryAx was used. A benign identifier like sorry_count in IR names will trigger this path and force Undecidable, creating false negatives for valid proofs.
Useful? React with 👍 / 👎.
New IR compiler crate parallel to the Coq compiler: lowers an obligation to a Lean 4 theorem with mathlib automation. New lean.rs solver adapter. Verdict is Discharged only if kernel-checked with no sorryAx; receipt records Lean version + mathlib commit + #print axioms trust base. Registered in the multi-solver portfolio (config/dispatch/registry/plan). Spec doc and install appendix included; Dockerfile not modified. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 participant
Summary
Adds Lean 4 + mathlib as a prove-portfolio backend, parallel to the existing Coq backend.
provekit-ir-compiler-lean(new crate): lowers an obligation to a Lean 4theoremwith theIrFormulaas the goal, plus a mathlib-automation tactic block (or asorry-flagged scaffold when no automation applies, which yieldsUnknown, neverDischarged). Byte-deterministic output; declares coverage fordependent_typeandcategorical_structureopacity positions plus general higher-order goals mathlib can close.solvers/lean.rs: invokeslake env lean. Exit 0, no errors, nosorry/sorryAxin#print axioms=>Discharged; otherwiseUnknown. The discharge receipt records the Lean toolchain version, the mathlib commit (fromlake-manifest.json), the emitted.leanfile CID, and the#print axiomsaxiom set as the proof's trust base.config/dispatch/registry/plan/mod);.provekit/config.tomlportfolio now includeslean.protocol/specs/2026-05-10-lean-backend.md; install appendixtools/portfolio/lean-mathlib-install.md(elan+ pinned Lean 4 +lake exe cache getfor the prebuilt mathlib oleans; the Dockerfile is not modified here).Why Lean and not just Coq: mathlib already contains most of the categorical machinery paper 13 references (
CategoryTheory,Algebra.Category,FreeAlgebra), so morphism-composition functoriality and initial-algebra universality become "cite the mathlib lemma" rather than reproving in Coq from scratch.Verification (local):
cargo build -p provekit-ir-compiler-lean -p provekit-verifierclean;cargo test -p provekit-ir-compiler-lean6 pass;cargo test -p provekit-verifier --test lean_solver5 pass + 1 ignored (binary-dependent);cargo test -p provekit-verifier --lib44 pass;cargo test -p provekit-verifier --test multi_solver_modes12 pass;cargo clippy -p provekit-ir-compiler-lean -- -D warningsclean.Test plan
cargo test -p provekit-ir-compiler-leanandcargo test -p provekit-verifiergreencargo clippy -p provekit-ir-compiler-lean -- -D warningscleanelan+ Lean 4 + mathlib cache installed: a known mathlib theorem lowered as an obligation discharges and#print axiomsshows nosorryAx🤖 Generated with Claude Code