Repository navigation
Import Shelah's bound for Hales–Jewett and update density Hales–Jewett to explicit bounds - #781
Merged
Conversation
Import the formalization of Shelah's proof of the Hales–Jewett theorem from "Primitive recursive bounds for van der Waerden numbers" (J. Amer. Math. Soc. 1 (1988), doi:10.1090/S0894-0347-1988-0929498-X), from gdahia/ShelahHalesJewett at 8a91fc0: the insensitive subspace, the Hales–Jewett theorem in dimension shelahBound, and the bound shelahBound k r < ack 5 (2k + r). The library moves under LeanPool.ShelahHalesJewett with its imports rewritten. The Palomar Challenge and Solution modules are left out, since Solution only restates the library theorem. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Update the density Hales–Jewett project to gdahia/DensityHalesJewett at 478533c, which states the density Hales–Jewett, Szemerédi and Varnavides theorems with thresholds given by the Ackermann function, built on Shelah's bound from LeanPool.ShelahHalesJewett. The library moves from LeanPool.DensityHalesJewett.DensityHalesJewett to LeanPool.DensityHalesJewett, and the Palomar Solution module is dropped, since it only restates the library theorems. pullback stays defined from parameterPreimage, as in the previous pool version. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
|
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 issue was found in the current changes. SummaryImports Shelah’s Hales–Jewett bound and uses it to give explicit Ackermann bounds for density Hales–Jewett, Szemerédi’s theorem, and Varnavides’ theorem.
Reviews (2) · Last reviewed commit: "Keep the Lean Pool layout of density Hal..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Collaborator
|
/review |
Restore the modules under LeanPool.DensityHalesJewett.DensityHalesJewett, the root and aggregator modules, and Solution with the asymptotic forms of the density theorems, now derived from the Ackermann thresholds. The card keeps its entries and adds the explicit theorems. Define composeLine as an alias of Combinatorics.Subspace.compLine from LeanPool.ShelahHalesJewett instead of repeating its definition. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
Proof profile (new / modified Lean files)
This build covers the added modules and their dependency cones on top of the measurement environment; modified files are measured without rebuilding the pool. Statement changes
|
| File | Δ lines | HB base | HB head | Δ HB | Δ HB % | Wall base (s) | Wall head (s) |
|---|---|---|---|---|---|---|---|
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement/Parameters.lean |
+75/-147 | 71,443 | 36,355 | -35,088 | -49.1% | 6.25 | 4.45 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Varnavides.lean |
+196/-288 | 111,635 | 94,735 | -16,901 | -15.1% | 8.98 | 12.92 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Word.lean |
+20/-20 | 48,210 | 48,232 | +22 | +0.0% | 5.19 | 4.36 |
| Total | +291/-455 | 231,288 | 179,321 | -51,967 | -22.5% | 20.4 | 21.7 |
New files — absolute profile
Total heartbeats: 315,997 maxHeartbeats units across 8 valid files (3,408 added LOC).
Sum of lean --profile: 21998.8 ms (= 22.00 s) across 8 valid files. Import-excluded time: 16500.8 ms (= 16.50 s).
Count-heartbeats wall-clock total: 34.07 s. Repeated import cost inside lean --profile: 5498.0 ms (= 5.50 s).
Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.
LOC counts added lines in the profiled Lean files from this PR diff.
| File | LOC | Heartbeats (maxHB) | Count wall (s) | lean --profile (s) |
Without import (s) | Import (s) | Commands | Errors |
|---|---|---|---|---|---|---|---|---|
LeanPool/DensityHalesJewett/DensityHalesJewett/Ackermann.lean |
643 | 149,509 | 10.84 | 13.71 | 12.17 | 1.54 | 168 | 0 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Induction.lean |
329 | 94,862 | 7.07 | 2.74 | 2.04 | 0.70 | 50 | 0 |
LeanPool/ShelahHalesJewett/HalesJewett.lean |
207 | 33,432 | 4.65 | 1.27 | 0.73 | 0.54 | 17 | 0 |
LeanPool/ShelahHalesJewett/Ackermann.lean |
105 | 20,642 | 3.08 | 1.25 | 0.70 | 0.55 | 23 | 0 |
LeanPool/DensityHalesJewett/DensityHalesJewett/HalesJewett.lean |
37 | 9,882 | 3.06 | 0.77 | 0.24 | 0.53 | 6 | 0 |
LeanPool/ShelahHalesJewett/Line.lean |
100 | 7,669 | 2.02 | 0.93 | 0.40 | 0.53 | 20 | 0 |
LeanPool/ShelahHalesJewett.lean |
29 | 0 | 1.66 | 0.67 | 0.11 | 0.55 | 3 | 0 |
LeanPool/ShelahHalesJewett/Imports.lean |
12 | 0 | 1.69 | 0.66 | 0.10 | 0.56 | 1 | 0 |
LeanPool/DensityHalesJewett.lean |
6 | — | — | — | — | — | 0 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett.lean |
3 | — | — | — | — | — | 0 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Canonization.lean |
79 | — | — | — | — | — | 0 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement.lean |
105 | — | — | — | — | — | 25 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement/CorrelatedFibers.lean |
207 | — | — | — | — | — | 52 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/DensityIncrement/StructuredCorrelation.lean |
217 | — | — | — | — | — | 57 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/FiniteUnions.lean |
151 | — | — | — | — | — | 0 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/GrahamRothschild.lean |
70 | — | — | — | — | — | 28 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Insensitive.lean |
550 | — | — | — | — | — | 144 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Main.lean |
122 | — | — | — | — | — | 0 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Subspace.lean |
62 | — | — | — | — | — | 0 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/Szemeredi.lean |
84 | — | — | — | — | — | 27 | 1 |
LeanPool/DensityHalesJewett/DensityHalesJewett/UniformFibers.lean |
281 | — | — | — | — | — | 90 | 1 |
LeanPool/DensityHalesJewett/Imports.lean |
3 | — | — | — | — | — | 0 | 1 |
LeanPool/DensityHalesJewett/Solution.lean |
6 | — | — | — | — | — | 11 | 1 |
| Total | 3,408 | 315,997 | 34.07 | 22.00 | 16.50 | 5.50 | 722 | 15 |
Aggregate phase totals
| Phase | Time |
|---|---|
blocked (unaccounted) |
8750.0 ms (= 8.75 s) |
import |
5498.0 ms (= 5.50 s) |
interpretation |
1833.4 ms (= 1.83 s) |
typeclass inference |
1687.1 ms (= 1.69 s) |
tactic execution |
935.6 ms (= 0.94 s) |
type checking |
720.2 ms (= 0.72 s) |
simp |
374.3 ms (= 0.37 s) |
grind |
344.0 ms (= 0.34 s) |
elaboration |
332.6 ms (= 0.33 s) |
sym typeclass inference |
295.8 ms (= 0.30 s) |
grind simp |
241.1 ms (= 0.24 s) |
initialization |
213.3 ms (= 0.21 s) |
Slowest changed modules (from lake build)
| Changed module | Lake time |
|---|---|
LeanPool.DensityHalesJewett.DensityHalesJewett.UniformFibers |
3.50 s |
LeanPool.ShelahHalesJewett.Line |
2.90 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Word |
2.90 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.Parameters |
2.90 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Ackermann |
2.60 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Insensitive |
2.50 s |
LeanPool.ShelahHalesJewett.Ackermann |
2.00 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.CorrelatedFibers |
1.90 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.FiniteUnions |
1.80 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Induction |
1.70 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.Canonization |
1.60 s |
LeanPool.DensityHalesJewett.DensityHalesJewett.HalesJewett |
1.50 s |
Per-file `lean --profile` output
LeanPool/DensityHalesJewett/DensityHalesJewett/Ackermann.lean
import took 1.54s
cumulative profiling times:
attribute application 0.558ms
blocked (unaccounted) 8.75s
compilation (IR) 0.738ms
compilation (LCNF base) 3.73ms
compilation (LCNF impure) 2.84ms
compilation (LCNF mono) 3.4ms
congr simp thm 10.8ms
declTypeLinter 14.2ms
elaboration 204ms
fix level params 2ms
grind 154ms
grind ac 2.3ms
grind cutsat 1.79ms
grind ematch 31.5ms
grind linarith 0.504ms
grind mark subsingleton 20.4ms
grind ring 1.37ms
grind simp 108ms
import 1.54s
initialization 24.9ms
instantiate metavars 4.07ms
interpretation 628ms
let-to-have transformation 0.688ms
linting 85.9ms
module linting 0.00834ms
norm_num 49.7ms
parsing 40.2ms
process pre-definitions 26ms
ring 38.5ms
share common exprs 18.8ms
simp 110ms
sym canon 37.7ms
sym typeclass inference 139ms
tactic execution 550ms
tacticAnalysis 12.7ms
type checking 418ms
typeclass inference 670ms
real 3.83
user 3.76
sys 0.90
LeanPool/DensityHalesJewett/DensityHalesJewett/HalesJewett.lean
import took 530ms
cumulative profiling times:
attribute application 0.0123ms
congr simp thm 0.472ms
declTypeLinter 1.58ms
elaboration 3.29ms
fix level params 0.0876ms
import 530ms
initialization 24.7ms
instantiate metavars 0.119ms
interpretation 93ms
let-to-have transformation 0.0151ms
linting 1.83ms
module linting 0.00847ms
parsing 1.19ms
process pre-definitions 0.456ms
share common exprs 0.241ms
simp 9.11ms
tactic execution 7.01ms
tacticAnalysis 1.14ms
type checking 1.36ms
typeclass inference 99.3ms
real 1.34
user 0.74
sys 0.64
LeanPool/DensityHalesJewett/DensityHalesJewett/Induction.lean
import took 701ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 122ms
cumulative profiling times:
attribute application 0.801ms
compilation (IR) 0.162ms
compilation (LCNF base) 1.4ms
compilation (LCNF impure) 0.623ms
compilation (LCNF mono) 1.16ms
congr simp thm 7.92ms
declTypeLinter 5.7ms
elaboration 68.1ms
fix level params 1.75ms
grind 61.6ms
grind ac 0.0329ms
grind cutsat 0.852ms
grind ematch 3.03ms
grind linarith 0.0202ms
grind mark subsingleton 6.15ms
grind ring 0.349ms
grind simp 29.4ms
import 701ms
initialization 25.2ms
instantiate metavars 3.92ms
interpretation 571ms
let-to-have transformation 0.339ms
linting 26.1ms
module linting 0.00982ms
norm_num 72.6ms
parsing 17.2ms
process pre-definitions 15.6ms
ring 25.7ms
share common exprs 15.4ms
simp 147ms
sym canon 6.81ms
sym typeclass inference 98.1ms
tactic execution 217ms
tacticAnalysis 5.9ms
type checking 120ms
typeclass inference 487ms
real 1.94
user 2.58
sys 0.76
LeanPool/ShelahHalesJewett.lean
import took 553ms
cumulative profiling times:
declTypeLinter 0.627ms
elaboration 0.171ms
import 553ms
initialization 31.2ms
interpretation 80.8ms
linting 0.518ms
module linting 0.00931ms
parsing 0.0552ms
tacticAnalysis 0.647ms
real 1.24
user 0.62
sys 0.66
LeanPool/ShelahHalesJewett/Ackermann.lean
import took 548ms
cumulative profiling times:
attribute application 0.0703ms
congr simp thm 1.36ms
declTypeLinter 3.48ms
elaboration 16ms
fix level params 0.145ms
grind 93.9ms
grind ac 0.077ms
grind cutsat 4.21ms
grind ematch 7.87ms
grind linarith 0.0105ms
grind mark subsingleton 10.4ms
grind ring 0.41ms
grind simp 59.8ms
import 548ms
initialization 25.4ms
instantiate metavars 1.03ms
interpretation 135ms
let-to-have transformation 0.0803ms
linting 6.6ms
module linting 0.0099ms
parsing 4.59ms
process pre-definitions 1.33ms
share common exprs 0.864ms
simp 10.6ms
sym canon 10.3ms
sym typeclass inference 49.1ms
tactic execution 51.7ms
tacticAnalysis 2.6ms
type checking 140ms
typeclass inference 61.1ms
real 1.50
user 1.16
sys 0.69
LeanPool/ShelahHalesJewett/HalesJewett.lean
import took 538ms
cumulative profiling times:
attribute application 0.0535ms
blocked (unaccounted) 0.0292ms
compilation (IR) 0.262ms
compilation (LCNF base) 2ms
compilation (LCNF impure) 1.1ms
compilation (LCNF mono) 1.59ms
congr simp thm 2.84ms
declTypeLinter 3.89ms
elaboration 15.5ms
fix level params 0.583ms
grind 8.67ms
grind ac 0.00312ms
grind cutsat 0.00586ms
grind ematch 0.183ms
grind linarith 0.00226ms
grind mark subsingleton 0.924ms
grind ring 0.00378ms
grind simp 15.4ms
import 538ms
initialization 25.5ms
instantiate metavars 1.93ms
interpretation 125ms
let-to-have transformation 0.0627ms
linting 8.14ms
module linting 0.00973ms
parsing 5.03ms
process pre-definitions 5.89ms
share common exprs 2.47ms
simp 68.9ms
sym canon 1.38ms
sym typeclass inference 0.498ms
tactic execution 88.1ms
tacticAnalysis 2.41ms
type checking 15.1ms
typeclass inference 326ms
real 1.54
user 1.20
sys 0.67
LeanPool/ShelahHalesJewett/Imports.lean
import took 556ms
cumulative profiling times:
declTypeLinter 0.104ms
elaboration 0.0855ms
import 556ms
initialization 30.4ms
interpretation 72.6ms
linting 0.199ms
module linting 0.00833ms
parsing 0.00252ms
tacticAnalysis 0.106ms
real 1.23
user 0.60
sys 0.66
LeanPool/ShelahHalesJewett/Line.lean
import took 532ms
cumulative profiling times:
attribute application 1.24ms
compilation (IR) 0.2ms
compilation (LCNF base) 1.34ms
compilation (LCNF impure) 0.818ms
compilation (LCNF mono) 1.39ms
congr simp thm 2.04ms
declTypeLinter 3.36ms
elaboration 25.5ms
fix level params 0.48ms
grind 25.8ms
grind ac 0.0185ms
grind cutsat 0.332ms
grind ematch 3.15ms
grind linarith 0.0111ms
grind mark subsingleton 2.84ms
grind ring 0.0425ms
grind simp 28.5ms
import 532ms
initialization 26ms
instantiate metavars 0.728ms
interpretation 128ms
let-to-have transformation 0.0473ms
linting 6.1ms
module linting 0.00993ms
parsing 3.62ms
process pre-definitions 2.83ms
share common exprs 1.19ms
simp 28.7ms
sym canon 3.08ms
sym typeclass inference 9.13ms
tactic execution 21.8ms
tacticAnalysis 2.9ms
type checking 25.7ms
typeclass inference 43.7ms
real 1.39
user 0.86
sys 0.68
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Collaborator
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
Both cards faithfully describe the Lean results; both project entry modules build locally, while CI remains pending. |
| Novelty | ✅ pass |
The explicit bounds genuinely extend the existing Mathlib and pooled results; no duplicate added headline was identified. |
| Significance | ✅ pass |
The quantitative Hales–Jewett and density-theorem development is research-level content suitable for pooling; CI remains pending. |
| Sources | ✅ pass |
The Shelah and Dodos–Kanellopoulos–Tyros citations support the attributed arguments; the explicit Ackermann estimates are derived in Lean, and both upstream formalizations are credited. |
| Code quality (advisory) | ✅ pass |
The shared AckBounded and IsTiling APIs replace repeated bookkeeping, and composeLine delegates to the Shelah implementation; I found no material maintenance issue. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Only the hypotheses stated in the cards; intermediate density-theorem hypotheses are discharged by the binary base case and alphabet induction. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | Ramsey theory |
| Mode | theory_building |
| Code quality | 4 / 5 |
Statement check: The exported theorems establish the stated Shelah bound, insensitivity lemma, Ackermann thresholds, and nonconstant arithmetic-progression existence and counts.
The PR proves Shelah’s recursive Hales–Jewett bound and its Ackermann estimate, then develops explicit bounds for density Hales–Jewett, Szemerédi, and Varnavides through finite unions, canonization, and density increments.
Tokens: 23,817,440 in / 43,764 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $95.9262 (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
approved these changes
Nov 8, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
There was a problem hiding this comment.
Approve source inclusion at 99835bfc8cf4fd30eb71467e105661e1094150ab.
I checked the Shelah recurrence and two-letter insensitivity argument, the density increment/alphabet induction, explicit Ackermann thresholds, digital transfer to Szemerédi, and Varnavides counting. The lines retain a genuine wildcard and the counted progressions require nonzero difference; intermediate density hypotheses are discharged by the development.
The quantitative results substantially extend the qualitative Hales–Jewett result in pinned Mathlib and the previous pooled density library. The scoped Mathlib, Tau Ceti and pool comparison identified no duplicate headline provider. Both pinned upstream formalizations have Apache-2.0 licenses and the cards disclose AI proof provenance. The arguments align with Shelah’s paper and Dodos–Kanellopoulos–Tyros; the exact numerical Ackermann estimates are derived in Lean rather than quoted as constants from those papers.
The new commit restores the exact public interfaces of exists_of_density_atTop and exists_of_density_nat_atTop through the exported Solution module. Their proofs choose the established explicit thresholds and preserve the nonzero progression difference. The implementation moves preserve the mathematical programs, and composeLine now delegates to the shared Shelah provider. I verified the complete current source/native delta and acyclic import graph; the global index, gates and unrelated projects are unchanged.
I read the current five-rubric report (job2412) independently. No material source finding remains in this review. Hosted validation and protected merge-queue validation remain separate requirements; no local compilation is claimed here.
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
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.
Import the formalization of Shelah, "Primitive recursive bounds for van der Waerden numbers" (J. Amer. Math. Soc. 1 (1988)), from$\mathrm{shelahBound}(k, r) < A(5, 2k + r)$ for the Ackermann function $A$ . I have also a Palomar submission for it.
gdahia/ShelahHalesJewettat 8a91fc0: the Hales–Jewett theorem with Shelah's bound, via a subspace on which a coloring is insensitive to two letters, and the boundOn top of it, update the density Hales–Jewett project to$n \ge A(4k, k + \lceil 1/\delta \rceil)$ and Szemerédi's and Varnavides' theorems for $n \ge A(4k + 1, k + \lceil 1/\delta \rceil)$ , with thresholds built on Shelah's bound through the finite-unions and Graham–Rothschild theorems.
gdahia/DensityHalesJewettat 478533c, which states the density Hales–Jewett theorem forThe Shelah library moves under
LeanPool.ShelahHalesJewettwith its imports rewritten, and its PalomarSolutionmodule is left out, since it only restates a library theorem. The density project keeps its Lean Pool layout,pullbackdefined fromparameterPreimage, andSolutionwith the asymptotic formsexists_of_density_atTopandexists_of_density_nat_atTop, now derived from the Ackermann thresholds. ItscomposeLineis an alias of the Shelah project'sCombinatorics.Subspace.compLine.🤖 Generated with Claude Code