Remove the Mathlib dependency from the Lean packages by achamayou · Pull Request #8702 · microsoft/CCF

Amaury Chamayou (achamayou) · 2026-11-08T16:43:10Z

Motivation

All five Lean packages (common, kv, consistency, disaster-recovery, consensus) depended on Mathlib but used only a handful of its definitions. Every fresh checkout cloned Mathlib and its dependencies into each package and then fetched Mathlib's prebuilt cache. That meant about 7.5 GB in .lake/packages per package, and CI paid for it in every package and trace-replay job. This PR replaces the parts we used with small local versions in lean/common/CCF/ (505 lines) and removes Mathlib from the specification packages. A separate, path-filtered CI job proves the replacements equivalent to the Mathlib definitions they replace.

Results

Summary

CI, Lean workflow (warm cache): total job time across the 8 Lean jobs drops from 1861s to 1012s (-46%). The longest job (consensus) drops from 459s to 259s (-44%).
CI, ci.yml ACI SNP Genoa: the "Build Lean recovery trace replayer" step drops from 107s to 85s.
Newcomer setup (all five packages): dependency download drops from 849 MB to 11 MB. Disk under .lake/packages drops from 36.1 GB to 34 MB (36.7 GB to 0.56 GB after building and linting). Dependency fetch plus first build drops from 23 min to 1.6 min.

CI time: `.github/workflows/lean.yml`

"Before" is the median of 15 successful runs of the same workflow on other open PRs that still depend on Mathlib and are based on recent main (42704196362, 42660899537, 42648080476, 42643390177, 42642153319, 42641356313, 42633945935, 42631611749, 42629351648, 42624452928, 42620159299, 42611960081, 42609299783, 42607468692, 42607116166). The Lean workflow runs only on pull requests, not on main. Run 42704196362 already includes the #8716 deadlock proofs and took 1901s in total, in line with the median. "After, cold" is this PR's run after merging main (42703295047, attempt 1), where every package job missed the dependency cache. "After, warm" is a rerun of the same workflow (attempt 2) with the dependency cache populated, which is the steady state.

Job	Before	After, cold	After, warm	Change (warm)
Lean package (common)	235s	159s	151s	-36%
Lean package (consensus)	459s	295s	259s	-44%
Lean package (consistency)	263s	170s	145s	-45%
Lean package (disaster-recovery)	298s	202s	161s	-46%
Lean package (kv)	304s	176s	154s	-49%
Package jobs, total	1559s	1002s	870s	-44%
Replay KV traces	106s	64s	53s	-50%
Replay consistency traces	84s	26s	28s	-67%
Replay native CCF consensus traces	112s	57s	61s	-46%
Replay jobs, total	302s	147s	142s	-53%
All Lean jobs	1861s	1149s	1012s	-46%

Most of the remaining replay job time is container setup and teardown, installing prerequisites and installing Lean (about 40s per job), which this PR does not change.

These changes account for the savings (medians over the same runs):

Step	Before	After (warm)
"Restore Mathlib cache" (`lake exe cache get`)	41-48s per job, in all 8 jobs	removed
"Restore dependency builds" (actions/cache restore)	1s median, up to 42s	0-3s
"Post Restore dependency builds" (actions/cache save)	15-16s median, up to 235s	0-5s
"Build, kernel and axiom check"	common 150s, consensus 336s, consistency 149s, DR 157s, kv 175s	125s, 218s, 107s, 111s, 110s
"Build * replay" in the replay jobs	KV 29s, consistency 3s, consensus 31s	7s, 4s, 7s

Smaller environments explain the faster build and check step: lake check exports and re-checks the whole import closure, which no longer includes Mathlib. The replay builds get faster because linking a replay executable used to compile the C code of every Mathlib module it imports.

CI time: other workflows

ci.yml, ACI SNP Genoa, "Build Lean recovery trace replayer": median 107s over 6 main runs, against 85s on this PR (run 42703294799). This step no longer clones Mathlib.
doc.yml: conf.py builds the same recovery replayer, so the docs build saves the same Mathlib clone and compile. It is not measured separately because it is folded into the Sphinx step.

Newcomer checkout and setup

The Git checkout itself is unchanged: the lean/ sources grow by about 1.3 KB. All the savings come from what lake fetches and builds afterwards.

