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,467 maxHeartbeats units across 17 files (6,025 added LOC). Sum of Count-heartbeats wall-clock total: 79.99 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.DensityHalesJewett.DensityHalesJewett.Insensitive |
5.00 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.StructuredCorrelation |
4.30 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Varnavides |
3.60 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Main |
3.40 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.FiniteUnions |
3.20 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.UniformFibers |
3.20 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement |
3.20 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.CorrelatedFibers |
3.10 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Word |
3.00 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.Parameters |
3.00 s |
LeanPool.DensityHalesJewett.DensityHalesJewett |
3.00 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Szemeredi |
1.90 s |
Per-file `lean --profile` output
LeanPool/DensityHalesJewett.lean
import took 1.29s
cumulative profiling times:
elaboration 0.237ms
import 1.29s
initialization 31.2ms
interpretation 151ms
linting 0.273ms
module linting 0.00106ms
overlappingInstancesLinter 0.247ms
parsing 0.032ms
tacticAnalysis 0.81ms
real 2.14
user 1.17
sys 0.98
LeanPool/DensityHalesJewett/DensityHalesJewett.lean
import took 1.3s
cumulative profiling times:
elaboration 0.086ms
import 1.3s
initialization 41.8ms
interpretation 152ms
linting 0.185ms
module linting 0.00124ms
overlappingInstancesLinter 0.0954ms
parsing 0.0022ms
tacticAnalysis 0.45ms
real 2.15
user 1.19
sys 0.97
LeanPool/DensityHalesJewett/DensityHalesJewett/Canonization.lean
import took 802ms
cumulative profiling times:
attribute application 0.752ms
compilation (IR) 0.282ms
compilation (LCNF base) 1.99ms
compilation (LCNF impure) 1.27ms
compilation (LCNF mono) 1.95ms
congr simp thm 4.45ms
elaboration 47.6ms
fix level params 1.27ms
import 802ms
initialization 31ms
instantiate metavars 1.82ms
interpretation 238ms
let-to-have transformation 0.13ms
linting 11.2ms
module linting 0.00152ms
overlappingInstancesLinter 5.27ms
parsing 13ms
process pre-definitions 6.3ms
share common exprs 3.19ms
simp 54.5ms
tactic execution 84.6ms
tacticAnalysis 25.6ms
type checking 16.9ms
typeclass inference 14.7ms
real 1.70
user 1.21
sys 0.78
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement.lean
import took 840ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 153ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 158ms
aesop took 136ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 244ms
cumulative profiling times:
aesop 136ms
attribute application 0.129ms
blocked (unaccounted) 15.8ms
congr simp thm 18.1ms
dsimp 6.26ms
elaboration 107ms
fix level params 2.22ms
grind 9.74ms
grind ac 0.00516ms
grind cutsat 0.00954ms
grind ematch 0.178ms
grind linarith 0.00361ms
grind mark subsingleton 0.47ms
grind ring 0.00776ms
grind simp 8.02ms
import 840ms
initialization 31.1ms
instantiate metavars 5.51ms
interpretation 1.14s
let-to-have transformation 0.4ms
linting 38.4ms
module linting 0.00158ms
norm_num 105ms
overlappingInstancesLinter 6.04ms
parsing 21.9ms
process pre-definitions 21.2ms
ring 39.5ms
share common exprs 19.7ms
simp 1.12s
sym canon 0.839ms
sym typeclass inference 0.789ms
tactic execution 307ms
tacticAnalysis 52.2ms
type checking 135ms
typeclass inference 1.83s
real 3.78
user 5.74
sys 0.86
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement/CorrelatedFibers.lean
import took 832ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 131ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 177ms
cumulative profiling times:
attribute application 0.316ms
blocked (unaccounted) 0.0771ms
compilation (IR) 0.437ms
compilation (LCNF base) 3.53ms
compilation (LCNF impure) 1.82ms
compilation (LCNF mono) 3.05ms
congr simp thm 40.4ms
dsimp 13.6ms
elaboration 280ms
fix level params 6.95ms
import 832ms
initialization 38.3ms
instantiate metavars 12.9ms
interpretation 1.61s
let-to-have transformation 2.69ms
linting 99.6ms
module linting 0.00143ms
norm_num 347ms
overlappingInstancesLinter 15.3ms
parsing 63.4ms
process pre-definitions 59.1ms
ring 126ms
share common exprs 62.6ms
simp 567ms
tactic execution 694ms
tacticAnalysis 126ms
type checking 273ms
typeclass inference 1.53s
real 3.27
user 6.62
sys 0.83
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement/Parameters.lean
import took 830ms
simp took 259ms
cumulative profiling times:
attribute application 0.248ms
congr simp thm 5.49ms
elaboration 62.5ms
fix level params 1.58ms
import 830ms
initialization 31.5ms
instantiate metavars 2.32ms
interpretation 665ms
let-to-have transformation 0.282ms
linting 23.2ms
module linting 0.00151ms
norm_num 96.3ms
overlappingInstancesLinter 4.41ms
parsing 17.3ms
process pre-definitions 21.4ms
ring 47.9ms
share common exprs 14.8ms
simp 332ms
tactic execution 193ms
tacticAnalysis 33.6ms
type checking 103ms
typeclass inference 864ms
real 2.45
user 3.21
sys 0.78
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement/StructuredCorrelation.lean
import took 826ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 313ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 427ms
tactic execution of Mathlib.Tactic.Positivity.positivity took 176ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 168ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 568ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 488ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 267ms
cumulative profiling times:
attribute application 0.35ms
blocked (unaccounted) 0.259ms
compilation (IR) 0.994ms
compilation (LCNF base) 9.61ms
compilation (LCNF impure) 5.03ms
compilation (LCNF mono) 7.37ms
congr simp thm 21.4ms
dsimp 6.63ms
elaboration 209ms
fix level params 5.31ms
grind 90.4ms
grind ac 0.0253ms
grind cutsat 1.68ms
grind ematch 9.65ms
grind linarith 0.0156ms
grind mark subsingleton 21.7ms
grind ring 0.3ms
grind simp 95.5ms
import 826ms
initialization 31.6ms
instantiate metavars 12.4ms
interpretation 3.21s
let-to-have transformation 0.737ms
linting 94ms
module linting 0.00179ms
norm_num 273ms
overlappingInstancesLinter 12.7ms
parsing 50ms
process pre-definitions 44.2ms
ring 120ms
share common exprs 49.5ms
simp 243ms
sym canon 8.49ms
sym typeclass inference 25ms
tactic execution 824ms
tacticAnalysis 107ms
type checking 231ms
typeclass inference 1.44s
real 4.46
user 7.85
sys 0.86
LeanPool/DensityHalesJewett/DensityHalesJewett/FiniteUnions.lean
import took 735ms
cumulative profiling times:
attribute application 0.0411ms
congr simp thm 6.36ms
elaboration 20.3ms
fix level params 1.12ms
grind 76.5ms
grind ac 0.0133ms
grind cutsat 0.173ms
grind ematch 2.26ms
grind linarith 0.00861ms
grind mark subsingleton 4.74ms
grind ring 0.128ms
grind simp 81ms
import 735ms
initialization 30.9ms
instantiate metavars 3.74ms
interpretation 236ms
let-to-have transformation 0.0627ms
linting 11.9ms
module linting 0.00142ms
overlappingInstancesLinter 3.84ms
parsing 10.8ms
process pre-definitions 7.58ms
share common exprs 4.41ms
simp 205ms
sym canon 8.26ms
sym typeclass inference 34.7ms
tactic execution 158ms
tacticAnalysis 34.1ms
type checking 48.6ms
typeclass inference 184ms
real 2.03
user 1.77
sys 0.75
LeanPool/DensityHalesJewett/DensityHalesJewett/GrahamRothschild.lean
import took 810ms
cumulative profiling times:
attribute application 0.143ms
blocked (unaccounted) 0.404ms
congr simp thm 5.6ms
elaboration 78.3ms
fix level params 1.71ms
import 810ms
initialization 31.6ms
instantiate metavars 2.18ms
interpretation 267ms
let-to-have transformation 0.169ms
linting 20.4ms
module linting 0.00149ms
overlappingInstancesLinter 7.74ms
parsing 13.5ms
process pre-definitions 7.32ms
share common exprs 4.01ms
simp 85ms
tactic execution 113ms
tacticAnalysis 41.2ms
type checking 22.6ms
typeclass inference 297ms
real 1.81
user 1.63
sys 0.79
LeanPool/DensityHalesJewett/DensityHalesJewett/Insensitive.lean
import took 817ms
cumulative profiling times:
attribute application 3.19ms
blocked (unaccounted) 1.52ms
compilation (IR) 0.373ms
compilation (LCNF base) 3.09ms
compilation (LCNF impure) 1.75ms
compilation (LCNF mono) 3.22ms
congr simp thm 51.5ms
dsimp 11.1ms
elaboration 435ms
fix level params 11.6ms
grind 76.5ms
grind ac 0.0275ms
grind cutsat 0.238ms
grind ematch 7.26ms
grind linarith 0.143ms
grind mark subsingleton 9.45ms
grind ring 0.2ms
grind simp 28.6ms
import 817ms
initialization 31.6ms
instantiate metavars 29.5ms
interpretation 1.52s
let-to-have transformation 19.7ms
linting 212ms
module linting 0.00397ms
norm_num 54.7ms
overlappingInstancesLinter 25.5ms
parsing 112ms
process pre-definitions 80.5ms
ring 52.5ms
share common exprs 57.4ms
simp 855ms
sym canon 10.8ms
sym typeclass inference 88.4ms
tactic execution 1.61s
tacticAnalysis 273ms
type checking 345ms
typeclass inference 2.13s
real 3.71
user 8.68
sys 0.90
LeanPool/DensityHalesJewett/DensityHalesJewett/Main.lean
import took 997ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 148ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 105ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 128ms
cumulative profiling times:
attribute application 0.599ms
blocked (unaccounted) 530ms
compilation (IR) 0.35ms
compilation (LCNF base) 2.9ms
compilation (LCNF impure) 1.42ms
compilation (LCNF mono) 2.76ms
congr simp thm 18.7ms
dsimp 5.77ms
elaboration 178ms
fix level params 2.81ms
grind 118ms
grind ac 0.037ms
grind cutsat 0.64ms
grind ematch 8.44ms
grind linarith 0.0204ms
grind mark subsingleton 14.8ms
grind ring 0.398ms
grind simp 73.7ms
import 997ms
initialization 35.6ms
instantiate metavars 6.96ms
interpretation 1.04s
let-to-have transformation 0.543ms
linting 42.8ms
module linting 0.00156ms
norm_num 103ms
overlappingInstancesLinter 8.76ms
parsing 39.2ms
process pre-definitions 25.2ms
ring 28.4ms
share common exprs 21.6ms
simp 275ms
sym canon 18.9ms
sym typeclass inference 298ms
tactic execution 507ms
tacticAnalysis 78.7ms
type checking 234ms
typeclass inference 993ms
real 3.36
user 4.90
sys 0.90
LeanPool/DensityHalesJewett/DensityHalesJewett/Subspace.lean
import took 784ms
cumulative profiling times:
attribute application 3.4ms
blocked (unaccounted) 61.3ms
compilation (IR) 0.726ms
compilation (LCNF base) 5.5ms
compilation (LCNF impure) 2.95ms
compilation (LCNF mono) 6.42ms
congr simp thm 6.55ms
elaboration 90.8ms
fix level params 1.69ms
import 784ms
initialization 30.8ms
instantiate metavars 1.37ms
interpretation 281ms
let-to-have transformation 0.269ms
linting 19.2ms
module linting 0.00136ms
overlappingInstancesLinter 11.3ms
parsing 17.4ms
process pre-definitions 11.1ms
share common exprs 3.21ms
simp 92ms
tactic execution 76.7ms
tacticAnalysis 39.8ms
type checking 28.3ms
typeclass inference 151ms
real 1.80
user 1.50
sys 0.79
LeanPool/DensityHalesJewett/DensityHalesJewett/Szemeredi.lean
import took 946ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 121ms
cumulative profiling times:
attribute application 1.39ms
blocked (unaccounted) 0.536ms
compilation (IR) 0.0717ms
compilation (LCNF base) 0.796ms
compilation (LCNF impure) 0.383ms
compilation (LCNF mono) 1.05ms
congr simp thm 4.15ms
dsimp 7.48ms
elaboration 36.3ms
fix level params 0.621ms
grind 6.7ms
grind mark subsingleton 0.307ms
grind simp 2.37ms
import 946ms
initialization 31.4ms
instantiate metavars 2.09ms
interpretation 401ms
let-to-have transformation 0.0936ms
linting 20.8ms
module linting 0.00181ms
norm_num 15.8ms
overlappingInstancesLinter 4.89ms
parsing 11.5ms
process pre-definitions 6.77ms
ring 6.53ms
share common exprs 5.93ms
simp 66.3ms
sym canon 1.59ms
sym typeclass inference 29.8ms
tactic execution 203ms
tacticAnalysis 29.4ms
type checking 38.3ms
typeclass inference 288ms
real 2.31
user 1.95
sys 0.86
LeanPool/DensityHalesJewett/DensityHalesJewett/UniformFibers.lean
import took 829ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 269ms
cumulative profiling times:
attribute application 1.83ms
compilation (IR) 0.688ms
compilation (LCNF base) 5.07ms
compilation (LCNF impure) 3.08ms
compilation (LCNF mono) 4.69ms
congr simp thm 34.9ms
dsimp 0.556ms
elaboration 249ms
fix level params 5.13ms
import 829ms
initialization 31.8ms
instantiate metavars 14.2ms
interpretation 1.49s
let-to-have transformation 1.01ms
linting 99.7ms
module linting 0.00157ms
norm_num 186ms
overlappingInstancesLinter 14.5ms
parsing 61.5ms
process pre-definitions 54.4ms
ring 107ms
share common exprs 47.4ms
simp 581ms
tactic execution 852ms
tacticAnalysis 138ms
type checking 306ms
typeclass inference 1.59s
real 3.36
user 6.44
sys 0.88
LeanPool/DensityHalesJewett/DensityHalesJewett/Varnavides.lean
import took 973ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 358ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 245ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 592ms
cumulative profiling times:
attribute application 0.168ms
compilation (IR) 0.333ms
compilation (LCNF base) 4.16ms
compilation (LCNF impure) 1.52ms
compilation (LCNF mono) 3.41ms
congr simp thm 14.6ms
dsimp 8.32ms
elaboration 80.4ms
fix level params 1.79ms
import 973ms
initialization 31.5ms
instantiate metavars 7.96ms
interpretation 1.89s
let-to-have transformation 1.86ms
linting 72ms
module linting 0.0016ms
norm_num 129ms
overlappingInstancesLinter 6ms
parsing 28.8ms
process pre-definitions 30.7ms
ring 54.8ms
share common exprs 20.8ms
simp 351ms
tactic execution 493ms
tacticAnalysis 67.6ms
type checking 243ms
typeclass inference 1.13s
real 4.00
user 5.39
sys 0.88
LeanPool/DensityHalesJewett/DensityHalesJewett/Word.lean
import took 805ms
cumulative profiling times:
attribute application 0.794ms
compilation (IR) 0.0964ms
compilation (LCNF base) 0.931ms
compilation (LCNF impure) 0.432ms
compilation (LCNF mono) 0.701ms
congr simp thm 6.52ms
elaboration 19.1ms
fix level params 0.569ms
import 805ms
initialization 31.2ms
instantiate metavars 0.512ms
interpretation 202ms
let-to-have transformation 0.0614ms
linting 5.91ms
module linting 0.00142ms
norm_num 0.678ms
overlappingInstancesLinter 3.62ms
parsing 4.53ms
process pre-definitions 2.54ms
ring 7.79ms
share common exprs 2.25ms
simp 111ms
tactic execution 36.4ms
tacticAnalysis 11ms
type checking 22ms
typeclass inference 607ms
real 2.14
user 1.76
sys 0.81
LeanPool/DensityHalesJewett/Solution.lean
import took 938ms
cumulative profiling times:
attribute application 0.0213ms
congr simp thm 0.395ms
elaboration 12ms
fix level params 0.0822ms
import 938ms
initialization 32ms
instantiate metavars 0.111ms
interpretation 184ms
let-to-have transformation 0.0397ms
linting 3.24ms
module linting 0.00145ms
overlappingInstancesLinter 3.17ms
parsing 2.36ms
process pre-definitions 0.624ms
share common exprs 0.331ms
simp 3.85ms
tactic execution 9.97ms
tacticAnalysis 11.1ms
type checking 2.17ms
typeclass inference 17.7ms
real 1.78
user 1.00
sys 0.84
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 proof library for combinatorics theorems. No outstanding review finding prevents merging; fresh final-head CI remains necessary. SummaryImports the density Hales–Jewett and Szemerédi formalization, including combinatorial infrastructure, density increments, arithmetic progressions, and asymptotic theorems.
Reviews (12) · 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 faithfully match the Lean statements, with no undisclosed mathematical assumptions. |
| Novelty | ✅ pass |
Searches of the pinned Mathlib sources and existing pool found no duplicate of either headline result. |
| Significance | ✅ pass |
This completed development of density Hales–Jewett, Szemerédi, and Varnavides supersaturation clearly meets the pool’s research-level significance bar. |
| Sources | ✅ pass |
The pinned upstream development supports the advertised results, and the PR credits both that formalization and the Dodos–Kanellopoulos–Tyros proof. |
| Code quality (advisory) | ✅ pass |
Competent, modular Lean with localized API duplication and unnecessary typeclass constraints that can be cleaned up without delaying merge. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Only the disclosed finiteness, positive-density, interval-containment and length hypotheses; intermediate HasDensityHJ assumptions are discharged by the proved alphabet-size induction. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | density Ramsey theory |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The Lean proves density Hales–Jewett for every finite alphabet and finite-interval Szemerédi over ℕ for every k ≥ 3, with thresholds independent of the set and a nonzero progression difference.
The project formalizes major density Ramsey theorems through a substantial development of canonization, insensitive-family tilings, density increments, and averaging; its 6,033 added Lean lines contain ordinary proofs rather than generated certificate bulk.
Code quality findings (2)
- overstrong-typeclass —
LeanPool/DensityHalesJewett/DensityHalesJewett/Subspace.lean:227
mapLineis definitionallycomposeLine, but requires three additional instances. These constraints propagate intoGrahamRothschild.linesandlines_twoColor, and require a localNontrivialinstance inMain.density_increment_chain_step. UsecomposeLinefor forward composition and confine the stronger assumptions to the inverse construction and equivalence.
Evidence:def composeLine (V : Combinatorics.Subspace η α ι) (l : Combinatorics.Line α η) : Combinatorics.Line α ι wherehas no typeclass assumptions. The wrapper isnoncomputable def mapLine [Fintype (η → α)] [DecidableEq (ι → α)] [Nontrivial α] (V : Combinatorics.Subspace η α ι) (l : Combinatorics.Line α η) : Combinatorics.Line α ι := (linesEquiv V l).1. The following lemma explicitly provesmapLine V l = composeLine V l := rfl. - duplicate-definition —
LeanPool/DensityHalesJewett/DensityHalesJewett/Insensitive.lean:850
The tiling and density-increment stages independently define the same subspace pullback asparameterPreimageandpullback. Coordinate padding is likewise implemented separately bytransportSubspace,padExtraSubspace, andUniformFibers.prependFixed, with separate evaluation proofs. This fragments the shared API and duplicates maintenance work. Move the general primitives intoSubspace.leanand implement specialized names through them.
Evidence:parameterPreimageconstructs its result withclassical; apply Finset.univ.filter; intro x; exact V x ∈ D;DensityIncrement/CorrelatedFibers.lean:33definespullbackbyFinset.univ.filter fun x ↦ V x ∈ A. For padding,transportSubspaceusesidxFun c := Sum.elim (fun a ↦ Sum.inl (z a)) V.idxFun (e c), whilepadExtraSubspaceusesidxFun i := match e.symm i with | Sum.inl j => Sum.inl (z j) | Sum.inr j => V.idxFun j.UniformFibers.lean:375repeats the latter construction withfinSumFinEquiv.symmin place ofe.symm.
Tokens: 6,564,549 in / 24,017 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $133.0923 (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 project check fails because Acceptance condition: repair the named defect 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; 17 changed project files, 6,025 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: Finite-density combinatorics and line encodings. 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": "49b6add9d9405b0cef1233c5499622da3d2715a6",
"verdict": "approve",
"assessment": "The density Hales–Jewett theorem and Szemerédi corollary are substantial, faithful results. Their mathematical source and card are unchanged from the prior complete five-rubric approval. The current revision resolves the only blocking integration defect: both umbrella modules now export the existing public dependency closure. A downstream module successfully imports both headline theorems.",
"repair": "Preserved the incoming module migration and merged current main. The registry retains all 217 main cards unchanged plus exactly this project card (218 total); the resulting PR diff contains only this project and its registry/index additions. No checks, options, waivers, or theorem statements were changed.",
"validation": "Warning-free project build (1726 jobs), all 17 module linters, style check, current generated index, downstream public imports, project metadata checks, 266 public declarations’ axiom audit, and compiled environment/backdoor audit passed. The authoritative merged source was rebuilt and re-audited. GitHub now reports MERGEABLE and fresh protected CI is queued; merge remains contingent on those full-pool checks.",
"findings": []
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "0d32b68075cf4a816a34eaf1683845542f24803f",
"verdict": "approve",
"scope": "Resolution review of the two outstanding documentation findings; approval is a recommendation recorded as COMMENT because the authenticated account authors the PR.",
"findings_resolved": [
{
"thread": "PRRT_kwDOSY3yXM6lCTQ9",
"evidence": "Szemeredi.lean now describes ArithmeticProgression over AddMonoid by its actual field diff_ne_zero: a nonzero common difference. The adjacent base-encoding comment uses the same contract, and the singleton-alphabet prose states only that distinct letters give distinct words. The natural-number Szemerédi theorem and every proof remain unchanged."
},
{
"thread": "PRRT_kwDOSY3yXM6lCTRF",
"evidence": "Solution.lean directly describes the asymptotic density bridges and names their explicit-threshold source theorems; it no longer points to an absent local Challenge.lean contract."
}
],
"validation": "All 17 project files retain identical executable Lean tokens to full-CI-green49b6add9. Scoped static/header/forbidden-token/file-size/proof-size/card/reachability and added-line-length checks pass. The incoming normal main mergebccc46721 is preserved, with all218maincards plus the unchanged own card. Index coverage matches all7,963LeanPool/3Challenge/1Solution files, with no missing or duplicate imports.",
"validation_limit": "No compilation or declaration-linter rerun was needed for the comments-only patch. Fresh final-head CI remains required before merge; root owns that decision."
}
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Reviewed current integration head 483c305e0a7ae19cda080cc7417d38d274f8ddff. The project's Lean source is byte-identical to the previously reviewed 0d32b68075cf4a816a34eaf1683845542f24803f; the existing mathematical assessment and fixes carry forward. The merge retains all 218 current-main project cards and this project's complete card, including their original text. The actual pinned mk_all --module --check command passes.
Recommendation: accept once fresh required CI passes. This review covers the lossless main integration; it does not claim another full local rebuild.
Vilin97
removed
the
needs-manual-rebase
|
/review Please reassess exact head |
Vilin97
added
the
needs-maintainer
Daily disposition: needs maintainer — protected merge operationReviewed exact head
The remaining authority boundary is operational: this repository has |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"reviewed_head": "b2ba41a2e56cec46147562229d4d209f0b6ff3ba",
"review_type": "focused incoming-source follow-up",
"verdict": "approve",
"assessment": "Read the full eight-file delta and the subspace, density, and line-composition contracts. transportSubspace, its application theorem, and parameterPreimage move unchanged into the shared Subspace module under the same namespace; padding/prepending now specialize that same coordinate map. pullback delegates to parameterPreimage, with an explicit finite-set extensionality proof relating its density to relativeDensity; it becomes noncomputable and no longer takes DecidableEq. mapLine returns the same composeLine as the former equivalence projection, eliminating unnecessary finiteness, equality, and nontriviality assumptions. The Graham\u2013Rothschild interfaces similarly drop unnecessary decidable equality. Every density increment, line witness, and main Hales\u2013Jewett conclusion retains its former mathematical scope.",
"scope": "Complete own-project delta from 687d498 reviewed. All 17 project files including the umbrella are retained and the project card is unchanged. Prior faithfulness, novelty, significance, and source assessments carry forward; this does not repeat the full project audit.",
"validation": "Changed-source/helper-contract inspection, inventory comparison and git diff --check passed. No fresh local compilation or complete-project linter run is claimed. Fresh required CI at the current head remains necessary before merge.",
"findings": []
}
This branch has not been deployed
1 participant
Imports the density Hales–Jewett and Szemerédi development from gdahia/densityhalesjewett at
1c2f5aa1b99caa8e2a87beacf80f07f066c309d3, including finite unions, Graham–Rothschild, block canonization, density increments, Varnavides averaging, and the proved asymptotic bridges. All 16 substantive upstream Lean modules are preserved; the duplicate upstream open challenge surface is omitted.The Lean/Mathlib 4.34 import records Gabriel Dahia, Apache-2.0 attribution and the declared upstream AI provenance. The asymptotic line theorem removes a provably unused nontriviality assumption while retaining its conclusion.
The final documentation correction describes a generic
ArithmeticProgressionby its actual contract: a nonzero common difference. It also describesSolution.leandirectly as the asymptotic bridge, and explains that wildcard coordinates distinguish distinct alphabet letters. All theorem statements and proofs, including the natural-number Szemerédi endpoint, are unchanged.The branch includes current main, preserving all 218 main project cards and its own card. The prior exact head
49b6add9d9405b0cef1233c5499622da3d2715a6passed full-pool build, linter, quality, axiom and documentation CI. Every project file retains the same executable Lean tokens. Focused local checks pass: executable-token equality, all-library index coverage with no duplicate or missing imports, unchanged project metadata/card, source reachability, headers, forbidden-token and file/proof-size checks. Compilation and declaration linting were not repeated for this documentation-only correction; fresh CI validates the final merged head. Fresh final-head CI remains required before merge. No checks or linter settings changed.