Forward-port to Lean/mathlib v4.31.0#830
Merged
Merged
Conversation
Forward-ports the library from Lean/mathlib v4.29.0 to v4.31.0 on top of current master (which already includes the FormalizedFormalLogic#794 FirstOrder redesign and the FormalizedFormalLogic#829 ProvabilityLogic removal). - Config bump: lean-toolchain, lakefile.toml (mathlib + doc-gen4 pinned to v4.31.0), lake-manifest.json regenerated. - Source changes to build green on v4.31.0. Whole library builds green (1730/1730 targets). No new proof holes: the sorry/admit count is unchanged versus the base commit. Recurring change patterns: - `simpa … using X` -> `simpa … using! X` (v4.31 needs the defeq-close hatch where the elaborated term is defeq but not syntactically equal to the goal). - `coe_injective'` -> `coe_injective` on mathlib FunLike/SetLike instance bodies (field renamed upstream). - Bare `zero_le a` -> `Arithmetic.zero_le a` across the arithmetic tree (mathlib's `zero_le` now shadows the protected Foundation lemma). - `instance` -> `lemma`/`def` where v4.31's stricter instance checker rejects a non-typeclass return type (`.Nonempty`, `.Countable`) or a hypothesis it cannot infer. - `Function.comp_def` added to simp sets for `f ∘ v` vs pointwise mismatches. - `Nat.testBit` / `Nat.bitIndices` API update in Proof/Coding. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Closed
SnO2WMaN
added a commit
that referenced
this pull request
Jul 2, 2026
Resolve modify/delete conflicts (from #830 v4.31.0 forward-port and later master commits) in favor of removing InterpretabilityLogic: keep the whole Foundation/InterpretabilityLogic tree deleted. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QDE3PcJrxn8nz7V5hJTbjH
This was referenced Jul 3, 2026
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.
Forward-ports the library from Lean/mathlib v4.29.0 → v4.31.0, on top of current
master(c089e7ab, which already includes the #794 FirstOrder redesign and #829 ProvabilityLogic removal).What changed
lean-toolchain,lakefile.toml(mathlib + doc-gen4 → v4.31.0),lake-manifest.jsonregenerated.Foundation.lean: regenerated vialake exe mk_all --module(v4.31 module-system header).Verification
axiom/sorry/admit. The only additions are 5 small proved helpers/compat-shims; severalinstances becamedef/lemma(same names) under v4.31's stricter instance checker.Recurring change patterns
simpa … using e→simpa … using! e— v4.31 tightenedsimpa's final match to reducible transparency;using!opts back into semireducible, so goals that hold only up to unfolding a semireducible def still close.coe_injective'→coe_injective(mathlib FunLike/SetLike field rename).zero_le a→Arithmetic.zero_le a(mathlib'szero_lenow shadows the protected lemma).instance→lemma/defwhere v4.31's instance checker rejects a non-typeclass return type or an uninferable hypothesis.Function.comp_defadded to simp sets;Nat.testBit/Nat.bitIndicesAPI update inProof/Coding.Related work
Semiterm.Operator.val) rather thanusing!.🤖 Generated with Claude Code