Repository navigation
Conversation
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Medium impact] No blocking defect was established in the follow-up changes; this is not whole-contribution clearance. SummaryImports the Eichler–Shimura development and supporting results about elliptic-curve Galois representations.
Reviews (4) · Last reviewed commit: "typo" · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Retain applicable upstream attribution; preserve every mathematical source file.
Vilin97
reviewed
Oct 20, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
There was a problem hiding this comment.
Scoped source review at 7860bd069f06153b6c96d46f6f6fcbbdb44e7b4f of the four advertised results and their supporting constructions.
The Eichler–Shimura result proves injective holomorphic and antiholomorphic maps with complementary ranges in the actual parabolic cocycle quotient. Its Hecke intertwining clauses quantify over a supplied cohomology operator and require that operator to descend from coeffHeckeFun (the all-primes theorem, lines 204–237). The card now states that condition. The good-prime Tate-module results use the genuine inverse-limit torsion representation; their cardinality hypothesis is already disclosed in the card.
The submitted head named a missing LeanPool.FLTEichlerShimura entry. Commit 7860bd069f06153b6c96d46f6f6fcbbdb44e7b4f adds that entry with the four headline imports and applicable upstream attribution, regenerates the project index, and corrects the card. The actual index/card checks and complete import DAG pass. All 1,192 mathematical files remain byte-identical; no hypothesis, proof, option, or gate changes.
Maintenance advisory: five RationalFunctionField modules contain roughly 2,600 matching helper lines after only solution-namespace normalization. A shared helper module would avoid repeating future repairs. I am retaining that finding as advisory while the independent project review weighs the import.
This audit covers the complete file inventory, the headline statements, selected supporting definitions/proofs, provenance samples, and the complete import graph. It does not claim a line-by-line review of all 1,192 proof modules or a completed build. Whole-import acceptance remains pending the independent configured review and complete current-head protected validation; current-main validation is also pending.
Collaborator
|
/review Please review exact head 7860bd0 under the current five project rubrics, including prior-art comparison and explicit coverage limits. The scoped source audit is review 5592057176. The card/entry/index repair preserves all 1,192 mathematical files. Current-head CI and current-main qualification remain independent pending requirements. |
Refresh the generated project card and retain all author proof changes and attribution.
Vilin97
reviewed
Oct 20, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
There was a problem hiding this comment.
Follow-up source review at 8b9383bc75adcdca8e3bdb81567651dbfd7bbfcb.
The author's da8d283 adds six complete proofs. The transfer formula preserves cocycles and coboundaries; the finite-orbit argument establishes parabolicity. The quotient construction then supplies actual cohomology operators, and exists_eichlerShimura_heckeEquivariant uses them to prove both the away-from-level T and at-level U compatibility. This constructively discharges the earlier descent hypothesis, so the new unconditional card headline is supported.
We reviewed all 1,244 added mathematical lines and the required existing intertwining supplier. The one-file entry update imports the new wrapper and refreshes the generated card. Its public import preserves the old conditional API, all 1,198 mathematical files are unchanged from da8d283, and the 1,200-module import graph and actual index/card checks pass.
The six-proof delta is favorable. The earlier scoped audit and advisory maintenance decision remain recorded; whole-import acceptance still awaits the independent configured review and complete protected validation at this exact head. Earlier-head CI or review results do not supply that acceptance.
Collaborator
|
/review Please review exact current head 8b9383b under the current five project rubrics, with explicit coverage limits. This new-head request follows the author’s six-proof Hecke-descent addition and final entry refresh. Earlier request 6302060076 was ingested for da8d283 and supplies no acceptance for this revision. The follow-up scoped source audit is review 5592216989. Current-head CI and current-main qualification remain independent requirements. |
Collaborator
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
The four card headlines match the Lean statements and constructions; current-head CI is still running, with no reported failure. |
| Novelty | 🤔 discuss |
The good-reduction Tate-module headline substantially overlaps Tau Ceti, but its global formulation has not been established as an exact duplicate. |
| Significance | ✅ pass |
The Eichler–Shimura and Tate-module results meet the significance bar; head CI remains pending, and local validation was blocked by a Mathlib dependency-fetch HTTP 403. |
| Sources | ✅ pass |
Checked FLT source statements and prior-work attributions agree with the diff; textbook references and exhaustive historical provenance remain unverifiable. |
| Code quality (advisory) | 🤔 discuss |
Duplicated proof libraries and widespread linter suppression merit human review; the full diff was scanned with sampled detailed inspection, and current-head CI remains pending. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Both Tate-module headlines assume the p-power torsion cardinalities, explicitly disclosed in the card and supported by WeierstrassCurve.card_torsionBy_eq_sq_of_isAlgClosed. The characteristic-polynomial theorem also takes a valuation above the prime and an arithmetic Frobenius lift. Complementarity takes maps satisfying the canonical-map and conjugation identities; the PR constructs witnesses for these inputs. The new headline constructs the descended Hecke operators rather than requiring descent as a hypothesis. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | research |
| Branch | arithmetic geometry and modular forms |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: For nonzero levels and weights at least two, the code constructs the Hecke-equivariant decomposition and establishes canonical complementarity, while the Tate-module results apply to integral models at primes away from their discriminant and p (complete diff scanned; detailed audit focused on headlines, definitions, and witness/descent constructions; no local build because dependencies are absent).
Develops parabolic cohomology and Hecke actions through the Eichler–Shimura decomposition, alongside Frobenius characteristic-polynomial and good-prime unramifiedness theorems for elliptic-curve Tate modules.
Novelty findings (1)
- partial-overlap —
LeanPool/FLTEichlerShimura/Theorems/Thm_WeierstrassCurve_tateModuleRep_isUnramifiedAt_of_isGoodPrimeFor.lean:211
This headline concludes((W.map (Int.castRingHom ℚ)).tateModuleRep p hcard).IsUnramifiedAt qunder good reduction andq ≠ p. Tau Ceti already proves trivial inertia action on Tate modules at good reduction over nonarchimedean local fields. The global formulation over ℚ using valuation subrings is distinct; whether it warrants a parallel headline requires a maintainer decision, since a formal subsumption has not been verified.
Evidence: WeierstrassCurve.tateModuleGaloisRepresentation_eq_one_of_mem_inertiaSubgroup proves that every inertia element acts identically on the Tate module when the curve has an integral model with unit discriminant over a nonarchimedean local field and the coefficient prime is nonzero in its residue field: declaration and hypotheses.
Code quality findings (2)
- duplicate-definition —
LeanPool/FLTEichlerShimura/Theorems/Thm_HeckeEis_coeffHeckeFun_mem_coeffCocycles.lean:68
This module and Thm_HeckeEis_coeffHeckeFun_mem_coeffCoboundaries.lean contain an identical 132-line Sh2 library, although each exports a different endpoint. The pattern extends throughout the extraction: lSpaceShiftEquiv has 16 identical copies, finrank_adeleBddSup_quotient has 15, and roots_prime_at_slot_nodup has two repeated variants with 19 and 6 copies. Maintaining separate proofs multiplies Mathlib migration and repair work. Extract shared helper modules and import them from the endpoints.
Evidence: The identical blocks occupy lines 68–199 here and 69–200 in Thm_HeckeEis_coeffHeckeFun_mem_coeffCoboundaries.lean, including:
include ha in
theorem mem_coeffCocycles {z : Gamma0 N → V} (hz : z ∈ coeffCocycles ρ) :
coeffHeckeFun N ℓ ρ a z ∈ coeffCocycles ρ := by
let := (heckeUpper N ℓ).fintypeQuotientOfFiniteIndex
The repeated rational-function helper begins at Thm_AlgebraicCurve_RationalFunctionField_ord_X_nonneg_of_ne_placeInfty.lean:375:
def lSpaceShiftEquiv (D : Divisor K F) {g : F} (hg : g ≠ 0)
{Dg : Divisor K F} (hDg : ∀ v, Dg v = v.ord g) :
LSpace D ≃ₗ[K] LSpace (D + Dg) where
- linter-suppression —
LeanPool/FLTEichlerShimura/Definitions/Defs_IsogenyEndDatum_sharedLibrary.lean:57
The PR introduces 82 active unused-variable suppressions across 52 files, frequently covering whole proof sections. These disable feedback that would otherwise expose unused binders and proof residue during maintenance. Restore the checks and address individual unused variables instead of suppressing their detection across these libraries.
Evidence:set_option linter.unusedVariables falseappears here at line 57, in Theorems/Thm_AlgebraicCurve_tateAgreement.lean at lines 1717, 1864, 2002, 2271, 2340, 2535, 3214, and 3506, and in Theorems/Thm_ModularCurve_LevelN_exists_place_ord_neg_forall_smul_eq.lean at line 69, all under LeanPool/FLTEichlerShimura/. The same active suppression occurs across the algebraic-curve, modular-curve, period, and isogeny proof sections.
Tokens: 7,588,708 in / 52,008 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $31.1350 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
CI was not green for this commit at review time; this review does not replace CI.
Vilin97
requested changes
Oct 20, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
There was a problem hiding this comment.
Reviewed exact head 8b9383bc75adcdca8e3bdb81567651dbfd7bbfcb.
Changes are required under the existing quality rules. I independently checked the complete Git blobs of the 52 affected files and confirmed 82 active set_option linter.unusedVariables false commands: 80 section-scoped commands and two command-local wrappers. These are active code, not comments or strings. Examples include Definitions/Defs_IsogenyEndDatum_sharedLibrary.lean:57 and Theorems/Thm_WeierstrassCurve_exists_velu2FunctionFieldHom_restrictAlong_placeOfPoint_veluPointMap2.lean:703, under LeanPool/FLTEichlerShimura/.
The same 52 files contain 76 additional active option commands, including maxHeartbeats, synthInstance.maxHeartbeats and backward.isDefEq.respectTransparency.types. Current .github/CODE_QUALITY.md:39–40 and python/lean_pool/quality.py forbid active set_option commands; CONTRIBUTING.md also prohibits adding linter waivers. This is an existing deterministic gate, independent of the advisory 2/5 quality assessment.
Please remove forbidden option commands throughout the import and fix the actual unused-binder/elaboration diagnostics under the unchanged checks. Preserve the mathematical statements, assumptions, proof arguments, public named-argument API and source credits. The affected scopes span 82,507 lines, so deleting the 82 suppression lines alone does not establish a warning-free repair. Validate the repaired exact head with the normal build, lint, style and quality checks.
The favorable scoped review of the six new Hecke descent proofs remains valid at this head. Whole-import acceptance remains pending; no waiver or new benchmark is being requested.
Collaborator
|
CI follow-up for The complete build-step log contains 137 distinct warning sites across 82 files:
Lint, text-style lint and repository quality checks were subsequently skipped, so those gates remain unvalidated. Please include these warning-cleanliness repairs alongside the existing request to remove 82 unused-variable suppressions across 52 files. Preserve mathematical statements, assumptions and the normal limits/checks while repairing the code. The existing changes request remains in force. |
Contributor
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 147,274,254 maxHeartbeats units across 1119 valid files (486,566 added LOC). Sum of Count-heartbeats wall-clock total: 20511.22 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_Affine_isAddCyclic_ker_pointMapOfPushforward_of_baseChange_algHom |
246.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_Affine_exists_algHom_baseChange_of_isAddCyclic_ker_pointMapOfPushforward |
230.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_Affine_exists_intermediateField_countable_map_eq_of_isAddCyclic_ker_pointMapOfPushforward |
223.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_IsIntegral_mem_span_of_adjoin_simple_constants_transcendental |
198.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WeierstrassCurve_exists_intermediateField_countable_map_eq_and_finrankAlong_eq |
184.00 s |
LeanPool.FLTEichlerShimura.Definitions.Def_ModularCurve_CharLFrobeniusGeomLevel |
166.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WLight_exists_levelFraction_of_stable_family |
162.00 s |
LeanPool.FLTEichlerShimura.Definitions.Defs_WeierstrassCurve_veluSharedLibrary |
157.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_WLight_levelN_structure_package |
147.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateTraceCompat_of_isSeparable |
124.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_ModularCurve_jqNModC_prime_not_mem_fullC |
122.00 s |
LeanPool.FLTEichlerShimura.Theorems.Thm_AlgebraicCurve_tateAgreement |
119.00 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 1200 files; the per-file table shows only the 313 hottest by heartbeats. The full table and raw
lean --profileoutput for every file are in the run's step summary andproof-profileartifact.
Advisory only — never blocks merge.
Author
|
I have pushed fixes for the 82 unused-variable warnings; and I removed one of the two elliptic-curve "main results" (unramifiedness of the Tate module), since it overlaps somewhat with existing results in Tau Ceti, + is subsumed by the other, much more important elliptic-curve result here (computing char poly of Frobenius). |
Vilin97
requested changes
Oct 21, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
There was a problem hiding this comment.
Reviewed exact head 5b7008d795c9c6733aa878083f54038cc4d6de23 and the complete 56-file follow-up.
The 82 linter.unusedVariables false commands and one other option command were removed; no option command was added. The YAML also genuinely withdraws unramifiedness as a separate headline. The remaining Eichler–Shimura, complementarity and Frobenius results remain substantial within the scoped mathematical review.
Changes are still required under the existing deterministic gates:
- A comment/string-aware scan of all 1,200 current Lean source files finds 1,065 active
set_optioncommands in 949 files. This includes 946backward.isDefEq.respectTransparency.types, 77synthInstance.maxHeartbeatsand 30maxHeartbeatscommands. For example,Definitions/Defs_IsogenyEndDatum_sharedLibrary.lean:51,55retains heartbeat and transparency overrides. The original 52-file review scope alone still contains 76 option commands. Remove forbidden overrides throughout the import and repair the underlying elaboration/resource issues under the unchanged settings. - The same checker also rejects
modifyScopeinDefinitions/Def_P2M_Util.lean:90and the remaining@[nolint unusedArguments]inTheorems/Thm_ModularCurve_LevelN_exists_linearMap_regularDifferentials_mdifferentiable.lean:363. Replace the namespace-routing mechanism with permitted source constructs and fix the unused arguments without a waiver. LeanPool/FLTEichlerShimura.lean:20still advertises the withdrawn unramifiedness headline in its generated project card. Regenerate that card from the updated YAML, preserving the public imports and source attribution.
Paths above are under LeanPool/FLTEichlerShimura/ unless fully qualified. These source requirements are independent of the advisory quality score. The cleanup spans 949 modules, so deleting option lines alone is not a validated repair: preserve the mathematics and pass the normal warning-free build, lint, style and quality checks on the repaired exact head. Current-head configured review and protected queue validation remain separate requirements.
Collaborator
|
CI update for The current head has 133 distinct warning locations in 80 files:
Please repair the warnings in the Lean code under the existing contribution rules. Lint, text-style and repository-quality steps were skipped after this failure, so they still need successful execution. The current Source changes-requested review and its remaining cleanup requirements remain in effect. |
This branch has not been deployed
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.
Extracting a chunk of material from the Claude formalization of Fermat's Last Theorem (which is Apache-2.0 licensed), with the intention to use it as the basis for a subsequent formalization of p-adic modular symbols following Mazur-Tate-Teitelbaum.