Repository navigation
Add Fel's Conjecture project; port to v4.30.0-rc2 Mathlib - #24
Conversation
Imports https://github.com/AxiomMath/fel-polynomial into Lean Pool. Provides: - LeanPool/FelConjecture.lean: project card (module docstring) + import. - LeanPool/FelConjecture/Solution.lean: copy of upstream solution.lean. Main result: fels_conjecture (proven via FelsConjectureProof.fels_conjecture_main), relating gap power sums of a numerical semigroup to invariants derived from its Hilbert series. Source: arXiv:2602.03716. Upstream contains no sorrys in the solution file. The companion problem.lean (sorries by design as the problem statement) is intentionally not imported. Port from upstream Lean v4.26.0 / Mathlib v4.26.0 to Lean Pool's v4.30.0-rc2 required exactly one API fix: - Finset.sum_eq_add_sum_diff_singleton changed from taking a membership proof to taking the element explicitly together with an "i not in s implies f i = 0" hypothesis. Two call sites in binomial_sum_minus_j_pow updated. Local checks: - lake build LeanPool: 8317 jobs, no errors. - lake exe mk_all --check: clean. - lake exe runLinter LeanPool: exits 0; reports 26 docBlame / synTaut findings to clean up in follow-up commits on this PR. Style cleanup is intentionally deferred (see PR description checklist): ~200 longLine warnings, 25 docBlame findings, 1 synTaut finding, 3 push_neg deprecations, a few flexible-tactic warnings. The CI warning gate will be red until those clear. projects.yml entry created with status: draft. Solution.lean carries a "-- size-limit-ok" waiver (~2300 nbnc lines vs. 2000 cap); thematic split is planned as a follow-up.
Three issues surfaced when adding the first populated entry to LeanPool/projects.yml: 1. Declaration parser stripped trailing primes from names. The regex used `\b` after `[A-Za-z_][A-Za-z0-9_'.]*`, but `\b` does not treat `'` as a word character, so `lemma foo'` was parsed as `foo` and the subsequent `#print axioms` audit failed with `unknown constant`. Replaced `\b` with a negative lookahead. 2. `_check_file_sizes` ignored `-- size-limit-ok:` waivers, even though CODE_QUALITY.md §5 documents them as the escape hatch for the 2000-line cap. Now honors the same waiver mechanism that `_check_proof_sizes` already uses. 3. `_check_project_card` required the module docstring to immediately follow the file header, but mathlib (and the existing forward_euler project card) place the docstring after the imports. Now searches for the first `/-!` block in the body rather than requiring it at position 0, matching standard Lean style. All 32 existing pytest tests still pass.
- Solution.lean
- Narrow imports: replace broad `import Mathlib` with the four modules
actually needed (Bernoulli, Choose.Sum, PowerSeries.WellKnown,
Tactic). Build drops from 8317 jobs to 3332.
- Wrap every line over 100 columns to satisfy
`linter.style.longLine`.
- Add `/-- ... -/` docstrings to all 25 definitions and structure
fields previously flagged by `docBlame`.
- Replace flexible/deprecated tactics with non-flexible
alternatives: `simp_all` -> `simp_all only` or hand-written
`Finset.sum_bij'` proofs; `simp at hn` ->
`simp only [Finset.mem_range, not_lt] at hn`; `simpa using e` ->
`simp` (or term proof); `refine'` -> `refine`.
- Replace 5 `push_neg` with `push Not` (deprecated in v4.30).
- Drop the unused `[DecidableEq α]` from `sum_factor_scalar'`,
rename the unused `hk` variable to `_hk`, and delete the
syntactic-tautology lemma `sum_extend_to_deg_sum`.
- FelConjecture.lean
- Reformat the project card to start with the auto-generated
schema (Source / Authors / Status / Main declarations / Tags) so
`_check_project_card` recognizes it. Mathematical overview and
provenance live in a follow-up `/-! ... -/` block.
- projects.yml
- Populate `tags` (top-level vocabulary + per-project) with
`number-theory, combinatorics, polynomials`.
- Drop the `url:` key in favor of arxiv-only (the schema requires
exactly one of arxiv/doi/url).
- Status: `verified` (axiom audit confirms only standard
axioms: `propext`, `Classical.choice`, `Quot.sound`).
Local CI pass:
- `lake build LeanPool`: 0 errors, 0 warnings.
- `lake exe mk_all --check`: clean.
- `lake exe runLinter LeanPool`: passed.
- `lake exe lint-style LeanPool`: passed.
- `python -m lean_pool.quality --repo .`: passed.
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | algebraic combinatorics |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a complete Lean formalization of a named published conjectural formula for numerical semigroups, with the main theorem proved from the developed definitions.
Tokens: 55,076 in / 1,772 out · Tier: standard · Cost: $0.3285
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
There was a problem hiding this comment.
Pull request overview
This PR adds a new Lean Pool project formalizing Fel’s conjecture (arXiv:2602.03716), registers it in projects.yml, and updates the repo’s quality tooling to better support large upstream imports and project-card placement.
Shape check (per REVIEW_RULES.md): N = 194, F = 1, A = true, C = true.
Changes:
- Add the Fel’s conjecture formalization (
LeanPool/FelConjecture/Solution.lean) and a documented entry module (LeanPool/FelConjecture.lean). - Register the project (tags, source, status, main declaration) in
LeanPool/projects.yml. - Update the Python quality checker to honor
size-limit-okwaivers and to locate the project card after imports; regenerateLeanPool.lean.
Reviewed changes
Copilot reviewed 4 out of 5 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| python/lean_pool/quality.py | Adjusts quality checks to support size-limit-ok waivers, more robust declaration parsing, and project-card detection after imports. |
| LeanPool/projects.yml | Adds the Fel’s conjecture project metadata (tags, source, status, main declaration). |
| LeanPool/FelConjecture/Solution.lean | Introduces the full formal development and main theorem fels_conjecture. |
| LeanPool/FelConjecture.lean | Adds the entry-point module and project card docstring for rendered docs. |
| LeanPool.lean | Regenerates the umbrella import list to include the new project files. |
| have h₁ : (PowerSeries.coeff 0) (PowerSeries.X * G.scaledExpFactor i) = 0 := by | ||
| simp | ||
| have h₂ : (PowerSeries.coeff 0) (-(G.d i : ℚ) • (PowerSeries.X * | ||
| G.scaledExpFactor i)) = (-(G.d i : ℚ)) * (PowerSeries.coeff 0) (PowerSeries.X * | ||
| G.scaledExpFactor i) := by | ||
| simp | ||
| rw [h₂, h₁] | ||
| ring_nf |
| lemma gap_le_sup {S : NumericalSemigroup} (g : ℕ) (hg : g ∈ S.gaps) : g ≤ S.gaps.sup id := | ||
| Finset.le_sup (f := id) hg | ||
|
|
| lemma neg_one_pow_ne_zero' (m : ℕ) : ((-1 : ℤ) ^ (m + 1)) ≠ 0 := by | ||
| exact Int.neg_one_pow_ne_zero | ||
|
|
||
| lemma hilbertNumerator_natDegree_ge_jstar {S : NumericalSemigroup} (G : | ||
| NumericalSemigroupGenerators S) | ||
| (hnonempty : S.gaps.Nonempty) : | ||
| G.productPolynomial.natDegree + S.gaps.sup id ≤ G.hilbertNumerator.natDegree := by | ||
| apply Polynomial.le_natDegree_of_ne_zero | ||
| rw [hilbertNumerator_coeff_at_jstar G hnonempty] | ||
| exact neg_one_pow_ne_zero' G.m |
It governs Copilot Chat / IDE features, not Copilot's PR review (which reads from .github/instructions/*.instructions.md). Nobody on this project uses Copilot Chat, so the file was dead weight that just created drift risk — caught it on PR #24, where the file was stale relative to the gpt-5.5 prompt rewrite while the actually-used review.instructions.md had been updated. If Copilot Chat use ever resumes, prefer a thin pointer file rather than re-duplicating the rules content. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | combinatorial commutative algebra |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a complete Lean proof of a named conjectural formula relating numerical-semigroup Hilbert numerator syzygy sums to gap power sums and Bernoulli-type generating-series coefficients.
Tokens: 55,076 in / 1,258 out · Tier: flex · Cost: $0.1566
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
…l/fel-conjecture
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | numerical semigroups and combinatorial commutative algebra |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a Lean formalization of a named research-level conjecture from a cited paper, with the expected definitions and final theorem present.
Findings (1)
- unrelated-infrastructure-change —
python/lean_pool/quality.py:277
The PR changes Lean Pool quality-checking policy and parsing behavior while adding a mathematics project. These infrastructure changes should be removed from this PR or split into a separate tooling PR; the mathematical project can then be reviewed on its own.
Tokens: 55,076 in / 1,340 out · Tier: flex · Cost: $0.1578
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
These three fixes were on the unmerged lean-pool-fel branch (PR #24) and never made it onto main. The audit caught their absence. 1. Declaration parser truncated trailing primes. Regex used \b after [A-Za-z_][A-Za-z0-9_'.]*, but \b does not treat ' as a word character, so 'lemma foo'' was parsed as 'foo' and the subsequent #print axioms audit failed with 'unknown constant'. Replaced with a negative lookahead. 2. _check_file_sizes ignored '-- size-limit-ok:' waivers. CODE_QUALITY.md §5 documents the waiver as the escape hatch for the 2000-line cap; _check_proof_sizes already honored it. Added the same waiver here. 3. _check_project_card required the docstring to immediately follow the file header, but mathlib convention is header → imports → docstring. Now searches for the first /-! block in the body. Adds regression tests for each: prime-suffix declaration parses correctly, file-size waiver is honored (and the cap still bites without it), project card after imports is accepted.
Per maintainer feedback on PR #24: - Take main's quality.py verbatim, dropping this PR's three quality.py modifications (size-limit-ok waiver, declaration regex with trailing primes, project-card-after-imports detection). Those should land separately, not as part of the Fel's Conjecture import. - Reorganize LeanPool/projects.yml: drop the top-level `tags:` field (which read like Lean Pool's library-wide vocabulary when it was just typo prevention) and keep the projects list with one element — Fel's project card. Per-project tags remain free-form. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Drop the opaque '-- size-limit-ok: <reason>' escape hatch from _check_file_sizes and _check_proof_sizes. Hard caps with no waivers are easier to reason about. Raise the file-size cap from 2000 to 10000 non-blank, non-comment lines so legitimately large vendored modules fit without an opt-out. Proof cap remains 100 lines. PR #24's vendored Solution.lean (~2826 lines) fits under 10000 without the marker; its size-limit-ok line should be dropped on rebase.
#print axioms emits one of two messages on stdout: 'NAME' depends on axioms: [a, b, c] 'NAME' does not depend on any axioms The new per-declaration audit only matched the first form, so any axiom-free declaration (like 'def hello := "world"', or any pure def/structure/inductive that doesn't transitively use Classical/propext/ Quot.sound) was reported as 'produced no result'. Extend the regex to match both forms. This was the regression that surfaced 13 spurious errors against PR #24 (NumericalSemigroup, hello, and the prime-suffix lemmas).
`_axiom_audit_resolved` and `_parse_axiom_output` parsed Lean's \`#print axioms\` output with `'([^']+)'` to capture the echoed name. That regex cannot match a name containing `'` — Lean's output for a prime-suffixed declaration is `'foo'' depends on axioms: [...]`, and the regex matches up to the first `'` (capturing `foo`, not `foo'`), then expects ` ` but finds `'`, then fails. PR #24 (Fel's Conjecture) has many `_'`-suffixed lemmas (`neg_one_pow_ne_zero'`, `exp_poly_sub_prod'`, `forward_inverse_id'`, etc.). Their axioms were never recorded as resolved, and the audit emitted "axiom audit produced no result for ..." for each. Replace `[^']+` with non-greedy `.+?` and anchor on `' ` (closing quote followed by Lean's mandatory space). Names cannot end in whitespace, so this is unambiguous. Test extended with two prime-suffixed declarations exercising both output forms. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…l/fel-conjecture
Proof profile (new / modified Lean files)
Per-file profile output
|
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | additive number theory and commutative algebra |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a complete Lean formalization of a published named conjecture expressing Fel's syzygy invariant for numerical semigroups in terms of gap power sums and generating-series coefficients.
Tokens: 54,458 in / 1,076 out · Tier: flex · Cost: $0.1523
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
…l/fel-conjecture
|
/review |
🤖 LLM review (
|
| Aspect | Value |
|---|---|
| Fit | ✅ good_fit |
| Level | research |
| Branch | numerical semigroups and combinatorial commutative algebra |
| Mode | theory_building |
| Obscure problem | no |
| Code quality | 3 / 5 |
The contribution is a complete formal proof of a named published conjecture-level identity for invariants of numerical semigroups.
Tokens: 54,458 in / 1,002 out · Tier: standard · Cost: $0.3024
Automated review against .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
Imports the AxiomMath/fel-polynomial formalization of Fel's conjecture on syzygies of numerical semigroups (paper: arXiv:2602.03716) into Lean Pool, ported from Lean v4.26.0 / Mathlib v4.26.0 to v4.30.0-rc2.
What's in this PR
LeanPool/FelConjecture.lean— project card module (matches the auto-generated schema fromLeanPool/projects.yml).LeanPool/FelConjecture/Solution.lean— upstreamsolution.lean, ported and cleaned up.LeanPool/projects.yml— new project entry (statusverified, tagsnumber-theory, combinatorics, polynomials).LeanPool.lean— regenerated vialake exe mk_all.python/lean_pool/quality.py— three bug fixes (see commite161b8c) that surfaced when adding the first populatedprojects.ymlentry: trailing-prime regex, file-size waiver, project-card position.Upstream's
problem.leanis intentionally not imported — it's a problem-statement file with threesorrys by design.solution.leanis self-contained and provesfels_conjecturewith nosorry.Mathlib v4.26 → v4.30 port
Only one Mathlib API change broke compilation:
Finset.sum_eq_add_sum_diff_singletonnow takes the element explicitly together with ani ∉ s → f i = 0hypothesis (instead of a membership proof). Two call sites inbinomial_sum_minus_j_powupdated.Cleanup applied
import Mathlibwith the four modules actually needed (NumberTheory.Bernoulli,Data.Nat.Choose.Sum,RingTheory.PowerSeries.WellKnown,Tactic). Build dropped from 8317 jobs to 3332./-- ... -/docstrings to all 25 definitions and structure fields flagged bydocBlame.simp_all→simp_all onlyor hand-writtenFinset.sum_bij'proofs;simp at hn→simp only [Finset.mem_range, not_lt] at hn;simpa using e→simp/ term proof;refine'→refine.push_negwithpush Not.[DecidableEq α]hypothesis fromsum_factor_scalar', renamed unusedhkto_hk, and deleted the syntactic-tautology lemmasum_extend_to_deg_sum.Local CI pass
lake build LeanPool— 0 errors, 0 warnings.lake exe mk_all --check— clean.lake exe runLinter LeanPool—Linting passed for LeanPool.lake exe lint-style LeanPool— clean.python -m lean_pool.quality --repo .—Quality checks passed.pytest(Python tests for quality.py) — 32 passed.Provenance
Upstream authors: Evan Chen, Kenny Lau, Ken Ono, Jujian Zhang. Upstream license: MIT. The file headers in this PR use Lean Pool's standard Apache 2.0 template per
.github/CODE_QUALITY.md§7, with all four authors credited.