I measured this locally from a cold start: a fresh git archive of lean/ and an empty XDG_CACHE_HOME, on a 10-core / 11 GB WSL machine. The script mirrors the CI package job, running each package in turn. "Deps" is lake exe cache get before and lake resolve-deps after. The machine was shared, so these wall-clock times are indicative only; the byte counts are exact.

Package	Deps time	Network download	`.lake/packages`	First `lake build`
common	144s -> 0.2s	519 MB -> 0	7.21 GB -> 0	14s -> 5s
kv	164s -> 5s	111 MB -> 4.5 MB	7.21 GB -> 13 MB	312s -> 22s
consistency	181s -> 2s	76 MB -> 1.1 MB	7.21 GB -> 3.8 MB	26s -> 11s
disaster-recovery	125s -> 5s	72 MB -> 4.4 MB	7.21 GB -> 13 MB	37s -> 22s
consensus	121s -> 2s	72 MB -> 1.0 MB	7.21 GB -> 3.8 MB	251s -> 24s
Total	735s -> 14s	849 MB -> 11 MB	36.1 GB -> 34 MB	641s -> 84s

Mathlib cache: the 463 MB of Mathlib cache files under ~/.cache/mathlib are no longer downloaded. The first package pays for it, and later packages reuse it but still clone Mathlib's Git repository into their own .lake/packages.
Total lean/ tree on disk after building and checking everything: 36.8 GB -> 0.56 GB.
First lake build: kv and consensus build replay executables. Before, that forced compiling the C code of the imported Mathlib modules. After, kv and DR compile Batteries from source in about 15s.
Full local validation (deps, build, lake check, check-imports, lake lint for all five packages): about 65 min -> 29 min. lake check is now the bulk of it (2391s -> 1552s), because the kernel re-checks Lean core itself.

Implementation summary

Mathlib types and definitions replaced

New modules in lean/common/CCF/:

Mathlib	Replacement	Definitions	Properties	Proofs	Notes
`Stream'.Seq`, with `nil`, `cons`, `map`, `ofList`, `ofStream`, `get?`, membership	`CCF.Seq` (`Seq.lean`)	44	21	11	A structure with `get? : Nat -> Option a`, plus a proof that once `get?` returns `none` it stays `none`. Used by `CCF.Execution` traces.
`Finset`, with `insert`, `erase`, `filter`, `union`, `inter`, `sdiff`, subset, `Nonempty`, `Disjoint` and `card`	`CCF.Finset` (`Finset.lean`, lemmas in `Proofs/Finset.lean`)	84	77	136	A strictly sorted list over a `StrictTotalOrder`. The representation is canonical, so `DecidableEq` and `ext` come for free and the kernel can evaluate it directly.
`List.toFinset`	`CCF.Finset.ofList`
`Finset.sort`	`CCF.Finset.sort` (the underlying list)				No sorting is needed at use sites.
`Finset.min` / `WithTop`	`CCF.Finset.min?`				`min = (n : WithTop _)` becomes `min? = some n`, with the same meaning.
`Finset.inter_nonempty_of_card_lt_card_add_card`, `card_union_of_disjoint`, `card_le_card`, etc.	Same names in `CCF.Finset`, declared in `CCF.Proofs.Finset`				Only the lemmas the proofs need.
`Function.update`	`CCF.Function.update` (`Function.lean`)	3	17	7	Same argument order and simp lemmas, including `update_eq_self` and `update_idem`.
`Prod.Lex` / `toLex` (successor ranking)	`rankBelow` in `Consensus/Model/Node.lean`				An explicit lexicographic comparison.
Total		131	115	154

Line counts exclude blank lines, imports, namespaces and module comments. Definitions include docstrings and the proofs that definitions carry, such as Seq's stability proofs. Properties are theorem statements with their docstrings and attributes, and Proofs are theorem bodies. The sortedness theorems in Finset.lean that insert needs count as properties and proofs (4 and 40 lines).

Definitions and theorems in lean/common are now split the same way as in the specification packages:

The theorems in CCF.Finset and CCF.Execution move, under the same names, to CCF.Proofs.Finset and CCF.Proofs.Execution.
Definition modules keep only the proofs their definitions carry, such as Finset's sortedness invariant.
CCF.Seq and CCF.Function keep their few rfl/simp lemmas alongside their definitions.
lake exe check-imports now rejects imports of CCF.Proofs, or of the CCF entrypoint that reexports it, from specification Model modules, and imports of CCF.Proofs from CCF definition modules. It also checks common's own CCF root.
The kv model now imports only CCF.TransitionSystem, which is all it uses.

