feat: bump lean version by dhsorens · Pull Request #176 · Verified-zkEVM/CompPoly

dhsorens · 2026-03-28T19:43:15Z

Thanks Claude! Bumps to v4.29.0-rc6

CHANGELOG

Lean v4.28.0 → v4.29.0-rc6; Mathlib v4.28.0 → v4.29.0-rc6; ExtTreeMapLemmas v4.28.0-patch-1 → v4.29.0-rc6 (lean-toolchain, lakefile.lean, lake-manifest.json).
36 Lean files touched: mostly tactic/instance fixes (rw → erw, Quotient.eq → Quotient.sound on quotient descent lemmas, stricter simp → dropped unused args, simp (config := { failIfUnchanged := false }), higher maxHeartbeats / maxSteps where needed).
set_option backward.isDefEq.respectTransparency false (file-scoped): Fields/Binary/Tower/Concrete/{Field,Algebra,Basis}.lean, Fields/Binary/Tower/Equiv.lean; scoped on theorems in Tower/Abstract/Basis.lean, Tower/Support/Preliminaries.lean, ToMathlib/MvPolynomial/Equiv.lean (support_finSuccEquivNth).
@[reducible] added on various class-valued defs (e.g. Data/RingTheory/AlgebraTower.lean toAlgebra + AlgebraTowerEquiv algebra defs; abstract/concrete binary tower algebra/module/scalar-tower helpers; Concrete/Core mkAddCommGroup/mkRing/mkDivisionRing/mkField; Concrete/Field liftConcreteBTField).
noncomputable: CBivariate.ofPoly; CMvPolynomial.degreeOf / degrees / vars; getBTFResult; Fintype instances for ConcreteBTField k and test BTF₃.
Lawful.lean / Unlawful.lean: set_option allowUnsafeReducibility true + attribute [local reducible] instDecidableEqOfLawfulBEq; mem_iff / zero_eq_empty proof tweaks.
Mathlib renames in proofs: Nat.cast_le → ENat.coe_le_coe (ENat floor lemma); Array.sum_eq_sum_toList → Array.sum_toList; List.extract_eq_drop_take → List.extract_eq_take_drop.
ENNReal.mul_inv_rev_ENNReal: statement now only ha : a ≠ 0 (drops hb); proof via ENNReal.mul_inv.
Binary tower / GHASH / NTT / multilinear / mv poly equiv: assorted erw, convert, conv, and simp list edits; NovelPolynomialBasis: degree_Xⱼ WithBot cast path reworked, redundant CoeffVecSpace AddCommGroup instance removed, toCoeffsVec.map_smul' unfolded; Split.lean unique_linear_decomposition_succ and split_algebraMap_eq_zero_x proofs reworked.
Multivariate/MvPolyEquiv/Instances.lean: Finsupp.single/single_eq_* steps adjusted for new simp behavior.
Rename.lean: toFinsupp_zero finishes with Vector.getElem_zero.
Tests Univariate/Linear.lean: test-local BEq defs @[reducible]; LawfulBEq proofs use erw on beq unfolds.

github-actions · 2026-03-28T19:45:17Z

🤖 Gemini PR Summary

Toolchain & Infrastructure

Version Bump: Updates lean-toolchain, lakefile.lean, and lake-manifest.json to Lean 4 v4.29.0-rc6 and Mathlib v4.29.0-rc6.
Dependency Alignment: Synchronizes ExtTreeMapLemmas to version v4.29.0-rc6.

Typeclass Resolution & Reducibility

Reducibility Adjustments:
- Marked class-valued definitions as @[reducible] to facilitate instance resolution, including toAlgebra, AlgebraTowerEquiv, and field construction helpers (mkAddCommGroup, mkRing, mkDivisionRing, mkField, liftConcreteBTField).
- Applied set_option allowUnsafeReducibility true and local reducible for instDecidableEqOfLawfulBEq in Lawful.lean and Unlawful.lean.
Transparency Control: Introduced set_option backward.isDefEq.respectTransparency false in files related to Binary Towers and MvPolynomial equivalences to maintain compatibility with Lean 4.29's unification behavior.

Proof Maintenance & Tactic Adjustments

Tactic Migrations:
- Migrated numerous proofs from rw to erw and updated quotient descent lemmas to use Quotient.sound instead of Quotient.eq.
- Adjusted simp calls to handle stricter behavior, utilizing (config := { failIfUnchanged := false }) and removing unused arguments.
- Increased maxHeartbeats and maxSteps for resource-intensive proofs in the binary tower implementation.
Mathlib Alignment:
- Updated lemma references for compatibility: Nat.cast_le → ENat.coe_le_coe, Array.sum_eq_sum_toList → Array.sum_toList, and List.extract_eq_drop_take → List.extract_eq_take_drop.
- Updated ENNReal.mul_inv_rev_ENNReal by removing the redundant hypothesis hb : b ≠ 0.

Mathematical Refactoring

Computability Markers: Marked CBivariate.ofPoly, CMvPolynomial.degreeOf, degrees, vars, getBTFResult, and Fintype instances for ConcreteBTField as noncomputable.
Binary Tower & NTT:
- Reworked NovelPolynomialBasis degree cast paths and removed redundant AddCommGroup instances for CoeffVecSpace.
- Refined proofs for unique_linear_decomposition_succ and split_algebraMap_eq_zero_x.
- Adjusted Finsupp.single and single_eq_* steps in Multivariate/MvPolyEquiv/Instances.lean to align with new simplifier behavior.

Discrepancy Note: The draft summary indicates systematic universe generalization (Type to Type*) and specific generalization of Unlawful lemmas to AddZeroClass. These changes are not explicitly mentioned in the PR body or changelog.

Warning: No sorry or admit placeholders were introduced in this PR. All modified proofs have been successfully closed under the updated toolchain.

Statistics

Metric	Count
📝 Files Changed	42
✅ Lines Added	318
❌ Lines Removed	298

Lean Declarations

✏️ **Removed:** 20 declaration(s)

def mkFieldInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Field (ConcreteBTField k) where in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
def BTField.isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) in CompPoly/Fields/Binary/Tower/Abstract/Basis.lean
def mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Ring (ConcreteBTField k) where in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
def degrees {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Multiset (Fin n) in CompPoly/Multivariate/CMvPolynomial.lean
def ofPoly {R : Type*} [BEq R] [LawfulBEq R] [Nontrivial R] [Semiring R] in CompPoly/Bivariate/ToPoly.lean
instance instFintype {k : ℕ} : Fintype (ConcreteBTField k) in CompPoly/Fields/Binary/Tower/Concrete/Field.lean
def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (BTField l) (BTField r) in CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean
def mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
def isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) in CompPoly/Fields/Binary/Tower/Concrete/Basis.lean
def liftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult (k in CompPoly/Fields/Binary/Tower/Concrete/Field.lean
def binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r) in CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean
def getBTFResult (k : ℕ) : ConcreteBTFStepResult k in CompPoly/Fields/Binary/Tower/Concrete/Field.lean
def degreeOf {R : Type} {n : ℕ} [Zero R] (i : Fin n) : CMvPolynomial n R → ℕ in CompPoly/Multivariate/CMvPolynomial.lean
def ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) : in CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean
def AlgebraTowerEquiv.toAlgebraOverRight (e : AlgebraTowerEquiv A B) (i j : ι) in CompPoly/Data/RingTheory/AlgebraTower.lean
def binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : in CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean
def NZConst {n : ℕ} {R : Type} [Zero R] (p : Lawful n R) : Prop in CompPoly/Multivariate/Lawful.lean
def mkAddCommGroupInstance {k : ℕ} : AddCommGroup (ConcreteBTField k) in CompPoly/Fields/Binary/Tower/Concrete/Core.lean
def vars {n : ℕ} {R : Type} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n) in CompPoly/Multivariate/CMvPolynomial.lean
def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι) in CompPoly/Data/RingTheory/AlgebraTower.lean

✏️ **Added:** 1 declaration(s)

def NzConst {n : ℕ} {R : Type*} [Zero R] (p : Lawful n R) : Prop in CompPoly/Multivariate/Lawful.lean

✏️ **Affected:** 50 declaration(s) (line number changed)

