Repository navigation
Import Fox–Lovász arithmetic triangle removal in vector spaces - #779
Merged
Vilin97 merged 1 commit intoNov 8, 2026
Merged
Conversation
Import the formalization of Fox and Lovász, "A tight bound for Green's arithmetic triangle removal lemma in vector spaces" (arXiv:1606.01230), from gdahia/ArithmeticTriangleRemovalInVectorSpaces at 3bddc92: the removal lemma in F_p^n with exponent C_p, the Kleinberg–Sawin–Speyer bound, the count of triangles spanned by vertex-disjoint triangles, and the tightness of C_p via Pebody's coupling and the KSS construction. The library moves under LeanPool.ArithmeticTriangleRemovalInVectorSpaces with its imports rewritten. The Palomar Challenge and Solution modules are left out, since Solution only restates the library theorems. 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. [Low impact] The PR adds a self-contained formal math library without changing existing application behavior. No blocking code defect was found; making the documented Pebody theorem public would improve reuse. Findings
SummaryImports the arithmetic triangle removal proof, the Kleinberg–Sawin–Speyer bound, and the construction showing the exponent is tight.
Reviews (1) · Last reviewed commit: "Import Fox–Lovász arithmetic triangle re..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
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: 3,712,044 maxHeartbeats units across 29 valid files (5,529 added LOC). Sum of Count-heartbeats wall-clock total: 400.81 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.ArithmeticTriangleRemovalInVectorSpaces.Coupling.Peeling |
10.00 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Construction.LowerBound |
10.00 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Construction.Family |
9.20 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.MulticoloredSumFree.Exponent |
8.80 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.DisjointTriangles.Sampling |
8.40 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Construction.TypeClass |
8.20 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Construction.Hash |
7.90 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.MulticoloredSumFree.SliceRank |
7.90 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Construction.Behrend |
7.00 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Coupling.Decomposition |
6.60 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Coupling.Uniform |
6.30 s |
LeanPool.ArithmeticTriangleRemovalInVectorSpaces.Tightness.Exponent |
6.20 s |
Per-file `lean --profile` output
LeanPool/ArithmeticTriangleRemovalInVectorSpaces.lean
import took 2.1s
cumulative profiling times:
declTypeLinter 1.08ms
elaboration 0.199ms
import 2.1s
initialization 31ms
interpretation 173ms
linting 1ms
module linting 0.0112ms
parsing 0.0481ms
tacticAnalysis 0.52ms
real 3.03
user 1.11
sys 1.09
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Construction/Behrend.lean
import took 1.35s
cumulative profiling times:
attribute application 0.0153ms
congr simp thm 2.02ms
declTypeLinter 1.49ms
elaboration 6.27ms
fix level params 0.152ms
grind 42.2ms
grind ac 0.00366ms
grind cutsat 1.35ms
grind ematch 4.06ms
grind linarith 0.00226ms
grind mark subsingleton 3.25ms
grind ring 0.148ms
grind simp 22.3ms
import 1.35s
initialization 36.9ms
instantiate metavars 0.628ms
interpretation 267ms
let-to-have transformation 0.0239ms
linting 3.46ms
module linting 0.0112ms
norm_num 1.17ms
parsing 2.49ms
process pre-definitions 0.996ms
share common exprs 0.971ms
simp 4.73ms
sym canon 5.76ms
sym typeclass inference 77.3ms
tactic execution 58ms
tacticAnalysis 1.48ms
type checking 70.4ms
typeclass inference 215ms
real 2.84
user 1.78
sys 1.01
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Construction/Family.lean
import took 1.05s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 433ms
interpretation of Mathlib.Tactic.GRewrite.evalGRewriteSeq._boxed took 180ms
cumulative profiling times:
attribute application 3.02ms
compilation (IR) 0.15ms
compilation (LCNF base) 0.897ms
compilation (LCNF impure) 0.762ms
compilation (LCNF mono) 1.32ms
congr simp thm 12.1ms
declTypeLinter 6.21ms
elaboration 103ms
fix level params 1.52ms
grind 148ms
grind cutsat 1.76ms
grind mark subsingleton 15.1ms
grind ring 0.191ms
grind simp 72.9ms
import 1.05s
initialization 38.9ms
instantiate metavars 4.52ms
interpretation 1.42s
let-to-have transformation 0.279ms
linting 53.3ms
module linting 0.0144ms
norm_num 125ms
parsing 25.3ms
process pre-definitions 12.9ms
ring 38.6ms
share common exprs 17.6ms
simp 329ms
sym canon 26.8ms
sym typeclass inference 193ms
tactic execution 528ms
tacticAnalysis 7.16ms
type checking 161ms
typeclass inference 2s
real 4.73
user 6.23
sys 0.95
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Construction/Hash.lean
import took 861ms
simp took 161ms
simp took 107ms
simp took 127ms
tactic execution of Lean.Parser.Tactic.congr took 127ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 176ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 193ms
cumulative profiling times:
attribute application 3.21ms
compilation (IR) 0.786ms
compilation (LCNF base) 20.5ms
compilation (LCNF impure) 3.81ms
compilation (LCNF mono) 8.86ms
congr simp thm 21.9ms
declTypeLinter 23ms
elaboration 488ms
fix level params 5.86ms
grind 296ms
grind ac 0.0329ms
grind cutsat 4.98ms
grind ematch 13.6ms
grind linarith 0.0201ms
grind mark subsingleton 22.9ms
grind ring 0.331ms
grind simp 169ms
import 861ms
initialization 40.7ms
instantiate metavars 20.8ms
interpretation 1.2s
let-to-have transformation 1.03ms
linting 136ms
module linting 0.0119ms
norm_num 7.39ms
parsing 51.2ms
process pre-definitions 43ms
ring 111ms
share common exprs 46.2ms
simp 989ms
sym canon 41.3ms
sym typeclass inference 246ms
tactic execution 756ms
tacticAnalysis 18.9ms
type checking 364ms
typeclass inference 1.22s
real 3.60
user 7.09
sys 0.90
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Construction/LowerBound.lean
import took 1.09s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 139ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 141ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 125ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 644ms
typeclass inference of Nonempty took 116ms
simp took 134ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.11s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 2.13s
tactic execution of Lean.Parser.Tactic.exact took 360ms
interpretation of Mathlib.Tactic.GRewrite.evalGRewriteSeq._boxed took 101ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 115ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 293ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 465ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 120ms
interpretation of Mathlib.Tactic.GRewrite.evalGRewriteSeq._boxed took 134ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 176ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 509ms
cumulative profiling times:
attribute application 0.383ms
congr simp thm 31.6ms
declTypeLinter 15.6ms
elaboration 348ms
fix level params 8.07ms
grind 449ms
grind ac 0.00829ms
grind cutsat 2.21ms
grind ematch 4.2ms
grind linarith 0.00525ms
grind mark subsingleton 46.1ms
grind ring 0.34ms
grind simp 241ms
import 1.09s
initialization 33.6ms
instantiate metavars 36.5ms
interpretation 9.34s
let-to-have transformation 0.779ms
linting 161ms
module linting 0.013ms
norm_num 934ms
parsing 56.4ms
process pre-definitions 101ms
ring 494ms
share common exprs 188ms
simp 687ms
sym canon 64.5ms
sym typeclass inference 295ms
tactic execution 1.6s
tacticAnalysis 14.6ms
type checking 497ms
typeclass inference 5.59s
real 8.40
user 22.05
sys 1.05
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Construction/TypeClass.lean
import took 1.48s
cumulative profiling times:
attribute application 0.474ms
compilation (IR) 0.355ms
compilation (LCNF base) 9.53ms
compilation (LCNF impure) 1.79ms
compilation (LCNF mono) 5.66ms
congr simp thm 10ms
declTypeLinter 7.34ms
elaboration 115ms
fix level params 1.76ms
grind 30.1ms
grind ac 0.0029ms
grind cutsat 0.0518ms
grind ematch 0.353ms
grind linarith 0.00183ms
grind mark subsingleton 0.964ms
grind ring 0.0115ms
grind simp 9.75ms
import 1.48s
initialization 32.4ms
instantiate metavars 5.68ms
interpretation 741ms
let-to-have transformation 0.357ms
linting 58.4ms
module linting 0.0146ms
norm_num 98.6ms
parsing 19.1ms
process pre-definitions 18.3ms
ring 88.1ms
share common exprs 29.3ms
simp 327ms
sym canon 4.03ms
sym typeclass inference 75.4ms
tactic execution 222ms
tacticAnalysis 8.23ms
type checking 122ms
typeclass inference 1.13s
real 3.31
user 4.21
sys 1.08
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Coupling/Basic.lean
import took 1.06s
cumulative profiling times:
attribute application 0.735ms
compilation (IR) 0.435ms
compilation (LCNF base) 4.77ms
compilation (LCNF impure) 1.84ms
compilation (LCNF mono) 3.26ms
congr simp thm 6.8ms
declTypeLinter 8.7ms
elaboration 101ms
fix level params 0.939ms
grind 147ms
grind ac 0.0318ms
grind cutsat 2.27ms
grind ematch 7.85ms
grind linarith 0.145ms
grind mark subsingleton 8.34ms
grind ring 0.417ms
grind simp 67.1ms
import 1.06s
initialization 33ms
instantiate metavars 5.12ms
interpretation 354ms
let-to-have transformation 0.197ms
linting 52.8ms
module linting 0.0182ms
parsing 16ms
process pre-definitions 10.4ms
share common exprs 7.12ms
simp 441ms
sym canon 16.8ms
sym typeclass inference 374ms
tactic execution 204ms
tacticAnalysis 9.06ms
type checking 224ms
typeclass inference 162ms
real 2.93
user 3.18
sys 0.98
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Coupling/Decomposition.lean
import took 1.01s
sym typeclass inference of Lean.Grind.IsCharP took 126ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 622ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 592ms
cumulative profiling times:
attribute application 0.287ms
congr simp thm 18.4ms
declTypeLinter 12.3ms
elaboration 160ms
fix level params 2.28ms
grind 341ms
grind ac 0.123ms
grind cutsat 1.19ms
grind ematch 7.52ms
grind linarith 0.18ms
grind mark subsingleton 30.2ms
grind ring 1.34ms
grind simp 201ms
import 1.01s
initialization 32.9ms
instantiate metavars 10.1ms
interpretation 1.91s
let-to-have transformation 0.371ms
linting 66.4ms
module linting 0.0129ms
norm_num 11.2ms
parsing 30.2ms
process pre-definitions 21.7ms
ring 89.1ms
share common exprs 28.2ms
simp 350ms
sym canon 57.6ms
sym typeclass inference 1.05s
tactic execution 523ms
tacticAnalysis 12.4ms
type checking 312ms
typeclass inference 995ms
real 4.76
user 7.12
sys 0.95
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Coupling/Decreasing.lean
import took 1.02s
cumulative profiling times:
attribute application 0.153ms
blocked (unaccounted) 0.423ms
congr simp thm 5.93ms
declTypeLinter 6.45ms
elaboration 69.2ms
fix level params 1.73ms
grind 19.8ms
grind ac 0.00792ms
grind cutsat 0.322ms
grind ematch 5.27ms
grind linarith 0.124ms
grind mark subsingleton 2.86ms
grind ring 0.0942ms
grind simp 5.37ms
import 1.02s
initialization 33.1ms
instantiate metavars 4.35ms
interpretation 871ms
let-to-have transformation 0.21ms
linting 24.7ms
module linting 0.0122ms
norm_num 229ms
parsing 11.9ms
process pre-definitions 19.9ms
ring 107ms
share common exprs 27.9ms
simp 103ms
sym canon 3.69ms
sym typeclass inference 40.9ms
tactic execution 164ms
tacticAnalysis 6.6ms
type checking 131ms
typeclass inference 455ms
real 2.62
user 3.13
sys 0.99
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Coupling/Peeling.lean
import took 1.02s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 475ms
type checking took 140ms
grind took 335ms
type checking took 516ms
sym typeclass inference of Lean.Grind.IsCharP took 142ms
sym typeclass inference of Lean.Grind.IsCharP took 125ms
sym typeclass inference of Lean.Grind.IsCharP took 118ms
cumulative profiling times:
attribute application 0.396ms
blocked (unaccounted) 0.691ms
compilation (IR) 0.327ms
compilation (LCNF base) 9.11ms
compilation (LCNF impure) 1.63ms
compilation (LCNF mono) 2.82ms
congr simp thm 15.1ms
declTypeLinter 15.7ms
elaboration 150ms
fix level params 2.45ms
grind 866ms
grind ac 2.83ms
grind cutsat 9.76ms
grind ematch 371ms
grind linarith 41.6ms
grind mark subsingleton 110ms
grind ring 22.1ms
grind simp 359ms
import 1.02s
initialization 33ms
instantiate metavars 14.9ms
interpretation 1.12s
let-to-have transformation 0.475ms
linting 68.5ms
module linting 0.00987ms
norm_num 15.1ms
parsing 31.7ms
process pre-definitions 23.5ms
ring 116ms
share common exprs 31.1ms
simp 497ms
sym canon 80.7ms
sym typeclass inference 1.73s
tactic execution 492ms
tacticAnalysis 14.9ms
type checking 1.13s
typeclass inference 779ms
real 4.52
user 8.97
sys 1.00
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Coupling/Uniform.lean
import took 1.04s
type checking took 124ms
type checking took 154ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 172ms
sym typeclass inference of Lean.Grind.IsCharP took 128ms
sym typeclass inference of Lean.Grind.IsCharP took 129ms
cumulative profiling times:
attribute application 0.339ms
blocked (unaccounted) 2.75s
congr simp thm 30.4ms
declTypeLinter 14.2ms
elaboration 154ms
fix level params 2.87ms
grind 429ms
grind ac 0.0577ms
grind cutsat 2.64ms
grind ematch 32.2ms
grind linarith 2.31ms
grind mark subsingleton 69.3ms
grind ring 23.4ms
grind simp 189ms
import 1.04s
initialization 30.9ms
instantiate metavars 11ms
interpretation 1.43s
let-to-have transformation 0.449ms
linting 70.8ms
module linting 0.014ms
norm_num 81.2ms
parsing 30.4ms
process pre-definitions 28.4ms
ring 205ms
share common exprs 50.3ms
simp 658ms
sym canon 66.9ms
sym typeclass inference 1.78s
tactic execution 451ms
tacticAnalysis 13.1ms
type checking 639ms
typeclass inference 1.12s
real 4.67
user 8.31
sys 0.99
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/DisjointTriangles/Embedding.lean
import took 1.02s
cumulative profiling times:
attribute application 0.1ms
compilation (IR) 0.0594ms
compilation (LCNF base) 0.4ms
compilation (LCNF impure) 0.274ms
compilation (LCNF mono) 0.381ms
congr simp thm 3.45ms
declTypeLinter 10.6ms
elaboration 92.7ms
fix level params 4.1ms
grind 12ms
grind mark subsingleton 0.547ms
grind ring 1.84ms
grind simp 8.89ms
import 1.02s
initialization 32.6ms
instantiate metavars 5.54ms
interpretation 299ms
let-to-have transformation 0.31ms
linting 29.6ms
module linting 0.013ms
norm_num 0.586ms
parsing 12.8ms
process pre-definitions 12.3ms
ring 3.33ms
share common exprs 11ms
simp 221ms
sym canon 6.11ms
sym typeclass inference 170ms
tactic execution 184ms
tacticAnalysis 4.59ms
type checking 73.1ms
typeclass inference 401ms
real 2.40
user 2.41
sys 0.95
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/DisjointTriangles/MaximalFamily.lean
import took 1.05s
typeclass inference of Nonempty took 128ms
simp took 321ms
simp took 310ms
simp took 259ms
simp took 222ms
simp took 211ms
simp took 215ms
simp took 224ms
simp took 215ms
simp took 211ms
simp took 221ms
simp took 210ms
simp took 210ms
simp took 847ms
cumulative profiling times:
attribute application 0.0901ms
congr simp thm 31.6ms
declTypeLinter 7.42ms
elaboration 80.9ms
fix level params 2.11ms
grind 13.5ms
grind mark subsingleton 0.788ms
grind simp 3.68ms
import 1.05s
initialization 36.1ms
instantiate metavars 2.43ms
interpretation 502ms
let-to-have transformation 0.158ms
linting 20.9ms
module linting 0.013ms
norm_num 55.2ms
parsing 10.1ms
process pre-definitions 11.3ms
ring 28.2ms
share common exprs 9.6ms
simp 4.28s
sym canon 3.21ms
sym typeclass inference 91.6ms
tactic execution 209ms
tacticAnalysis 4.71ms
type checking 44.4ms
typeclass inference 1.9s
real 5.56
user 8.19
sys 0.98
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/DisjointTriangles/Pruning.lean
import took 1.06s
cumulative profiling times:
attribute application 0.215ms
compilation (IR) 0.0617ms
compilation (LCNF base) 0.639ms
compilation (LCNF impure) 0.38ms
compilation (LCNF mono) 0.597ms
congr simp thm 26.7ms
declTypeLinter 14.8ms
elaboration 190ms
fix level params 4.5ms
grind 44.8ms
grind ac 0.00782ms
grind cutsat 0.0749ms
grind ematch 5.75ms
grind linarith 0.17ms
grind mark subsingleton 8.28ms
grind ring 0.666ms
grind simp 21ms
import 1.06s
initialization 39.2ms
instantiate metavars 7.47ms
interpretation 1.28s
let-to-have transformation 0.484ms
linting 54.2ms
module linting 0.0135ms
norm_num 59.2ms
parsing 30.8ms
process pre-definitions 23.8ms
ring 62.2ms
share common exprs 26.1ms
simp 674ms
sym canon 16.6ms
sym typeclass inference 70ms
tactic execution 490ms
tacticAnalysis 9.78ms
type checking 169ms
typeclass inference 1.24s
real 3.66
user 5.37
sys 1.00
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/DisjointTriangles/Sampling.lean
import took 1.09s
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 116ms
simp took 138ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 133ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 135ms
simp took 200ms
interpretation of Mathlib.Tactic.Tauto._aux_Mathlib_Tactic_Tauto___elabRules_Mathlib_Tactic_Tauto_tauto_1._boxed took 117ms
interpretation of Mathlib.Tactic.GRewrite.evalGRewriteSeq._boxed took 149ms
simp took 104ms
tactic execution of Mathlib.Tactic.GRewrite.grewriteSeq took 103ms
interpretation of Mathlib.Tactic.GRewrite.evalGRewriteSeq._boxed took 107ms
cumulative profiling times:
attribute application 1.91ms
compilation (IR) 0.339ms
compilation (LCNF base) 3.6ms
compilation (LCNF impure) 1.71ms
compilation (LCNF mono) 3.62ms
congr simp thm 41.6ms
declTypeLinter 34.1ms
elaboration 625ms
fix level params 13.4ms
grind 36.7ms
grind ac 0.485ms
grind cutsat 0.00815ms
grind linarith 0.0633ms
grind mark subsingleton 2.44ms
grind ring 0.00271ms
grind simp 17ms
import 1.09s
initialization 38.6ms
instantiate metavars 16.1ms
interpretation 2.75s
let-to-have transformation 1.31ms
linting 133ms
module linting 0.0145ms
norm_num 191ms
parsing 60.8ms
process pre-definitions 55.5ms
ring 105ms
share common exprs 58.3ms
simp 2.82s
sym canon 4.48ms
sym typeclass inference 83.7ms
tactic execution 1.79s
tacticAnalysis 18.7ms
type checking 339ms
typeclass inference 5.5s
real 6.46
user 15.56
sys 1.01
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/DisjointTriangles/TensorPower.lean
import took 1s
cumulative profiling times:
attribute application 0.058ms
congr simp thm 3.71ms
declTypeLinter 6.92ms
elaboration 55.1ms
fix level params 1.31ms
grind 24ms
grind ac 0.00489ms
grind cutsat 0.048ms
grind ematch 2.74ms
grind linarith 0.113ms
grind mark subsingleton 3.18ms
grind ring 0.351ms
grind simp 9.69ms
import 1s
initialization 33.2ms
instantiate metavars 1.96ms
interpretation 466ms
let-to-have transformation 0.124ms
linting 17ms
module linting 0.0135ms
norm_num 56.3ms
parsing 7.91ms
process pre-definitions 6.07ms
ring 23.8ms
share common exprs 9.15ms
simp 26.8ms
sym canon 8.19ms
sym typeclass inference 43.2ms
tactic execution 125ms
tacticAnalysis 4ms
type checking 71.6ms
typeclass inference 344ms
real 2.47
user 2.15
sys 0.95
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Imports.lean
import took 1.03s
cumulative profiling times:
declTypeLinter 0.12ms
elaboration 0.145ms
import 1.03s
initialization 37.3ms
interpretation 158ms
linting 0.272ms
module linting 0.0125ms
parsing 0.00155ms
tacticAnalysis 0.136ms
real 1.95
user 1.06
sys 0.93
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/LinearMap/Card.lean
import took 819ms
cumulative profiling times:
attribute application 0.381ms
congr simp thm 3.51ms
declTypeLinter 9.03ms
elaboration 23.2ms
fix level params 1.01ms
import 819ms
initialization 40.1ms
instantiate metavars 0.693ms
interpretation 207ms
let-to-have transformation 0.0912ms
linting 6.77ms
module linting 0.0139ms
parsing 3.12ms
process pre-definitions 2.64ms
share common exprs 2.06ms
simp 71.1ms
tactic execution 34.3ms
tacticAnalysis 3.03ms
type checking 26.3ms
typeclass inference 233ms
real 1.99
user 1.37
sys 0.87
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/MulticoloredSumFree/Basic.lean
import took 406ms
cumulative profiling times:
attribute application 0.0348ms
congr simp thm 0.479ms
declTypeLinter 7.12ms
elaboration 11.9ms
fix level params 0.297ms
grind 0.766ms
grind mark subsingleton 0.0186ms
grind simp 1.76ms
import 406ms
initialization 36.1ms
instantiate metavars 0.312ms
interpretation 89.3ms
let-to-have transformation 0.0369ms
linting 4.93ms
module linting 0.0133ms
parsing 2.45ms
process pre-definitions 1.35ms
share common exprs 0.633ms
simp 9.18ms
sym canon 0.0707ms
sym typeclass inference 0.0651ms
tactic execution 17.1ms
tacticAnalysis 1.79ms
type checking 4.29ms
typeclass inference 14.1ms
real 1.22
user 0.65
sys 0.67
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/MulticoloredSumFree/Exponent.lean
import took 1.1s
interpretation of Mathlib.Meta.Positivity.evalMul._lam_3._boxed took 131ms
cumulative profiling times:
attribute application 0.134ms
congr simp thm 6.08ms
declTypeLinter 4.47ms
elaboration 57.6ms
fix level params 1.39ms
grind 49.5ms
grind ac 0.00211ms
grind cutsat 0.562ms
grind ematch 0.488ms
grind linarith 0.00108ms
grind mark subsingleton 4.28ms
grind ring 0.061ms
grind simp 21.1ms
import 1.1s
initialization 32ms
instantiate metavars 2.74ms
interpretation 964ms
let-to-have transformation 0.21ms
linting 23.9ms
module linting 0.0126ms
norm_num 287ms
parsing 13.8ms
process pre-definitions 18.4ms
ring 57.2ms
share common exprs 15.5ms
simp 178ms
sym canon 11.3ms
sym typeclass inference 146ms
tactic execution 220ms
tacticAnalysis 6.6ms
type checking 111ms
typeclass inference 658ms
real 3.02
user 3.73
sys 0.98
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/MulticoloredSumFree/Monomials.lean
import took 1.02s
cumulative profiling times:
attribute application 0.0177ms
compilation (IR) 0.407ms
compilation (LCNF base) 3.71ms
compilation (LCNF impure) 1.68ms
compilation (LCNF mono) 2.72ms
congr simp thm 1.83ms
declTypeLinter 1.79ms
elaboration 7.27ms
fix level params 0.319ms
import 1.02s
initialization 32.8ms
instantiate metavars 0.0283ms
interpretation 247ms
let-to-have transformation 0.031ms
linting 5.59ms
module linting 0.0106ms
norm_num 14.1ms
parsing 2.75ms
process pre-definitions 2.93ms
ring 5.57ms
share common exprs 2.5ms
simp 27.3ms
tactic execution 94ms
tacticAnalysis 3.95ms
type checking 15.2ms
typeclass inference 99.2ms
real 2.28
user 1.43
sys 0.92
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/MulticoloredSumFree/Product.lean
import took 685ms
cumulative profiling times:
attribute application 0.139ms
congr simp thm 6.81ms
declTypeLinter 13ms
elaboration 63.8ms
fix level params 4.65ms
grind 20.2ms
grind ac 0.00262ms
grind cutsat 1.62ms
grind ematch 2.42ms
grind linarith 0.00213ms
grind mark subsingleton 2.32ms
grind ring 0.903ms
grind simp 25.5ms
import 685ms
initialization 31.8ms
instantiate metavars 6.43ms
interpretation 504ms
let-to-have transformation 0.154ms
linting 30.5ms
module linting 0.0147ms
norm_num 4.65ms
parsing 16.6ms
process pre-definitions 13ms
share common exprs 9.54ms
simp 244ms
sym canon 2.84ms
sym typeclass inference 11.5ms
tactic execution 207ms
tacticAnalysis 5.81ms
type checking 96.4ms
typeclass inference 529ms
real 2.14
user 2.45
sys 0.81
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/MulticoloredSumFree/SliceRank.lean
import took 1.1s
simp took 1.74s
cumulative profiling times:
attribute application 0.0872ms
congr simp thm 16.1ms
declTypeLinter 8.31ms
elaboration 75.2ms
fix level params 1.16ms
grind 112ms
grind ac 0.0113ms
grind cutsat 2.34ms
grind ematch 10.6ms
grind linarith 0.00645ms
grind mark subsingleton 18.5ms
grind ring 0.186ms
grind simp 66.1ms
import 1.1s
initialization 38.1ms
instantiate metavars 4.58ms
interpretation 386ms
let-to-have transformation 0.285ms
linting 27ms
module linting 0.0124ms
parsing 14.6ms
process pre-definitions 7.19ms
share common exprs 7.64ms
simp 1.97s
sym canon 34.4ms
sym typeclass inference 706ms
tactic execution 192ms
tacticAnalysis 6.34ms
type checking 110ms
typeclass inference 992ms
real 4.60
user 5.68
sys 1.00
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/MulticoloredSumFree/SmallPrimes.lean
import took 1.05s
cumulative profiling times:
attribute application 0.0695ms
congr simp thm 1.73ms
declTypeLinter 3.88ms
elaboration 48.2ms
fix level params 1.58ms
grind 22.2ms
grind mark subsingleton 1.9ms
grind simp 6.32ms
import 1.05s
initialization 32ms
instantiate metavars 2.25ms
interpretation 884ms
let-to-have transformation 0.163ms
linting 21.4ms
module linting 0.0129ms
norm_num 550ms
parsing 9.25ms
process pre-definitions 13.4ms
ring 70.4ms
share common exprs 26.1ms
simp 10.5ms
sym canon 3.36ms
sym typeclass inference 28.2ms
tactic execution 135ms
tacticAnalysis 3.7ms
type checking 108ms
typeclass inference 494ms
real 2.84
user 3.26
sys 0.95
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/MulticoloredSumFree/TensorPower.lean
import took 1.05s
cumulative profiling times:
attribute application 0.0491ms
congr simp thm 2.44ms
declTypeLinter 6.5ms
elaboration 24.8ms
fix level params 0.754ms
import 1.05s
initialization 41.4ms
instantiate metavars 0.89ms
interpretation 349ms
let-to-have transformation 0.0814ms
linting 9.79ms
module linting 0.0132ms
norm_num 61.2ms
parsing 4.34ms
process pre-definitions 4.89ms
ring 18ms
share common exprs 5.6ms
simp 43.8ms
tactic execution 102ms
tacticAnalysis 2.7ms
type checking 41ms
typeclass inference 474ms
real 2.45
user 2.01
sys 0.96
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/SliceRank/Diagonal.lean
import took 955ms
simp took 152ms
sym typeclass inference of Lean.Grind.NoNatZeroDivisors took 117ms
sym typeclass inference of Lean.Grind.NoNatZeroDivisors took 112ms
cumulative profiling times:
attribute application 0.061ms
congr simp thm 11ms
declTypeLinter 7.27ms
elaboration 43.3ms
fix level params 2.54ms
grind 53ms
grind ac 0.00615ms
grind cutsat 1.26ms
grind ematch 3.36ms
grind linarith 0.00408ms
grind mark subsingleton 12ms
grind ring 0.0211ms
grind simp 43.8ms
import 955ms
initialization 38.9ms
instantiate metavars 3.08ms
interpretation 283ms
let-to-have transformation 0.145ms
linting 15.6ms
module linting 0.0128ms
norm_num 0.209ms
parsing 9.88ms
process pre-definitions 5.92ms
ring 4.72ms
share common exprs 5.8ms
simp 717ms
sym canon 41.1ms
sym typeclass inference 445ms
tactic execution 313ms
tacticAnalysis 4.04ms
type checking 74.9ms
typeclass inference 819ms
real 3.15
user 3.69
sys 0.94
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Tightness/Exponent.lean
import took 1.02s
tactic execution of Mathlib.Tactic.nlinarith took 233ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 101ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 152ms
cumulative profiling times:
attribute application 0.121ms
congr simp thm 2.05ms
declTypeLinter 5.61ms
elaboration 57ms
fix level params 1.85ms
import 1.02s
initialization 31.6ms
instantiate metavars 2.5ms
interpretation 1.08s
let-to-have transformation 0.222ms
linting 35.4ms
module linting 0.0127ms
norm_num 181ms
parsing 13ms
process pre-definitions 18.8ms
ring 87.7ms
share common exprs 25ms
simp 13.6ms
tactic execution 698ms
tacticAnalysis 6.07ms
type checking 137ms
typeclass inference 1.27s
real 3.30
user 4.44
sys 0.96
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Triangle/Basic.lean
import took 658ms
simp took 101ms
cumulative profiling times:
attribute application 1.05ms
compilation (IR) 0.108ms
compilation (LCNF base) 2.81ms
compilation (LCNF impure) 0.645ms
compilation (LCNF mono) 1.56ms
congr simp thm 4.6ms
declTypeLinter 9.81ms
elaboration 64.2ms
fix level params 1.52ms
grind 75.3ms
grind ac 0.175ms
grind cutsat 0.0164ms
grind ematch 0.824ms
grind linarith 0.152ms
grind mark subsingleton 9.48ms
grind ring 0.0187ms
grind simp 40.6ms
import 658ms
initialization 32.5ms
instantiate metavars 1.92ms
interpretation 200ms
let-to-have transformation 0.156ms
linting 13.4ms
module linting 0.013ms
parsing 8.67ms
process pre-definitions 5.06ms
share common exprs 3.56ms
simp 175ms
sym canon 8.2ms
sym typeclass inference 107ms
tactic execution 77ms
tacticAnalysis 5.5ms
type checking 57ms
typeclass inference 102ms
real 1.79
user 1.58
sys 0.79
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/ZMod.lean
import took 1.05s
cumulative profiling times:
attribute application 0.116ms
congr simp thm 4.8ms
declTypeLinter 8.59ms
elaboration 138ms
fix level params 1.88ms
grind 65.8ms
grind mark subsingleton 4.5ms
grind simp 39.5ms
import 1.05s
initialization 35ms
instantiate metavars 2.81ms
interpretation 612ms
let-to-have transformation 0.468ms
linting 33ms
module linting 0.0125ms
norm_num 67.5ms
parsing 15.3ms
process pre-definitions 14ms
ring 37.1ms
share common exprs 13.7ms
simp 51ms
sym canon 9.41ms
sym typeclass inference 34.7ms
tactic execution 216ms
tacticAnalysis 6.81ms
type checking 87.4ms
typeclass inference 710ms
real 2.98
user 3.09
sys 0.93
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Vilin97
approved these changes
Nov 8, 2026
Vilin97
left a comment
Vilin97
left a comment
Collaborator
There was a problem hiding this comment.
Source review of 7aeacb2323354535ec03bc7cf622fbee8abfbc24: approve.
This is a significant, completed formalization of the Fox–Lovász polynomial arithmetic triangle removal bound and its sharp exponent. The four public statements in ZMod.lean match the card and the paper’s Theorems 1–3: the multicolored sum-free bound, the count of triangles spanned by vertex-disjoint triples, removal within the total εN deletion budget, and the all-dimension obstruction δ ≤ ε^(C_p − η) below an explicit positive threshold. The prime-field hypotheses, strict triangle-count premise, quantifiers, and constants are preserved.
The detailed review covered all 27 mathematical modules. In particular, the lower construction supplies actual families through the geometric coupling, type classes, Behrend sets and hashing; it does not assume the hard combinatorial step. The upper proof supplies the sampling, pruning, embedding and tensor amplification arguments. The exponent positivity and zero/empty boundary cases are handled. The 29-module import graph is acyclic, and all four advertised endpoints are public through the registered entry module.
All 27 mathematical files match the pinned upstream after reversing the import-prefix change. Apache-2.0 attribution and the card’s AI provenance agree with that source. Bounded comparisons with current Mathlib, Tau Ceti and the pool found related supporting results, but no duplicate of these sharp endpoints.
The general compatible_of_isDecreasingOn theorem being private is a nonblocking API improvement: the theorem is proved internally, its geometric specialization is public, and the card’s four public endpoints are available. Exporting the general theorem with its public prerequisite imports would be a useful follow-up, rather than a prerequisite for this import.
This approval records source acceptance at this exact head. Applicable hosted checks and normal protected integration remain independent; I have not run a local compiler build.
Collaborator
|
/review |
Collaborator
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All four headline results match the card, with the coupling and extremal constructions proved internally. |
| Novelty | ✅ pass |
No duplicate was identified for the four headlines; broader coverage remains unverifiable given the unavailable semantic Mathlib searches and bounded Tau Ceti evidence. |
| Significance | ✅ pass |
The quantitative triangle removal theorem and asymptotic optimality result form a completed research-level project with substantial supporting theory. |
| Sources | ✅ pass |
Fox–Lovász Theorems 1–3 support the headline results, and the upstream Lean development is credited; auxiliary citation numbers need correction. |
| Code quality (advisory) | ✅ pass |
Focused helper lemmas, shared counting arguments, and reuse of IsMulticoloredSumFree.map and IsMulticoloredSumFree.pi keep the development maintainable; no material quality concerns found. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The optimality theorem assumes that the same ε and δ satisfy the removal property in every dimension, as disclosed in the card; the other headlines use their stated primality and configuration hypotheses. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | additive combinatorics |
| Mode | theory_building |
| Code quality | 4 / 5 |
Statement check: The Lean proves the stated removal, sum-free-family, triangle-count, and exponent-optimality bounds in every dimension, with the specified constants and explicit positive threshold.
Formalizes the Fox–Lovász arithmetic triangle removal theorem and optimality of its exponent through slice-rank bounds, triangle counting, couplings, and extremal constructions.
Sources findings (1)
- incorrect-source-locators —
LeanPool/ArithmeticTriangleRemovalInVectorSpaces/Coupling/Uniform.lean:237
Several incorrect locators obstruct tracing the Lean arguments to their sources. In published Pebody, the mixture result is Corollary 10; Decomposition's cited Lemma 2.1 corresponds to Lemma 5, and Peeling's Lemma 3.1 and Corollary 3.2 correspond to Lemma 7 and Corollary 8. In published Kleinberg–Sawin–Speyer, TypeClass's entropy estimate is Lemma 3, Hash's sum-free construction is Lemma 9, and its averaging estimate occurs in Lemma 12, rather than the cited 3.1, 4.3, and 4.6. Correct all repeated locators or identify an edition using those numbers. The underlying results are supported, so this is nonblocking.
Evidence: The diff introducesprivate lemma compatible_lastcase {i j r : ℕ} (hij : DecreasingCompatible (i + j))with: “Corollary 5.2 of Pebody. Fori > 0, the distributionsunif i,unif Nand the mixture
ofunif jandunif Nwith mean(N - i) / 2are compatible, whereN = i + j + r + 1.” The other repeated citations include “Lemma 2.1 of Pebody, after applyinghat.”, “Lemma 3.1 of Pebody.”, “Corollary 3.2 of Pebody.”, “Lemma 4.3 of Kleinberg, Sawin and Speyer.”, and “Lemma 4.6 of Kleinberg, Sawin and Speyer.”.
Tokens: 11,765,699 in / 35,292 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $47.5922 (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.
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 Fox and Lovász, "A tight bound for Green's arithmetic triangle removal lemma in vector spaces" (arXiv:1606.01230), from gdahia/ArithmeticTriangleRemovalInVectorSpaces at 3bddc92: the removal lemma in$\mathbb{F}_p^n$ with exponent $C_p$ , the Kleinberg–Sawin–Speyer bound, the count of triangles spanned by vertex-disjoint triangles, and the tightness of $C_p$ via Pebody's coupling and the KSS construction.
The library moves under
LeanPool.ArithmeticTriangleRemovalInVectorSpaceswith its imports rewritten.