Conversation
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: 1,862 maxHeartbeats units across 11 files (5,588 added LOC). Sum of Count-heartbeats wall-clock total: 60.14 s. Repeated import cost inside Heartbeat values come from Mathlib's 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.ChipFiring.ChipFiringWithLean.Basic |
11.00 s |
LeanPool.ChipFiring.ChipFiringWithLean.Config |
6.70 s |
LeanPool.ChipFiring.ChipFiringWithLean.CFGraphExample |
5.60 s |
LeanPool.ChipFiring.ChipFiringWithLean.Orientation |
4.90 s |
LeanPool.ChipFiring.ChipFiringWithLean.Rank |
4.20 s |
LeanPool.ChipFiring.ChipFiringWithLean.RRGHelpers |
3.60 s |
LeanPool.ChipFiring.ChipFiringWithLean.Algorithms |
3.30 s |
LeanPool.ChipFiring.ChipFiringWithLean.RiemannRoch |
3.00 s |
LeanPool.ChipFiring.ChipFiringWithLean.PalomarSolution |
2.30 s |
LeanPool.ChipFiring.ChipFiringWithLean |
2.20 s |
LeanPool.ChipFiring |
2.10 s |
Per-file `lean --profile` output
LeanPool/ChipFiring.lean
import took 1.85s
cumulative profiling times:
elaboration 0.272ms
import 1.85s
initialization 37.6ms
interpretation 196ms
linting 0.397ms
module linting 0.00283ms
overlappingInstancesLinter 0.68ms
parsing 0.0579ms
tacticAnalysis 3.39ms
real 3.06
user 1.95
sys 1.13
LeanPool/ChipFiring/ChipFiringWithLean.lean
import took 1.77s
cumulative profiling times:
elaboration 0.14ms
import 1.77s
initialization 44.5ms
interpretation 186ms
linting 0.24ms
module linting 0.00228ms
overlappingInstancesLinter 0.177ms
parsing 0.00248ms
tacticAnalysis 0.679ms
real 2.96
user 1.79
sys 1.19
LeanPool/ChipFiring/ChipFiringWithLean/Algorithms.lean
import took 1.71s
cumulative profiling times:
attribute application 12.4ms
compilation (IR) 0.649ms
compilation (LCNF base) 7.27ms
compilation (LCNF impure) 2.8ms
compilation (LCNF mono) 5.44ms
congr simp thm 7.55ms
elaboration 89ms
fix level params 0.408ms
import 1.71s
initialization 40.2ms
instantiate metavars 0.637ms
interpretation 299ms
let-to-have transformation 7.34ms
linting 13.6ms
module linting 0.00223ms
overlappingInstancesLinter 4.65ms
parsing 13.6ms
process pre-definitions 67.4ms
share common exprs 1.6ms
simp 136ms
tactic execution 12.7ms
tacticAnalysis 26.5ms
type checking 80.6ms
typeclass inference 124ms
real 3.33
user 2.44
sys 1.15
LeanPool/ChipFiring/ChipFiringWithLean/Basic.lean
import took 1.72s
process pre-definitions took 105ms
cumulative profiling times:
attribute application 6.95ms
blocked (unaccounted) 503ms
compilation (IR) 1.75ms
compilation (LCNF base) 27.5ms
compilation (LCNF impure) 7.68ms
compilation (LCNF mono) 18.9ms
congr simp thm 37ms
dsimp 88.4ms
elaboration 373ms
fix level params 14.6ms
import 1.72s
initialization 37ms
instantiate metavars 24.5ms
interpretation 1.76s
let-to-have transformation 140ms
linting 192ms
module linting 0.00209ms
norm_num 17.5ms
overlappingInstancesLinter 29.7ms
parsing 106ms
process pre-definitions 257ms
ring 151ms
share common exprs 53.5ms
simp 1.02s
tactic execution 1.33s
tacticAnalysis 268ms
type checking 397ms
typeclass inference 1.16s
real 5.16
user 8.98
sys 1.17
LeanPool/ChipFiring/ChipFiringWithLean/CFGraphExample.lean
import took 1.71s
type checking took 140ms
cumulative profiling times:
attribute application 1.12ms
blocked (unaccounted) 0.559ms
compilation (IR) 1.27ms
compilation (LCNF base) 12.6ms
compilation (LCNF impure) 5.89ms
compilation (LCNF mono) 9.23ms
congr simp thm 0.838ms
elaboration 110ms
fix level params 0.478ms
import 1.71s
initialization 33.9ms
instantiate metavars 1.11ms
interpretation 394ms
let-to-have transformation 0.416ms
linting 21.9ms
module linting 0.00275ms
overlappingInstancesLinter 10.2ms
parsing 18.4ms
process pre-definitions 13.8ms
share common exprs 2.34ms
simp 11.8ms
tactic execution 1.13s
tacticAnalysis 42.1ms
type checking 497ms
typeclass inference 46.2ms
real 3.59
user 3.84
sys 1.16
LeanPool/ChipFiring/ChipFiringWithLean/Config.lean
import took 1.64s
cumulative profiling times:
attribute application 2.88ms
blocked (unaccounted) 215ms
compilation (IR) 0.508ms
compilation (LCNF base) 8ms
compilation (LCNF impure) 2.44ms
compilation (LCNF mono) 4.7ms
congr simp thm 22.8ms
dsimp 98.4ms
elaboration 195ms
fix level params 7.18ms
import 1.64s
initialization 40.8ms
instantiate metavars 11.9ms
interpretation 844ms
let-to-have transformation 41.4ms
linting 72.5ms
module linting 0.00273ms
norm_num 10.6ms
overlappingInstancesLinter 9.68ms
parsing 47.4ms
process pre-definitions 104ms
ring 69.5ms
share common exprs 25ms
simp 404ms
tactic execution 509ms
tacticAnalysis 107ms
type checking 174ms
typeclass inference 628ms
real 4.03
user 4.85
sys 1.15
LeanPool/ChipFiring/ChipFiringWithLean/Orientation.lean
import took 1.73s
cumulative profiling times:
attribute application 0.965ms
blocked (unaccounted) 379ms
compilation (IR) 0.844ms
compilation (LCNF base) 8.9ms
compilation (LCNF impure) 3.96ms
compilation (LCNF mono) 8.53ms
congr simp thm 33ms
dsimp 57.7ms
elaboration 214ms
fix level params 10.9ms
import 1.73s
initialization 37ms
instantiate metavars 16.5ms
interpretation 1.36s
let-to-have transformation 1.3ms
linting 100ms
module linting 0.00235ms
norm_num 29ms
overlappingInstancesLinter 16.7ms
parsing 71.2ms
process pre-definitions 51.8ms
ring 141ms
share common exprs 43.8ms
simp 580ms
tactic execution 839ms
tacticAnalysis 174ms
type checking 246ms
typeclass inference 671ms
real 4.36
user 6.26
sys 1.15
LeanPool/ChipFiring/ChipFiringWithLean/PalomarSolution.lean
import took 1.68s
cumulative profiling times:
attribute application 0.0372ms
congr simp thm 0.423ms
elaboration 13.6ms
fix level params 0.388ms
import 1.68s
initialization 40.4ms
instantiate metavars 0.397ms
interpretation 245ms
let-to-have transformation 0.0424ms
linting 4.89ms
module linting 0.00179ms
norm_num 0.558ms
overlappingInstancesLinter 2.24ms
parsing 2.93ms
process pre-definitions 1.62ms
ring 10.6ms
share common exprs 1.9ms
simp 10.4ms
tactic execution 24ms
tacticAnalysis 7.86ms
type checking 16.2ms
typeclass inference 31.1ms
real 2.86
user 1.91
sys 1.06
LeanPool/ChipFiring/ChipFiringWithLean/RRGHelpers.lean
import took 1.66s
cumulative profiling times:
attribute application 0.301ms
congr simp thm 9.76ms
dsimp 13.1ms
elaboration 103ms
fix level params 5.27ms
import 1.66s
initialization 37.8ms
instantiate metavars 7.05ms
interpretation 732ms
let-to-have transformation 0.27ms
linting 60.3ms
module linting 0.0027ms
norm_num 9.15ms
overlappingInstancesLinter 7.84ms
parsing 35.5ms
process pre-definitions 25.7ms
ring 74ms
share common exprs 20ms
simp 100ms
tactic execution 407ms
tacticAnalysis 86.7ms
type checking 116ms
typeclass inference 341ms
real 3.27
user 3.56
sys 1.15
LeanPool/ChipFiring/ChipFiringWithLean/Rank.lean
import took 1.67s
cumulative profiling times:
attribute application 0.351ms
congr simp thm 4.54ms
dsimp 4.85ms
elaboration 78.6ms
fix level params 3.28ms
import 1.67s
initialization 38.6ms
instantiate metavars 3.71ms
interpretation 580ms
let-to-have transformation 0.236ms
linting 33.3ms
module linting 0.00224ms
norm_num 16ms
overlappingInstancesLinter 6.25ms
parsing 27.7ms
process pre-definitions 16.4ms
ring 52.9ms
share common exprs 14.7ms
simp 118ms
tactic execution 254ms
tacticAnalysis 51.8ms
type checking 97.3ms
typeclass inference 259ms
real 3.17
user 3.07
sys 1.15
LeanPool/ChipFiring/ChipFiringWithLean/RiemannRoch.lean
import took 1.67s
cumulative profiling times:
attribute application 0.577ms
blocked (unaccounted) 0.285ms
congr simp thm 2.78ms
dsimp 5.45ms
elaboration 75ms
fix level params 4.62ms
import 1.67s
initialization 36.6ms
instantiate metavars 5.69ms
interpretation 842ms
let-to-have transformation 0.757ms
linting 46.1ms
module linting 0.00155ms
norm_num 46ms
overlappingInstancesLinter 5.38ms
parsing 19.7ms
process pre-definitions 26ms
ring 142ms
share common exprs 27.9ms
simp 26.4ms
tactic execution 363ms
tacticAnalysis 59.9ms
type checking 120ms
typeclass inference 310ms
real 3.28
user 3.52
sys 1.15
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
changed the title
Automation disposition: needs-maintainerReviewed exact head No concrete author-actionable defect was established in this bounded review that would justify an ordinary change request. The PR is still marked draft, so protected merge is not permitted. Maintainer decision required: confirm the headline result's significance, faithfulness, novelty, source/provenance and scope, then ask the author to mark the PR ready (or give scope direction). This is a maintainer disposition, not an approval. |
Vilin97
added
the
needs-maintainer
|
/review |
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low risk] Adds mathematical library code for chip-firing graph theory. No outstanding review finding blocks merging, though independent validation of the upstream source and measured build cost remains open. SummaryImports the chip-firing development, including graph divisors, reduction algorithms, Riemann–Roch, Clifford’s theorem, and a project catalog entry. No new actionable issue was identified in the changes since the previous review. Reviews (19) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
Both card headlines are faithfully proved for finite connected loopless multigraphs. |
| Novelty | ✅ pass |
Full-diff review and searches of pinned Mathlib v4.34.0 and pooled projects found no duplicate of either graph-divisor headline. |
| Significance | ✅ pass |
This substantial, self-contained development of graph divisor theory meets the significance bar without a generated-bulk maintenance burden. |
| Sources | ✅ pass |
The citations support the stated results in Corry–Perkinson, variants are labelled, and the pinned upstream formalization is explicitly credited. |
| Code quality (advisory) | ✅ pass |
The development is competent overall, with two unnecessary public theorem hypotheses worth removing for easier reuse. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Connectivity and Clifford’s nonnegative-rank conditions match the card’s connected-graph and special-divisor hypotheses; CFGraph supplies the finite, nonempty, loopless multigraph domain, while rank existence and the required reduction and orientation results are proved internally. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | algebraic graph theory |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The Lean proves r(D) − r(K−D) = deg(D) + 1 − g for every divisor, and r(D) ≤ deg(D)/2 in ℚ when both ranks are nonnegative; the wrappers’ rank predicates have proved existence and uniqueness.
The project develops reduced divisors, superstability, orientations, and ranks into proofs of Baker–Norine graph Riemann–Roch and the graph analogue of Clifford’s theorem.
Code quality findings (1)
- unused-hypothesis —
LeanPool/ChipFiring/ChipFiringWithLean/Orientation.lean:492
Remove the second acyclicity hypothesis from orientation_determined_by_indegrees: its proof only needs acyclicity of O. Likewise, superstable_of_divisor_negative_k in RRGHelpers.lean:76–91 never uses its superstability hypothesis; Config already supplies the nonnegativity needed by config_eff. These assumptions impose unnecessary proof obligations on downstream callers.
Evidence: Orientation.lean:isAcyclic G O → isAcyclic G O' → (∀ v : G.V, indeg G O v = indeg G O' v) → O = O' := by;intro h_acyc h_acyc' h_indeg_eq; the acyclicity application issubset_source G O T h_T_nonempty h_acyc, with no use of h_acyc'. RRGHelpers.lean, superstable_of_divisor_negative_k:superstable G q c → k < 0 := by;intro h_not_winnable c k h_equiv h_super; effectivity follows fromexact (config_eff (configDegree c + k) c).2 (by linarith), and the proof ends withexact winnable_equiv_winnable G D' D h_winnable_D' h_equiv.symm, without using h_super.
Tokens: 6,884,594 in / 23,200 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $139.4319 (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.
# Conflicts: # LeanPool.lean
Changes requested by automated reviewReviewed exact current head The exact-head Build pool and Build project checks fail because Acceptance condition: repair the named defects on a new head and make all required protected checks green. Do not change repository policy or add waivers. |
Vilin97
removed
the
needs-maintainer
Changes requested by automated reviewReviewed head
Review coverage: complete changed-file inventory and full diff retained; 11 changed project files, 5,681 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Divisor rank and reduced-divisor infrastructure; overlaps supporting graph theory in #510, not its endpoints. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head. |
Vilin97
added
the
needs-manual-rebase
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "b8c44faaebffc40595a258ec2aae80c9b356a00e",
"verdict": "approve",
"assessment": "The completed graph Riemann\u2013Roch and Clifford theorems retain the statements and proofs covered by the prior complete five-rubric approval. The incoming module-system migration and main integration are preserved. This revision repairs the remaining experimental reduction API defect: the loop now returns none on fuel exhaustion and some only when its reduction stopping condition holds; findQReducedDivisor propagates that result.",
"repair": "One file changed (8 added, 10 removed lines). The only external caller of findQReducedDivisorLoop is its wrapper in the same file; the Riemann\u2013Roch proof does not depend on this algorithm. Existing wrappers dhar and isWinnable keep their signatures and failure behavior.",
"validation": "The modified Algorithms module and its three local dependencies compile warning-free with the unchanged package options. Three separately compiled proofs verify zero-fuel failure, successful completion with fuel, and failure after one unfinished step. Source/header/size checks and git diff checks pass. The exact parent head had successful full CI, including repository lint and trust gates. A new local linter run has not completed: script execution encountered a missing toolchain private artifact, and the shared memory-safe build slot is occupied. Fresh authoritative CI must pass on this new head before merge.",
"findings": []
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Current-main reconciliation at ef954fca68a3f791e38bf8a784da7d8e87ea41ed.
Merged main 0e9b057b62cc4eaa1b4a42cf23766cf7b9bd3537 normally into the previously reviewed head 58507d115778ab5ccebdb0e605f63a7dff6e9eb3. All 11 Lean files in LeanPool.ChipFiring remain byte-for-byte identical. All 218 main project cards and this PR's own unchanged card are preserved, with both parsed-value and original-card-text checks (only trailing separator whitespace ignored). The actual pinned mk_all --module --check passed, and the refresh introduces no whitespace errors.
The prior substantive review carries forward because this refresh changes none of this project's Lean source or stated results. No new local compiler job was started for the refresh. Acceptance remains conditional on fresh required CI for this exact merged head.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed current-main integration 4b6522f1c4e499380df0e6c4545657d379a8025d. All 11 project files remain byte-identical to the previously reviewed head ef954fca68a3f791e38bf8a784da7d8e87ea41ed. All 219 main cards and the project's own card retain their values and original payload bytes; the actual pinned mk_all --module --check passes. The prior substantive review and source validation carry forward unchanged. Fresh required CI at this exact integration commit remains necessary before normal merge.
Vilin97
removed
the
needs-manual-rebase
Changes requested by automated reviewReviewed
Acceptance condition: propagate an explicit unknown/fuel-exhausted result, or provide the necessary connectedness/termination and correctness contract; alternatively remove the unused exploratory algorithm surface from this completed formalization. The whole-file “experimental” disclaimer does not make a Boolean negative into an unwinnability certificate. Keep the established mathematical theorem statements unchanged and pass the ordinary gates. The source census found no consumers of these decision wrappers outside this module, so a bounded repair is available; closure or |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "Focused repair review at 9b476e6. ChipFiring.CF.isWinnable intentionally changes its public return type from Bool to Option Bool: effective divisors return some true immediately, exhausted preprocessing or reduction returns none, and completed reduction retains the source-coordinate sign test. This fixes the reported effective-divisor counterexample and distinguishes an inconclusive search from unwinnability. There are no in-project callers to migrate; the other ten project files, headline mathematics, incoming cards, index and configuration are unchanged. The exact repaired module compiled warning-free. Five regression proofs also compiled warning-free: on two isolated vertices, wealth (0,0) gives some true, (0,-1) gives none during preprocessing, and (-1,0) gives none during reduction; on one edge, (-1,1) gives some true and (-1,0) gives some false. A strict isWinnable axiom inspection found only propext, Classical.choice and Quot.sound. Four scoped static checks, actual-target style, and the pinned native index check passed; source, configuration and six reused module artifacts were hash-verified. Independent source review passed. This approves the bounded repair and carries forward the prior source assessment, with fresh required full-project CI still pending; it is not a general algorithm-correctness proof or a whole-project compiler claim.",
"assessment": {
"scope": "Winnability result and effective-input bug fix",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The explicit inconclusive result corrects the observable behavior while making the intentional public type change clear; current required CI must pass before merge."
},
"verdict": "approve",
"findings": []
}
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
Vilin97
added
the
needs-maintainer
|
Reviewed exact head The complete prior review was carried forward after checking the project source/card and inspecting the repair delta; prior local validation is inherited evidence. Previous rubric review. The original maintainer blocker is resolved; clearing Observed checks: Successor-head reconciliation ( |
Vilin97
added
needs-maintainer
|
Disposition: needs-maintainer — protected merge operation. Reviewed head The remaining maintainer decision is to authorize normal protected auto-merge or arrange serialized current-main integration and protected merging. No mathematical blocker justifies requested changes or closure; no protected merge is queued. This label records the unresolved operational authority/coordination decision and must be removed before merge. Repository settings and protection were not changed. |
This branch has not been deployed
1 participant
Imports the full chip-firing and graph-divisor development from dhyeymavani2003/chip-firing-with-lean at
5b422d855c02af60591121ba7c11b5e8242542b8: all ten production Lean modules, including algorithms, examples, the graph Riemann–Roch theorem and proved submission bridge. Duplicate open statements and documentation build harnesses are excluded; their completed mathematical content remains present.Ports the complete source to Lean/Mathlib v4.34.0, retains upstream authorship and Apache licensing, documents public APIs, and makes the five recursive algorithm helpers explicit without changing their fuel bounds or behavior. Uses the declared mixed proof provenance.
Validation: warning-free targeted build, all 15 Lean linters, style, generated index, project metadata, static quality, public-declaration axiom audit and compiled-environment audit pass. Full integration CI and independent review are pending for the migrated head. Never merged.
Current checkpoint
7d32440a1preserves the automated main merge and migrates all 11 retained files to the Lean module system. Its warning-free build, all 15 declaration linters, style, module-index and compiled audits pass. Fresh CI is pending. The PR’s existing ready-for-review state is preserved.