def eval₂ {R S : Type*} {n : ℕ} [Semiring R] [CommSemiring S] : in CompPoly/Multivariate/CMvPolynomial.lean moved from L128 to L128
def restrictDegree {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L211 to L211
def aeval {n : ℕ} {R σ : Type*} [CommSemiring R] [CommSemiring σ] [Algebra R σ] in CompPoly/Multivariate/Operations.lean moved from L126 to L126
lemma bind₁_eq_aeval {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L173 to L173
def rename {n m : ℕ} {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L207 to L207
def leadingTerm {n : ℕ} {R : Type*} [Zero R] [BEq R] [LawfulBEq R] [MonomialOrder n] in CompPoly/Multivariate/Operations.lean moved from L75 to L75
def eval {R : Type*} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvPolynomial n R → R in CompPoly/Multivariate/CMvPolynomial.lean moved from L133 to L133
def eval₂Hom {S : Type*} [CommSemiring S] in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L89 to L89
lemma fromCMvPolynomial_X {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L271 to L271
def X {n : ℕ} {R : Type*} [Zero R] [One R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L53 to L53
abbrev CMvPolynomial (n : ℕ) (R : Type*) [Zero R] : Type _ in CompPoly/Multivariate/CMvPolynomial.lean moved from L42 to L42
def support {R : Type*} {n : ℕ} [Zero R] (p : CMvPolynomial n R) : Finset (Fin n →₀ ℕ) in CompPoly/Multivariate/CMvPolynomial.lean moved from L138 to L138
lemma fromCMvPolynomial_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L244 to L244
lemma list_foldl_add_comm {β K V : Type*} [AddCommMonoid β] in CompPoly/Multivariate/Rename.lean moved from L36 to L36
def monomial {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L157 to L157
lemma foldl_eq_sum {β : Type*} [AddCommMonoid β] in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L190 to L190
abbrev Unlawful (n : ℕ) (R : Type*) : Type _ in CompPoly/Multivariate/Unlawful.lean moved from L34 to L34
def sumToIter {n : ℕ} {R : Type*} [Zero R] [Add R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L216 to L216
def restrictBy {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L194 to L194
def leadingCoeff {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] in CompPoly/Multivariate/Operations.lean moved from L85 to L85
lemma foldl_add_comm {β : Type*} [AddCommMonoid β] {k : ℕ} in CompPoly/Multivariate/Operations.lean moved from L359 to L359
def evalMonomial {R : Type*} {n : ℕ} [CommSemiring R] : (Fin n → R) → CMvMonomial n → R in CompPoly/Multivariate/CMvMonomial.lean moved from L198 to L198
lemma add_getD? [AddZeroClass R] {m : CMvMonomial n} {p q : Unlawful n R} : in CompPoly/Multivariate/Unlawful.lean moved from L229 to L231
theorem ENNReal.mul_inv_rev_ENNReal {a b : ℕ} (ha : a ≠ 0) : in CompPoly/Data/Nat/Bitwise.lean moved from L52 to L52
lemma filter_get {R : Type*} [BEq R] [LawfulBEq R] {v : R} {m : CMvMonomial n} (a : Unlawful n R) : in CompPoly/Multivariate/Unlawful.lean moved from L225 to L227
def leadingMonomial {n : ℕ} {R : Type*} [Zero R] [MonomialOrder n] in CompPoly/Multivariate/Operations.lean moved from L58 to L58
lemma degreeOf_eq_count_degrees {n : ℕ} {R : Type*} [Zero R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L169 to L169
def coeff {R : Type*} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : CMvPolynomial n R) : R in CompPoly/Multivariate/CMvPolynomial.lean moved from L59 to L59
lemma list_foldl_add_comm {β K V : Type*} [AddCommMonoid β] in CompPoly/Multivariate/Operations.lean moved from L348 to L348
def restrictTotalDegree {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] in CompPoly/Multivariate/CMvPolynomial.lean moved from L203 to L203
lemma toList_pairs_monomial_coeff {β : Type*} [AddCommMonoid β] in CompPoly/Multivariate/MvPolyEquiv/Instances.lean moved from L179 to L179
lemma sumToIter_eq {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L378 to L378
def coeff {R : Type*} {n : ℕ} [Zero R] (m : CMvMonomial n) (p : Unlawful n R) : R in CompPoly/Multivariate/Unlawful.lean moved from L221 to L223
lemma eval₂_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] {f : (R →+* S)} in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L25 to L25
lemma zero_eq_empty [BEq R] [LawfulBEq R] : (0 : Unlawful n R) = ∅ in CompPoly/Multivariate/Unlawful.lean moved from L138 to L138
lemma coeff_sumToIter {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L389 to L389
def C {n : ℕ} {R : Type*} [BEq R] [LawfulBEq R] [Zero R] (c : R) : CMvPolynomial n R in CompPoly/Multivariate/CMvPolynomial.lean moved from L49 to L49
abbrev MonoR (n : ℕ) (R : Type*) in CompPoly/Multivariate/CMvMonomial.lean moved from L167 to L167
lemma eval₂Hom_apply {S : Type*} [CommSemiring S] in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L98 to L98
lemma totalDegree_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] : in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L56 to L56
lemma X_eq_monomial {k : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L222 to L222
def bind₁ {n m : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L166 to L166
lemma not_mem_zero : x ∉ (0 : Unlawful n R) in CompPoly/Multivariate/Unlawful.lean moved from L148 to L150
lemma zero_eq_empty : (0 : Lawful n R) = ∅ in CompPoly/Multivariate/Lawful.lean moved from L114 to L116
lemma degreeOf_equiv {S : Type*} {p : CMvPolynomial n R} [CommSemiring S] : in CompPoly/Multivariate/MvPolyEquiv/Eval.lean moved from L60 to L60
def Lawful (n : ℕ) (R : Type*) [Zero R] : Type _ in CompPoly/Multivariate/Lawful.lean moved from L28 to L30
lemma foldl_add_comm' {β : Type*} [AddCommMonoid β] {k : ℕ} in CompPoly/Multivariate/Rename.lean moved from L48 to L48
lemma isNoZeroCoef_zero : isNoZeroCoef (n in CompPoly/Multivariate/Unlawful.lean moved from L151 to L153
lemma sumToIter_add {n : ℕ} {R : Type*} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/Operations.lean moved from L398 to L398
def totalDegree {R : Type*} {n : ℕ} [Zero R] : CMvPolynomial n R → ℕ in CompPoly/Multivariate/CMvPolynomial.lean moved from L142 to L142

sorry Tracking

No sorrys were added, removed, or affected.

🎨 **Style Guide Adherence**

The following violations of the style guide were identified:

Acronyms treated as words (Violation Count: > 50)

Rule: "Acronyms: Treat as words (e.g., HtmlParser not HTMLParser)."
Representative Examples:
- Line 53 (CompPoly/Data/Nat/Bitwise.lean): ENNReal in ENNReal.mul_inv_rev_ENNReal should be Ennreal.
- Line 399 (CompPoly/Fields/Binary/AdditiveNTT/Impl.lean): BTF₃ should be Btf3.
- Line 39 (CompPoly/Multivariate/CMvPolynomial.lean): CMvPolynomial should be CmvPolynomial.
- Line 189 (CompPoly/Fields/Binary/BF128Ghash/Basic.lean): BF128Ghash should be Bf128Ghash.
- Line 28 (CompPoly/Multivariate/MvPolyEquiv/Core.lean): fromCMvPolynomial should be fromCmvPolynomial.

Spaces around operators and delimiters (Violation Count: > 50)

Rule: "Put spaces on both sides of :, :=, and infix operators."
Representative Examples:
- Line 84 (CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean): (l:=k), (r:=k+1), and (h_le:=by omega) are missing spaces around :=.
- Line 1346 (CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean): (n:=ℓ) is missing spaces around :=.
- Line 17 (tests/CompPolyTests/Univariate/Linear.lean): (a=b) is missing spaces around the infix operator =.
- Line 301 (CompPoly/Multilinear/Equiv.lean): h_binary: (∀ j: Fin n, ...) is missing a space after the colon and around the colon in the binder.

Function Syntax and fun ↦ Preference (Violation Count: > 50)

Rule: "Functions: Prefer fun x ↦ ... over λ x, ...."
Representative Examples:
- Line 104 (CompPoly/Multivariate/Unlawful.lean): Uses λ instead of fun ... ↦.
- Lines 751, 1346, 1403, and numerous others: Use => instead of the preferred ↦ (e.g., fun x hx => should be fun x hx ↦).

Missing Declaration Docstrings (Violation Count: ~15)

Rule: "Every definition and major theorem should have a docstring. ... Declaration Docstrings: Use /-- ... -/ above definitions."
Representative Examples:
- Line 179 (CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean): def binaryAlgebraTower lacks a docstring.
- Line 215 (CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean): def binaryTowerModule lacks a docstring.
- Line 535 (CompPoly/Fields/Binary/Tower/Concrete/Core.lean): def mkAddCommGroupInstance lacks a docstring.
- Line 587 (CompPoly/Fields/Binary/Tower/Concrete/Field.lean): def liftConcreteBTField lacks a docstring.

Additional Specific Violations:

Line 175 (CompPoly/Bivariate/ToPoly.lean): exact (toImpl_add (p.coeff x) (q.coeff x)).symm violates "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)". It should be Eq.symm (...).
Line 56 (CompPoly/Data/Nat/Bitwise.lean): (...).symm violates "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)". It should be Eq.symm (...).
Line 219 (CompPoly/Fields/Binary/Tower/Abstract/Split.lean): (h_k : k > 0) violates "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering." It should be 0 < k.
Line 310 (CompPoly/Fields/Binary/Tower/Abstract/Split.lean): (h_pos : k > 0) violates "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
Line 329 (CompPoly/Fields/Binary/Tower/Abstract/Split.lean): (h_pos : k > 0) violates "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
Line 301 (CompPoly/Multilinear/Equiv.lean): (∀ j: Fin n, ...) violates "Use a space after binders (e.g., ∀ x, not ∀x,)." (Specifically missing space before/after the binder's type colon).

📄 **Per-File Summaries**

CompPoly/Bivariate/ToPoly.lean: This change marks the ofPoly definition as noncomputable and refines several existing proofs to improve tactic robustness, specifically by substituting rw with erw and adjusting congruence applications. No new theorems are introduced, and no sorry or admit placeholders were added.
CompPoly/Data/Nat/Bitwise.lean: This update simplifies the proof of ENNReal.mul_inv_rev_ENNReal by utilizing existing ENNReal lemmas, which allows for the removal of an unnecessary non-zero hypothesis. Additionally, it updates a lemma reference in ENat.le_floor_NNReal_iff to maintain consistency with the current library. No sorry or admit placeholders were introduced.
CompPoly/Data/Polynomial/Frobenius.lean: This change modifies the proof of degree_dvd_of_irreducible_dvd_X_pow_card_pow_sub_X by replacing a standard rewrite with erw to resolve a definitional equality involving the cardinality of units. No new theorems or definitions are introduced, and the file contains no sorry or admit placeholders.
CompPoly/Data/RingTheory/AlgebraTower.lean: This change marks AlgebraTower.toAlgebra and related definitions in AlgebraTowerEquiv as reducible. This is intended to improve typeclass resolution by allowing the elaborator to more easily unfold these definitions when searching for Algebra instances within a tower.
CompPoly/Data/Vector/Basic.lean: This change modifies the proof of the theorem tail_cons by updating a lemma name in a simplification tactic to match current library naming conventions. No new theorems or definitions are introduced, and the file contains no sorry placeholders.
CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean: This change refines the proof of the additiveNTT_correctness theorem by updating the simplification and rewrite strategy for base_coeffsBySuffix. It replaces a standard simp/rw sequence with explicit erw calls to ensure the correctness proof remains robust, without introducing any new definitions or sorry placeholders.
CompPoly/Fields/Binary/AdditiveNTT/Impl.lean: This change marks the Fintype instance for the binary tower field BTF₃ as noncomputable. It does not introduce new theorems or definitions and contains no sorry placeholders.
CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean: This change modifies existing proofs by replacing rw with erw in two lemmas to resolve unification issues during rewriting. No new theorems, definitions, or sorry placeholders are introduced.
CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean: The changes refactor and stabilize several proofs related to polynomial degrees and linear maps between coefficient spaces, specifically improving the handling of natural number casts and submodule scalar multiplication. The modifications streamline existing proofs without introducing new definitions, theorems, or sorry placeholders.
CompPoly/Fields/Binary/BF128Ghash/Basic.lean: This change refines the proof of the root_satisfies_poly theorem by adjusting the simplification and rewriting tactics used to evaluate the field's minimal polynomial. Specifically, it replaces a portion of the simp call with erw to ensure that polynomial evaluation lemmas for powers and variables are applied correctly.
CompPoly/Fields/Binary/Common.lean: This change refactors the proof of toPoly_128_extend_256 by replacing a complex simp call with a more explicit and structured argument. It utilizes Nat.testBit_lt_two_pow directly to handle bitwise logic, improving the proof's clarity without introducing new theorems or sorry placeholders.
CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean: This update refines several proofs in the binary field tower formalization by adjusting simplification tactics and adding congr steps to handle casting more robustly. Additionally, it marks the binaryAlgebraTower and binaryTowerModule definitions as @[reducible] to improve instance resolution. No new theorems or sorry placeholders were introduced.
CompPoly/Fields/Binary/Tower/Abstract/Basis.lean: This PR refines and fixes proofs related to power bases and multilinear bases in binary tower fields by addressing issues with instance resolution and definitional equality. Key changes include using erw and specific compiler options (backward.isDefEq.respectTransparency) to bridge gaps where simp failed, and increasing resource limits for the complex multilinearBasis_apply theorem. No new theorems were added, and no sorry or admit placeholders were introduced.
CompPoly/Fields/Binary/Tower/Abstract/Split.lean: This PR refines the proofs for the linear decomposition and splitting of binary tower field elements, primarily by improving the handling of algebraic mappings and dependent type casts (eqRec). The changes replace implicit convert tactics with more explicit derivation steps in unique_linear_decomposition_succ and update the simplification path for embeddings in split_algebraMap_eq_zero_x. No new theorems or sorry placeholders are introduced.
CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean: This change marks ConcreteBTFieldAlgebra and binaryTowerModule as reducible and adjusts unification transparency settings to improve typeclass resolution and definitional equality checks within the concrete binary tower field hierarchy. No new theorems or sorry placeholders are introduced.
CompPoly/Fields/Binary/Tower/Concrete/Basis.lean: This change refactors and optimizes proofs related to basis constructions in the concrete binary tower field, notably by marking isScalarTower_succ_right as reducible and adjusting definitional equality transparency settings. The PR streamlines the proofs of PowerBasis.cast_basis_succ_of_eq_rec_apply and multilinearBasis_apply and introduces no new theorems or sorry placeholders.
CompPoly/Fields/Binary/Tower/Concrete/Core.lean: This PR refactors existing proofs in ConcreteBTField for better maintainability and modifies several instance-generating definitions (such as mkFieldInstance and mkRingInstance) by marking them as @[reducible]. The changes focus on streamlining tactic use—replacing complex simp calls with more direct erw and show statements—without introducing new theorems or sorry placeholders.
CompPoly/Fields/Binary/Tower/Concrete/Field.lean: This change refines the concrete binary tower field implementation by marking several core definitions and Fintype instances as noncomputable or @[reducible]. It also adjusts the backward.isDefEq.respectTransparency setting to ensure proper definitional equality behavior during field construction; no new theorems or sorry placeholders are introduced.
CompPoly/Fields/Binary/Tower/Equiv.lean: This Lean file updates the environment configuration by setting the backward.isDefEq.respectTransparency option to false. This change is intended to facilitate definitional equality checks and unification during the proofs of equivalences between abstract and concrete binary tower constructions.
CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean: This change modifies the proof environment for two theorems, linear_form_of_elements_in_adjoined_commring and its uniqueness counterpart, by disabling transparency checks during definitional equality. This adjustment is likely intended to resolve unification or elaboration issues occurring within the proofs of these theorems. No new theorems or definitions are introduced, and there are no sorry placeholders.
CompPoly/Multilinear/Basic.lean: This change refines the proofs of mobius_apply_zeta_apply_eq_id and zeta_apply_mobius_apply_eq_id by removing redundant simplification lemmas from their respective simp blocks. No new theorems or definitions are introduced, and no sorry placeholders were added.
CompPoly/Multilinear/Equiv.lean: This change streamlines the proofs of map_add' and map_smul' within the linearEquivMvPolynomialDeg1 definition by replacing redundant conv blocks and simp sequences with more direct rewrites. The modifications simplify the internal logic for mapping coefficients between multilinear and multivariate polynomials without introducing new definitions or theorems.
CompPoly/ToMathlib/MvPolynomial/Equiv.lean: This change applies the backward.isDefEq.respectTransparency configuration option to the support_finSuccEquivNth theorem to adjust how definitional equality is handled during proof elaboration. It does not introduce new theorems or sorry placeholders.
CompPoly/Univariate/Quotient/Core.lean: This refactors several proofs in the polynomial quotient implementation by replacing manual rewrites of quotient equality with the more idiomatic Quotient.sound. These changes simplify the proofs for operational "descending" lemmas (such as addition, multiplication, and power) without introducing new definitions or theorems.
CompPoly/Univariate/Raw/Proofs.lean: This change modifies the proof of the equiv_mul_one lemma by updating a lemma reference from Array.sum_eq_sum_toList to Array.sum_toList. No new definitions or sorry placeholders are introduced.
tests/CompPolyTests/Univariate/Linear.lean: This update marks custom BEq Nat instances as reducible and modifies the associated lawfulness proofs to use erw for more explicit unfolding. The changes refine existing internal proofs without introducing new theorems or sorry placeholders.
CompPoly/Multivariate/FinSuccEquiv.lean: This change generalizes the universe level of the ring type R by replacing Type with Type* in the variable declaration. It does not introduce new theorems or definitions.
CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean: This change generalizes the universe level of the commutative semiring type R by replacing Type with Type*. It maintains the existing lemmas without introducing new definitions, theorems, or sorry placeholders.
CompPoly/Multivariate/MvPolyEquiv/Eval.lean: This change generalizes the universe levels for the types R and S by replacing Type with Type* in several lemmas and definitions. These modifications increase the polymorphism of multivariate polynomial evaluation tools, such as eval₂_equiv and eval₂Hom, without altering the underlying logic or proofs.
CompPoly/Multivariate/Lawful.lean: This update generalizes Lawful multivariate polynomials to be universe-polymorphic and improves the reducibility of decidable equality instances to facilitate automation. It also standardizes naming conventions for constant checks and makes minor tactical adjustments to existing proofs.
CompPoly/Multivariate/MvPolyEquiv/Instances.lean: This change generalizes universe levels for ring and type variables from Type to Type* and updates the proof of map_mul to be more robust against beta-reduction changes in newer Lean versions. The modifications ensure the internal definition of F₃ is correctly handled during rewriting, without introducing any sorry or admit placeholders.
CompPoly/Multivariate/CMvPolynomial.lean: The changes generalize the universe levels of ring types R and S by replacing Type with Type* across numerous definitions and lemmas. Additionally, the definitions degreeOf, degrees, and vars are marked as noncomputable. No new theorems were introduced and no sorry placeholders were added.
CompPoly/Multivariate/Operations.lean: This change generalizes the universe levels for types (such as the coefficient ring $R$) across various multivariate polynomial definitions and lemmas by replacing Type with Type*. These updates increase the library's flexibility by allowing operations like leadingMonomial, aeval, and bind₁ to be used in higher type universes.
CompPoly/Multivariate/CMvMonomial.lean: This change generalizes the universe level of the type parameter R from Type to Type* across the MonoR and evalMonomial definitions. This ensures that these multivariate monomial structures and their evaluation functions can be used with types residing in any universe level.
CompPoly/Multivariate/MvPolyEquiv/Core.lean: This change generalizes the universe level of the coefficient ring and refines the proofs for the equivalence between CMvPolynomial and MvPolynomial. It modifies existing proofs to use more explicit lemma applications for ExtTreeMap operations and contains no sorry or admit placeholders.
CompPoly/Multivariate/VarsDegrees.lean: This change generalizes the universe level of the type parameter R from Type to Type*. This allows the definitions and lemmas in the file to be used with types in any universe level rather than being restricted to Type 0.
CompPoly/Multivariate/Restrict.lean: This update introduces universe polymorphism for type parameters and refactors a proof to use the renamed Array.sum_toList lemma. No new theorems or sorry placeholders are added.
lakefile.lean: This update bumps the versions of the mathlib and ExtTreeMapLemmas dependencies to align the project with the v4.29.0-rc6 release cycle.
CompPoly/Multivariate/Rename.lean: This update generalizes universe levels from Type to Type* across several declarations and modifies the proof of toFinsupp_zero by adding an explicit terminal step. No new theorems, definitions, or sorry placeholders are introduced.
CompPoly/Multivariate/Unlawful.lean: This PR refactors the Unlawful multivariate polynomial type from a definition to an abbreviation and updates the coefficient type R to be universe polymorphic. It also generalizes the add_getD? lemma to require only an AddZeroClass instance and adjusts internal reducible attributes to improve elaborator performance. No sorry or admit placeholders were introduced.

Last updated: 2026-03-31 19:46 UTC.

github-actions · 2026-03-28T19:45:56Z

Build Timing Report

Commit: 0655a3a
Message: Merge ba504dc into fe33688
Ref: dhsorens/bump_to_4.29.0-rc6
Comparison baseline: 2aeb7af from the previous successful PR update.
Measured on ubuntu-latest with /usr/bin/time -p.
Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; test path lake test.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	244.80	241.75	-3.05	ok
Warm rebuild	1.72	1.71	-0.01	ok
Test path	16.55	15.94	-0.61	ok

Incremental Rebuild Signal

Warm rebuild saved 240.04s vs clean (141.37x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
58.00	57.00	+1.00	`CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowModCertificate.lean`
55.00	56.00	-1.00	`CompPoly/Fields/Binary/Tower/Abstract/Basis.lean`
45.00	48.00	-3.00	`CompPoly/Bivariate/ToPoly.lean`
28.00	24.00	+4.00	`CompPoly/Fields/Binary/BF128Ghash/Impl.lean`
26.00	25.00	+1.00	`CompPoly/Univariate/Raw/Proofs.lean`
23.00	23.00	+0.00	`CompPoly/Univariate/Lagrange.lean`
22.00	21.00	+1.00	`CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean`
20.00	18.00	+2.00	`CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean`
17.00	15.00	+2.00	`CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean`
16.00	16.00	+0.00	`CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean`
14.00	15.00	-1.00	`CompPoly/Fields/Binary/AdditiveNTT/Domain.lean`
13.00	16.00	-3.00	`CompPoly/Fields/Binary/Tower/Abstract/Core.lean`
13.00	16.00	-3.00	`CompPoly/Univariate/Quotient/Core.lean`
11.00	8.20	+2.80	`CompPoly/Fields/Basic.lean`
11.00	13.00	-2.00	`CompPoly/Univariate/Basic.lean`
10.00	12.00	-2.00	`CompPoly/Multivariate/Unlawful.lean`
10.00	9.60	+0.40	`CompPoly/Fields/Binary/BF128Ghash/XPowTwoPowGcdCertificate.lean`
10.00	7.80	+2.20	`CompPoly/Multivariate/MvPolyEquiv/Instances.lean`
9.50	9.60	-0.10	`CompPoly/Data/Nat/Bitwise.lean`
9.50	9.00	+0.50	`CompPoly/Fields/KoalaBear.lean`

github-actions · 2026-03-28T19:56:56Z

🤖 Initial AI review without external context

🤖 AI Review

Overall Summary:

Executive Summary

1. TL;DR
The mathematical foundations and recent universe generalizations in this PR are highly solid, featuring excellent cleanups (e.g., ENNReal.mul_inv_rev_ENNReal) and proper use of Type*. However, several structural issues involving legacy transparency options (backward.isDefEq.respectTransparency) and unidiomatic theorem definitions for Prop-valued types need to be addressed before merging.

2. Checklist Coverage
No explicit checklist was provided for this review.

(Note: No Critical Misformalizations were found in this PR. The mathematical logic and algebraic constructions are sound.)

3. Key Lean 4 / Mathlib Issues

Overuse of Legacy Transparency Options (2 primary files, 5 secondary files):
The PR heavily utilizes set_option backward.isDefEq.respectTransparency false. This is flagged as a blocker in Fields/Binary/Tower/Equiv.lean (used globally) and Fields/Binary/Tower/Support/Preliminaries.lean (used to override theorem-level transparency), and noted as a minor issue in Abstract/Basis.lean, Concrete/Algebra.lean, Concrete/Basis.lean, Concrete/Field.lean, and ToMathlib/MvPolynomial/Equiv.lean.
- Action: This is a legacy compatibility flag that can lead to unpredictable elaboration and masks structural issues. Global use is strongly discouraged in Mathlib. Please remove it in favor of explicit API tactics (unfold, dsimp, change, erw), strictly scope it using set_option ... in, or—if absolutely necessary for performance/timeouts—add explanatory comments detailing exactly why it is required.
Improper Syntax for Prop-Valued Declarations (1 file):
In Fields/Binary/Tower/Concrete/Basis.lean, isScalarTower_succ_right is defined using @[reducible] def without an explicit return type. Because it returns a proof of IsScalarTower (a Prop-valued typeclass), it must be declared as a lemma or theorem with an explicit return type. The @[reducible] attribute is unnecessary here due to proof irrelevance.

4. Minor Observations & Nitpicks

abbrev vs @[reducible] def: Across several files (AlgebraTower.lean, Concrete/Algebra.lean, Concrete/Field.lean), @[reducible] def is used. In Lean 4, abbrev is the standard, idiomatic shorthand for this pattern.
Duplicate Instances: Fields/Binary/Tower/Concrete/Field.lean defines two identical noncomputable instance declarations for Fintype (ConcreteBTField k). One should be removed to prevent overlapping instances during typeclass resolution.
Naming Conventions: In Multivariate/Rename.lean, list_foldl_add_comm should be renamed to List.foldl_add_comm to align with Mathlib namespace conventions. In Multivariate/Lawful.lean, consider renaming NzConst to isNzConst (lowerCamelCase is preferred for Prop-valued predicates).
Proof & Command Style:
- In AlgebraTower.lean, by exact ... is redundant and can be replaced directly with the term.
- In ToMathlib/MvPolynomial/Equiv.lean, ensure docstrings (/-- ... -/) are placed above the set_option ... in command modifiers for stylistic consistency.

5. Overall Verdict
Changes Requested

📄 **Review for `CompPoly/Bivariate/ToPoly.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Data/Nat/Bitwise.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The diff is a welcome and highly effective cleanup. It removes an unnecessary hypothesis (hb : b ≠ 0) from ENNReal.mul_inv_rev_ENNReal and drastically simplifies its proof by taking advantage of the robust ENNReal.mul_inv lemma. The simp lemma update in ENat.le_floor_NNReal_iff is also fully correct.)

📄 **Review for `CompPoly/Data/Polynomial/Frobenius.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Data/RingTheory/AlgebraTower.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

In Lean 4, it is generally more idiomatic to use abbrev instead of @[reducible] def. For example, you can write abbrev AlgebraTowerEquiv.toAlgebraOverLeft ... which automatically makes the definition reducible.

The bodies of toAlgebraOverLeft and toAlgebraOverRight use by exact .... This is redundant and can just be written directly as the term:

@[reducible] def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι)
    (h : i ≤ j) : Algebra (A i) (B j) :=
  (e.algebraMapRightUp i j h).toAlgebra

📄 **Review for `CompPoly/Data/Vector/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/Correctness.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/Impl.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The addition of noncomputable is correct and necessary here, as the inferred Fintype (ConcreteBTField 3) instance relies on ConcreteBinaryTower.instFintype, which is itself noncomputable since it is derived from getBTFResult.)

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/Intermediate.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/BF128Ghash/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Common.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Tower/Abstract/Basis.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
The increase of maxHeartbeats to 800,000 and the use of set_option backward.isDefEq.respectTransparency false indicate that multilinearBasis_apply and cast_basis_succ_of_eq_rec_apply are struggling significantly with definitional equality checks, likely due to dependent typing and cast/Eq.rec over deeply nested algebraic structures. While these changes are reasonable, pragmatic fixes to get the proofs to compile without timing out, you might consider refactoring the underlying definitions in the future to avoid Eq.rec (or minimize its scope) to improve performance and maintainability.

📄 **Review for `CompPoly/Fields/Binary/Tower/Abstract/Split.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Algebra.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Transitional Option: The use of set_option backward.isDefEq.respectTransparency false is generally intended as a transitional compatibility flag for code broken by the isDefEq transparency fixes introduced in Lean 4.8+. It is recommended to eventually fix the underlying proofs or defeq issues and remove this option, as it may be deprecated and removed in future Lean versions.
abbrev vs @[reducible] def: Adding @[reducible] to def ConcreteBTFieldAlgebra and def binaryTowerModule is correct and necessary for unification to see through the definitions. However, abbrev is the idiomatic shorthand for @[reducible] def in Lean 4 and could be used here for stylistic consistency.

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Basis.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

Idiom violation in isScalarTower_succ_right: You are using @[reducible] def without an explicit return type for a declaration that returns a proof of a Prop (specifically, IsScalarTower, which is a Prop-valued typeclass).
- Top-level declarations should always have explicit return types.
- Since IsScalarTower is a Prop, this should be a lemma or theorem. The @[reducible] attribute is unnecessary for Props due to proof irrelevance.
It should be rewritten as:
```
lemma isScalarTower_succ_right (l r : ℕ) (h_le : l ≤ r) : 
    IsScalarTower (ConcreteBTField l) (ConcreteBTField r) (ConcreteBTField (r + 1)) :=
  instAlgebraTowerConcreteBTF.toIsScalarTower (i:=l) (j:=r) (k:=r+1)
    (h1:=by omega) (h2:=by omega)
```

Nitpicks:

Global compiler option: The addition of set_option backward.isDefEq.respectTransparency false at the top of the file alters how definitional equality is checked for the entire file. While sometimes necessary for performance or working around timeouts with heavy algebraic hierarchies, it is generally discouraged as it can lead to bad typechecking behavior. Ensure this is strictly necessary and consider adding a short comment explaining why it is needed here.
Proof style: The use of simp (config := { failIfUnchanged := false }) only [...] is a bit fragile and unidiomatic for proof scripts. If the simp is not expected to change the goal in all cases, consider structuring the proof so that the conditional simplification is avoided or handled by a tactic like try simp only [...].

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
The changes are excellent. Adding @[reducible] to instance-building helpers (mkAddCommGroupInstance, mkRingInstance, mkDivisionRingInstance, mkFieldInstance) is a solid Lean 4 best practice. It ensures typeclass resolution and definitional equality checks can transparently unfold these helpers, preventing frustrating typeclass diamonds (e.g., Lean failing to unify the addition from AddCommGroup with the addition from Ring). The proof simplifications are also clean and idiomatic.

📄 **Review for `CompPoly/Fields/Binary/Tower/Concrete/Field.lean`**

Verdict: Needs Minor Revisions

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Duplicate Instances: The PR modifies two identical Fintype instances for ConcreteBTField k to make them noncomputable. Having duplicate instances for the same typeclass is redundant and can cause overlapping instances during typeclass resolution. You should remove one of them.
```
noncomputable instance (k : ℕ) : Fintype (ConcreteBTField k) := (getBTFResult k).instFintype

noncomputable instance instFintype {k : ℕ} : Fintype (ConcreteBTField k) :=
  (getBTFResult k).instFintype
```
File-level set_option: You added set_option backward.isDefEq.respectTransparency false at the top of the file. While occasionally necessary for defEq performance, it is generally preferred to scope such options locally using set_option ... in for the specific problematic declarations, or at least leave a comment explaining which definitions/proofs required this workaround.
@[reducible] def vs abbrev: You added @[reducible] to def liftConcreteBTField. In Lean 4, abbrev liftConcreteBTField ... is the standard idiomatic shorthand for @[reducible] def.

📄 **Review for `CompPoly/Fields/Binary/Tower/Equiv.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

Global use of backward compatibility options: The PR introduces set_option backward.isDefEq.respectTransparency false globally at the top of the file. This option is generally considered a temporary workaround for performance or timeout issues caused by how the Lean 4 unifier handles transparency. Its global use is strongly discouraged in Mathlib because it can lead to unpredictable elaboration behavior and masks underlying structural issues (e.g., missing abbrev/reducible attributes or overly complex defeq checks).
- If this is strictly necessary to make the file compile or to prevent timeouts, please add an explanatory comment or a TODO describing what breaks without it.
- Ideally, scope the option only to the specific declarations or proofs that require it by using set_option backward.isDefEq.respectTransparency false in rather than setting it for the entire file.

Nitpicks:
None

📄 **Review for `CompPoly/Fields/Binary/Tower/Support/Preliminaries.lean`**

Verdict: Changes Requested

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

The PR adds set_option backward.isDefEq.respectTransparency false in to linear_form_of_elements_in_adjoined_commring and unique_linear_form_of_elements_in_adjoined_commring. This is a legacy compatibility option from the Lean 3 to Lean 4 porting effort and is considered highly unidiomatic in modern Lean 4 / Mathlib. It indicates that the proof relies on a definitional equality that is intentionally hidden behind a transparency boundary (e.g., irreducible or opaque definitions). Instead of overriding the transparency settings globally for the entire theorem and its proof, you should explicitly rewrite using the appropriate API lemmas or use tactics like unfold, dsimp, change, or erw to unfold the specific definitions where needed.

Nitpicks:
None

📄 **Review for `CompPoly/Multilinear/Basic.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multilinear/Equiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/CMvMonomial.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/CMvPolynomial.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/CMvPolynomialEvalLemmas.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Comments:
This is a straightforward and correct fix. Changing R : Type to R : Type* properly makes the lemmas universe-polymorphic, matching the definition of CMvPolynomial and avoiding unnecessary universe restrictions that would prevent these simp lemmas from applying to polynomials over types in higher universes.

📄 **Review for `CompPoly/Multivariate/FinSuccEquiv.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Lawful.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Unsafe Reducibility: The addition of set_option allowUnsafeReducibility true in alongside attribute [local reducible] is a bit of a code smell. While safe here because it is scoped locally, relying on this to force definitional equality of instances (presumably for grind) usually indicates that the instance itself should have been an abbrev or that the proofs might be brittle.
Naming Conventions: Lean 4 naming conventions prefer lowerCamelCase for Prop-valued predicates (unless they are typeclasses). Consider renaming NzConst to isNzConst or nzConst. (The change from NZConst to NzConst is still an improvement, as it avoids consecutive capital letters which the linter dislikes!).

📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Eval.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/MvPolyEquiv/Instances.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Operations.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Rename.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

list_foldl_add_comm: It is generally preferred to leverage namespaces for theorems about core types. Consider renaming this lemma to List.foldl_add_comm to align with typical Mathlib naming conventions.

📄 **Review for `CompPoly/Multivariate/Restrict.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `CompPoly/Multivariate/Unlawful.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The changes in this diff are excellent. Generalizing Type to Type* for universe polymorphism, replacing def with abbrev to avoid reducible/transparency issues with type synonyms, and weakening the typeclass bound in add_getD? from [CommSemiring R] to [AddZeroClass R] all align perfectly with Mathlib best practices.)

📄 **Review for `CompPoly/Multivariate/VarsDegrees.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

Reviewer Notes:
The change appropriately updates the variable R to be universe-polymorphic (Type* instead of Type), which aligns with standard Mathlib conventions and matches the definition of CMvPolynomial. This is a clean and necessary improvement.

📄 **Review for `CompPoly/ToMathlib/MvPolynomial/Equiv.lean`**

Verdict: Needs Minor Revisions

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

The use of set_option backward.isDefEq.respectTransparency false is a known workaround for typechecker performance degradation or defeq failures. It is highly recommended to include a brief comment explaining why this option is required here (e.g., "Workaround for heavy defeq checks unfolding MvPolynomial or Finsupp internals"), so future maintainers know under what conditions it can be safely removed.
Idiomatically in Mathlib, docstrings (/-- ... -/) are typically placed above set_option ... in command modifiers. While Lean 4's parser handles both orderings correctly, consider moving the set_option line below the docstring for style consistency:
```
/-- The support of `finSuccEquivNth R p f` equals the support of `f` projected onto the `p`-th
variable. -/
set_option backward.isDefEq.respectTransparency false in
theorem support_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) :
```

📄 **Review for `CompPoly/Univariate/Quotient/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

(The replacement of rw [Quotient.eq]; simp [...] with apply Quotient.sound is an excellent and idiomatic simplification for proving the equality of quotients.)

📄 **Review for `CompPoly/Univariate/Raw/Proofs.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `lakefile.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `tests/CompPolyTests/Univariate/Linear.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

Verbosity in proofs: The pattern erw [show natBeqEq.beq a a = decide (a = a) from rfl] is a bit verbose. Since you made natBeqEq and natBeqSucc @[reducible], they unfold transparently. You could often just use change decide (a = a) = true or dsimp only [natBeqEq] to achieve the same result more idiomatically. However, since this is a test file and the proofs are short, the current approach is perfectly acceptable.

* refactor(multivariate): generalize coefficient universes * refactor(multivariate): restore ExtTreeMap lemmas dependency * style(multivariate): clean review nits * fix(multivariate): adapt universe branch to Lean 4.29

feat: bump lean version

1590b5b

fix: linter

2aeb7af

Generalize CMvPolynomial coefficient universes (#178)

ba504dc

* refactor(multivariate): generalize coefficient universes * refactor(multivariate): restore ExtTreeMap lemmas dependency * style(multivariate): clean review nits * fix(multivariate): adapt universe branch to Lean 4.29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: bump lean version#176

feat: bump lean version#176
dhsorens wants to merge 3 commits intomasterfrom
dhsorens/bump_to_4.29.0-rc6

dhsorens commented Mar 28, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 28, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 28, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 28, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

dhsorens commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

CHANGELOG

Uh oh!

github-actions bot commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Gemini PR Summary

Toolchain & Infrastructure

Typeclass Resolution & Reducibility

Proof Maintenance & Tactic Adjustments

Mathematical Refactoring

Uh oh!

github-actions bot commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Build Timing Report

Incremental Rebuild Signal

Slowest Current Clean-Build Files

Uh oh!

github-actions bot commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Initial AI review without external context

🤖 AI Review

Executive Summary

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

dhsorens commented Mar 28, 2026 •

edited

Loading

github-actions bot commented Mar 28, 2026 •

edited

Loading

github-actions bot commented Mar 28, 2026 •

edited

Loading

github-actions bot commented Mar 28, 2026 •

edited

Loading