Mathlib tactics and lemmas rewritten in proofs

Tactics:
- split_ifs -> by_cases/split
- set -> generalize
- nth_rewrite -> rw (occs := ...)
- conv_lhs/conv_rhs -> conv => lhs/rhs
- t <;> [a; b] -> focused bullets
- Mathlib's two-argument congrArg, by_contra and push_neg -> core equivalents
Lemmas:
- generic order and algebra lemmas -> Nat.*
- Mathlib's order dot notation (h.trans, h.le, h.ge, h.trans_le) -> Nat.le_trans, Nat.le_of_lt, Nat.le_of_eq, Nat.lt_of_lt_of_le
- max_choice -> Std.max_eq_or
- le_or_gt -> (Nat.lt_or_ge b a).symm
- goals that rw closed through Mathlib's @[refl] tags (7 proofs) -> explicit Nat.le_refl, List.prefix_refl or List.suffix_refl
- Nat.strong_induction_on -> Nat.strongRecOn
- List.monotone_filter_right -> List.countP_mono_left
- IsPrefix.take -> List.prefix_take_iff
simp calls: a few needed extra lemmas, such as guard and Nat.not_lt_of_le.
lemma declarations: Lean core has no lemma command, so the 280 lemma declarations (276 before merging lean: Prove deadlock freedom for consistency and recovery #8716) become theorem. The statements and proofs are unchanged. lean/AGENT.md now identifies witnesses by their _witness suffix rather than the keyword.
Deadlock-freedom proofs from main (lean: Prove deadlock freedom for consistency and recovery #8716): aesop -> Lean core grind in DisasterRecovery.Proofs.Deadlock, and their witnesses use theorem.
Witnesses hack: the consensus Witnesses workaround that rewrote Finset.sort to insertion sort for kernel evaluation is gone. Its macro is renamed unfold_run.

Equivalence with Mathlib

A new lean/mathlib-equivalence package, the only Lean package that still depends on Mathlib (v4.35.0, as before), proves that the replacements match Mathlib:

Module	CCF definition	Mathlib definition	Result
`MathlibEquivalence.Seq`	`CCF.Seq`	`Stream'.Seq`	An equivalence of types preserving `get?`, `nil`, `cons`, `map`, `ofList`, `ofStream` and membership
`MathlibEquivalence.Finset`	`CCF.Finset`	`Finset` (for a `LinearOrder`)	An equivalence of types preserving membership, empty, singleton, `insert`, `filter`, `erase`, union, intersection, difference, `ofList` (`List.toFinset`), subset, `Nonempty`, `Disjoint`, `card`, `sort` and `min?` (`Finset.min`)
`MathlibEquivalence.Function`	`CCF.Function.update`	`Function.update`	Equal
`MathlibEquivalence.Rank`	`rankBelow`, `findSuccessor`	`toLex`	`rankBelow` is `toLex` comparison, and `findSuccessor` equals its previous `toLex` definition

The new workflow .github/workflows/lean-mathlib-equivalence.yml restores Mathlib's cache, runs lake check (kernel re-check, standard axioms only) and checks formatting. It runs only on pull requests that change CCF/Seq.lean, CCF/Finset.lean, CCF/Function.lean, Consensus/Model/Node.lean, the equivalence package, the toolchain, the format script or the workflow, and can be run manually. The main Lean workflow ignores lean/mathlib-equivalence/**, its package inventory check excludes it, and scripts/lean-format-checks.sh checks it only when asked by name. In CI it takes 275s cold and 230s warm (run 42703294871): about 45s to restore the cached dependency builds, 4s for lake exe cache get and 158s for lake check. The CI time and setup figures above exclude it, since it does not run on most Lean changes and newcomers do not need it.

Dependencies and CI

Mathlib is removed from every lakefile.toml and lake-manifest.json.
kv and disaster-recovery now require Batteries (v4.35.0) directly, for their batteries/runLinter lint driver. The other packages depend only on Lean core and leanfmt.
The four lake exe cache get ("Restore Mathlib cache") steps are removed from lean-package.yml and lean.yml.
The READMEs, .github/workflows/README.md and doc/build_apps/kv/semantics.rst are updated.

Safety and compatibility

There is no runtime impact. Only Lean specifications, proofs, replayers and CI change; no C++ or CCF runtime code is touched.

Theorems: statements are unchanged apart from the types they mention (CCF.Finset, CCF.Seq).
lake check: the kernel re-check passes for every package and target. Axioms used are only propext, Quot.sound and Classical.choice.
Other checks: check-imports, lake lint, leanfmt and the ASCII checks pass.
Mathlib equivalence: lake check on lean/mathlib-equivalence passes locally with only propext, Quot.sound and Classical.choice (about 18.5 min, mostly re-checking imported Mathlib declarations).
Replay fixtures: all pass, both locally and in CI. That covers consensus and consistency (valid and invalid), KV (72/72), DR (419/419), the DR schema check and the viewer dump.
Lint coverage: the kv/DR runLinter loses the Mathlib-only environment linters; the Batteries linters are kept.

Replace the few Mathlib facilities the specifications use with minimal versions in ccf_common: CCF.Seq (Stream'.Seq), CCF.Finset (Finset as strictly sorted lists), CCF.Function (Function.update), CCF.Order (Nat order dot notation and @[refl] tags) and CCF.Lemma (the lemma command). Port the proofs off Mathlib-only tactics and lemmas, keep Batteries for the kv and disaster-recovery lint drivers, and drop the Mathlib cache steps from CI. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: bfc327d9105b46d7a664aadb096fa538

Copilot

🔵 Needs a closer look

Replacing foundational Seq and Finset types changes consensus and recovery theorem domains, requiring human confirmation of semantic equivalence with the former Mathlib models that kernel checks alone cannot establish.

No open issues 🎉

What changed in this PR

Removes Mathlib from CCF's five Lean packages, reducing dependency downloads, disk usage, and verification overhead without changing C++ runtime code.

Changes:

Adds small shared replacements for sequences, finite sets, function updates, order helpers, and lemma syntax.
Migrates models, proofs, tests, and replayers to local definitions and Lean core facilities.
Removes Mathlib dependencies and cache-fetch steps, retains Batteries for KV and disaster-recovery linting, and updates setup documentation.

Custom instructions used: Repository guidance supplied in the review context; no additional instruction files loaded.

File	Description
`lean/kv/README.md`	Removes Mathlib cache setup command.
`lean/kv/lakefile.toml`	Replaces Mathlib with Batteries.
`lean/kv/lake-manifest.json`	Locks Batteries and removes Mathlib dependencies.
`lean/kv/Kv/Properties.lean`	Imports local lemma syntax.
`lean/kv/Kv/Proofs/Witnesses.lean`	Imports local lemma syntax.
`lean/disaster-recovery/README.md`	Updates dependencies and validation instructions.
`lean/disaster-recovery/lakefile.toml`	Replaces Mathlib with Batteries.
`lean/disaster-recovery/lake-manifest.json`	Locks Batteries and removes Mathlib dependencies.
`lean/disaster-recovery/DisasterRecovery/Tests/Trace.lean`	Uses local sequences in trace tests.
`lean/disaster-recovery/DisasterRecovery/Tests/Execution.lean`	Migrates execution tests to local sequences.
`lean/disaster-recovery/DisasterRecovery/Properties.lean`	Imports local lemma syntax.
`lean/disaster-recovery/DisasterRecovery/Proofs/Witnesses.lean`	Constructs witnesses using local sequences.
`lean/disaster-recovery/DisasterRecovery/Proofs/Safety.lean`	Replaces Mathlib sequence, set, and proof facilities.
`lean/disaster-recovery/DisasterRecovery/Proofs/Local.lean`	Adapts local proofs to core simplification.
`lean/disaster-recovery/DisasterRecovery/Proofs/Evaluation.lean`	Uses local sequences for execution construction.
`lean/consistency/README.md`	Updates import guidance and validation commands.
`lean/consistency/lakefile.toml`	Removes Mathlib requirement.
`lean/consistency/lake-manifest.json`	Removes Mathlib dependency tree.
`lean/consistency/consistency/Properties.lean`	Imports local lemma syntax.
`lean/consistency/consistency/Proofs/Witnesses.lean`	Uses core logic and order lemmas.
`lean/consistency/consistency/Proofs/Ordering.lean`	Replaces Mathlib proof helpers with core equivalents.
`lean/consistency/consistency/Proofs/Invalidation.lean`	Replaces Mathlib simplification lemmas.
`lean/consensus/replay/README.md`	Removes Mathlib setup and cache references.
`lean/consensus/README.md`	Updates setup and dependency-import guidance.
`lean/consensus/lakefile.toml`	Removes Mathlib requirement.
`lean/consensus/lake-manifest.json`	Removes Mathlib dependency tree.
`lean/consensus/Consensus/Tests/CanonicalTraces.lean`	Selects the local finite-set type.
`lean/consensus/Consensus/Replay/Reduction.lean`	Builds replay membership sets locally.
`lean/consensus/Consensus/Replay/Interpreter.lean`	Selects the local finite-set type.
`lean/consensus/Consensus/Properties.lean`	Uses local finite sets and lemma syntax.
`lean/consensus/Consensus/Proofs/Witnesses.lean`	Migrates traces and removes the sorting workaround.
`lean/consensus/Consensus/Proofs/SafetyInvariant.lean`	Migrates safety proofs to local and core facilities.
`lean/consensus/Consensus/Proofs/Direct.lean`	Migrates direct proofs to local and core facilities.
`lean/consensus/Consensus/Model/NodeState.lean`	Replaces Mathlib finite-set imports.
`lean/consensus/Consensus/Model/Node.lean`	Uses explicit successor ranking and local function updates.
`lean/consensus/Consensus/Model/ClusterConfig.lean`	Selects the local finite-set type.
`lean/consensus/Consensus/Model.lean`	Uses optional minimum for bootstrap selection.
`lean/common/README.md`	Documents replacement modules and dependency policy.
`lean/common/lakefile.toml`	Removes Mathlib requirement.
`lean/common/lake-manifest.json`	Clears external package dependencies.
`lean/common/CCF/Seq.lean`	Adds finite and infinite sequences with supporting lemmas.
`lean/common/CCF/Order.lean`	Adds natural-number order aliases and reflexivity tags.
`lean/common/CCF/Lemma.lean`	Adds `lemma` as a theorem macro.
`lean/common/CCF/Function.lean`	Adds point updates and supporting lemmas.
`lean/common/CCF/Finset.lean`	Adds sorted finite sets, operations, and proofs.
`lean/common/CCF/Execution.lean`	Migrates shared execution traces to local sequences.
`lean/common/CCF.lean`	Exports the new shared modules.
`doc/build_apps/kv/semantics.rst`	Removes Mathlib cache setup command.
`.github/workflows/README.md`	Documents reduced dependencies and revised CI steps.
`.github/workflows/lean.yml`	Removes cache-fetch steps from replay jobs.
`.github/workflows/lean-package.yml`	Removes cache-fetch step from package verification.

_{Review effort: Balanced}

Lean core has no `lemma` command, so the packages carried a macro that expanded it to `theorem`. Declare those 276 witnesses and supporting proofs with `theorem` instead, remove the shim, and identify witnesses by their `_witness` suffix in lean/AGENT.md. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot

🔵 Needs a closer look

Replacing foundational Finset/Seq types affects consensus and recovery safety proofs, requiring Lean-domain review of semantic equivalence and reported kernel, axiom, and replay checks that could not be independently rerun.

No open issues 🎉

_{Review effort: Balanced}

The packages now require lean/mathlib-subset instead of Mathlib, so CI and local setup no longer clone Mathlib or fetch its build cache. The proofs adopt the Mathlib-free rewrites from #8702 where they reduce what must be vendored. The kv and disaster-recovery packages drop the Batteries runLinter lint driver, which needed full Batteries; Lean's built-in linters still run. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Replace the Nat dot-notation aliases with the core Nat lemmas they wrapped, max_choice with Std.max_eq_or, and le_or_gt with Nat.lt_or_ge. Close the reflexive goals that relied on the @[refl] tags with Nat.le_refl, List.prefix_refl and List.suffix_refl, and remove the CCF.Order module. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot

🟢 Approval recommended

No active review issues are recorded for the removal of Mathlib from the five Lean packages.

No open issues 🎉

_{Review effort: Balanced}

Move the theorems about executions and finite sets out of CCF.Execution and CCF.Finset into CCF.Proofs.Execution and CCF.Proofs.Finset, keeping their names. Definition modules keep only the proofs their definitions carry, such as Finset's sortedness invariant. Extend the architecture check so that specification Model modules, and CCF modules other than the entrypoint and CCF.Proofs, cannot import CCF.Proofs, and run it on the common package's own CCF root too. The kv model now imports only CCF.TransitionSystem, which is all it uses. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: bfc327d9105b46d7a664aadb096fa538

Copilot

🟡 Changes recommended

The import check still allows Model modules to access shared proof modules through the CCF umbrella, bypassing the intended architecture boundary.

1 open issue

Block Model imports of the CCF umbrella module · New

_{Review effort: Balanced}

The CCF entrypoint reexports CCF.Proofs, so importing it from a model would bypass the rule that models depend only on shared definitions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: bfc327d9105b46d7a664aadb096fa538

Copilot · 2026-11-09T17:40:51Z

One or more custom setup steps configured for this repository failed during this Copilot code review run:

Install CI checks dependencies

Setup steps run before each review. If the review above is missing context, or no review was posted at all, the failing step above may be the cause. See the workflow run for failure details, fix your setup steps configuration, and re-request a review.

Note

You can configure setup steps for Copilot code review separately from Copilot cloud agent with a copilot-code-review.yml file. Read the docs for details.

Copilot

🔵 Needs a closer look

Replacing foundational sequence and finite-set representations in the consensus and recovery specifications requires human confirmation of semantic equivalence and the reported kernel/axiom and replay validation.

No open issues 🎉

1 resolved since last review

Block Model imports of the CCF umbrella module

_{Review effort: Balanced}

The packages now require lean/mathlib-subset instead of Mathlib, so CI and local setup no longer clone Mathlib or fetch its build cache. The proofs adopt the Mathlib-free rewrites from #8702 where they reduce what must be vendored. The kv and disaster-recovery packages drop the Batteries runLinter lint driver, which needed full Batteries; Lean's built-in linters still run. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

… job Add a lean/mathlib-equivalence package, the only one that depends on Mathlib, proving that CCF.Seq, CCF.Finset and CCF.Function.update are equivalent to Stream'.Seq, Finset and Function.update, and that rankBelow/findSuccessor match the previous toLex ordering. A separate workflow checks it only when those definitions or the package change. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: bfc327d9105b46d7a664aadb096fa538

Copilot

Note

Copilot was unable to run its full agentic suite in this review.

Copilot review overview

5 open issues

decidable_of_iff expects a Prop, but s.val.all ... is a Bool. This will not typecheck as… · New
This module uses omega (and several other omega calls later) but only imports… · New
This file uses the omega tactic but does not import it, so it likely won't compile. Add the… · New
This is factually inaccurate: Lean supports lemma as a command keyword (it is effectively a… · New
This introduces a dependency on Prod.lexLt, but this file no longer imports… · New

_{Review effort: Lite}

Port the new deadlock-freedom proofs from main off Mathlib: declare the witnesses with theorem, drop the Mathlib.Tactic.Lemma and Aesop imports, and use Lean core's grind instead of aesop. Drop the Mathlib cache step from the new verification docs and keep main's replay README layout. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: bfc327d9105b46d7a664aadb096fa538

Copilot

🔵 Needs a closer look

The finite-set and sequence types underpin consensus quorum and trace properties, requiring Lean-maintainer review of kernel/axiom results and replay validation that could not be independently run in the dependency-free environment.

No open issues 🎉

5 resolved since last review

This file uses the omega tactic but does not import it, so it likely won't compile. Add the…
This module uses omega (and several other omega calls later) but only imports…
decidable_of_iff expects a Prop, but s.val.all ... is a Bool. This will not typecheck as…
This introduces a dependency on Prod.lexLt, but this file no longer imports…
This is factually inaccurate: Lean supports lemma as a command keyword (it is effectively a…

_{Review effort: Balanced}

Resolve the disaster recovery witness conflicts by taking main's generalized statements, declared with theorem. Port main's new GlobalWitnesses proofs off Mathlib: rename lemma to theorem, import CCF.Function, unfold guard in two simp calls, close two reflexive goals explicitly, and add the update_eq_self and update_idem simp lemmas that Mathlib's Function.update provided. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Copilot

🟢 Approval recommended

No active review issues remain for the removal of Mathlib from the five main Lean packages.

No open issues 🎉

_{Review effort: Balanced}

Amaury Chamayou (achamayou) marked this pull request as ready for review November 8, 2026 22:18

Amaury Chamayou (achamayou) requested a review from a team as a code owner November 8, 2026 22:18

Copilot AI balanced review requested due to automatic review settings November 8, 2026 22:18

Copilot started reviewing on behalf of Amaury Chamayou (achamayou) November 8, 2026 22:19

View session

Copilot AI reviewed Nov 8, 2026

View reviewed changes

Copilot AI balanced review requested due to automatic review settings November 9, 2026 13:24

Copilot started reviewing on behalf of Amaury Chamayou (achamayou) November 9, 2026 13:24

View session