Import Polynomial Freiman–Ruzsa formalization - #386
Open
Vilin97 wants to merge 11 commits into
Open
Conversation
Greptile SummaryThe PR imports the Polynomial Freiman–Ruzsa formalization, exposes six closed Marton results, and registers the project with pinned PFR and AddCombi provenance.
|
| Filename | Overview |
|---|---|
| LeanPool/PFR.lean | Defines the stable PFR project entry point and records the formalization’s source, scope, and contributors. |
| LeanPool/PFR/Solution.lean | Bridges the six Palomar statements to imported PFR results while clearly documenting that the upstream challenge module is omitted. |
| LeanPool/projects.yml | Registers the PFR project with pinned PFR and AddCombi sources, licensing, mixed provenance, headline declarations, and corrected contributor attribution. |
| LeanPool.lean | Adds the PFR umbrella and constituent modules to the aggregate LeanPool import surface. |
| LeanPool/PFR/ApproxHomPFR.lean | Adds the approximate-homomorphism consequence and its supporting bridge through the imported PFR development. |
Reviews (11): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger 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: 12,942 maxHeartbeats units across 51 files (16,777 added LOC). Sum of Count-heartbeats wall-clock total: 337.91 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.PFR.RhoFunctional |
43.00 s |
LeanPool.PFR.MoreRuzsaDist |
31.00 s |
LeanPool.PFR.TorsionEndgame |
31.00 s |
LeanPool.PFR.WeakPFR |
24.00 s |
LeanPool.PFR.ImprovedPFR |
19.00 s |
LeanPool.PFR.BoundingMutual |
18.00 s |
LeanPool.PFR.Endgame |
14.00 s |
LeanPool.PFR.ForMathlib.Entropy.RuzsaDist |
13.00 s |
LeanPool.PFR.AddCombi.BSG |
11.00 s |
LeanPool.PFR.Mathlib.LinearAlgebra.Basis.VectorSpace |
9.40 s |
LeanPool.PFR.ForMathlib.ThreeVariables |
8.90 s |
LeanPool.PFR.Kullback |
7.70 s |
Per-file `lean --profile` output
LeanPool/PFR.lean
import took 7.82s
cumulative profiling times:
elaboration 0.147ms
import 7.82s
initialization 44ms
interpretation 182ms
linting 0.321ms
module linting 0.00181ms
overlappingInstancesLinter 0.312ms
parsing 0.0337ms
tacticAnalysis 0.898ms
real 9.30
user 1.17
sys 0.69
LeanPool/PFR/AddCombi/BSG.lean
import took 769ms
simp took 286ms
simp took 2.59s
simp took 169ms
interpretation of Mathlib.Tactic.GRewrite.evalGRewriteSeq._boxed took 130ms
cumulative profiling times:
aesop 32.7ms
attribute application 0.427ms
blocked (unaccounted) 1.37s
congr simp thm 43.8ms
elaboration 541ms
fix level params 15.2ms
grind 195ms
grind ac 0.117ms
grind cutsat 0.253ms
grind ematch 29.1ms
grind linarith 0.679ms
grind mark subsingleton 23.5ms
grind ring 1.23ms
grind simp 102ms
import 769ms
initialization 31.6ms
instantiate metavars 12.7ms
interpretation 3.08s
let-to-have transformation 1.15ms
linting 102ms
module linting 0.00128ms
norm_num 207ms
overlappingInstancesLinter 21ms
parsing 38.5ms
process pre-definitions 51.3ms
ring 101ms
share common exprs 81.4ms
simp 4.71s
sym canon 43.6ms
sym typeclass inference 591ms
tactic execution 749ms
tacticAnalysis 98.3ms
type checking 467ms
typeclass inference 6.09s
real 6.27
user 18.00
sys 0.64
LeanPool/PFR/AddCombi/Convolution/Finite/Defs.lean
import took 723ms
simp took 199ms
cumulative profiling times:
aesop 43.2ms
attribute application 2.77ms
blocked (unaccounted) 157ms
compilation (IR) 1.14ms
compilation (LCNF base) 27.6ms
compilation (LCNF impure) 4.61ms
compilation (LCNF mono) 9.74ms
congr simp thm 21.7ms
elaboration 223ms
fix level params 3.74ms
grind 21.8ms
grind ac 0.0586ms
grind cutsat 0.0108ms
grind ematch 0.646ms
grind linarith 0.0656ms
grind mark subsingleton 0.995ms
grind ring 0.0116ms
grind simp 10.1ms
import 723ms
initialization 37.2ms
instantiate metavars 1.53ms
interpretation 335ms
let-to-have transformation 0.469ms
linting 28.7ms
module linting 0.00163ms
norm_num 0.825ms
overlappingInstancesLinter 25.9ms
parsing 13.3ms
process pre-definitions 13.4ms
share common exprs 9.83ms
simp 725ms
sym canon 4.52ms
sym typeclass inference 151ms
tactic execution 82.9ms
tacticAnalysis 50.8ms
type checking 153ms
typeclass inference 957ms
real 2.61
user 3.64
sys 0.53
LeanPool/PFR/AddCombi/Convolution/Finite/Order.lean
import took 741ms
cumulative profiling times:
attribute application 0.0589ms
congr simp thm 0.743ms
elaboration 93.4ms
fix level params 0.607ms
import 741ms
initialization 31.9ms
instantiate metavars 0.277ms
interpretation 174ms
let-to-have transformation 0.116ms
linting 6.73ms
module linting 0.00168ms
overlappingInstancesLinter 9.07ms
parsing 2.61ms
process pre-definitions 2.4ms
share common exprs 1.73ms
simp 40.5ms
tactic execution 35.2ms
tacticAnalysis 11.1ms
type checking 21.8ms
typeclass inference 387ms
real 1.60
user 1.51
sys 0.51
LeanPool/PFR/AddCombi/Mathlib/Algebra/GroupWithZero/Indicator.lean
import took 377ms
cumulative profiling times:
elaboration 2.44ms
import 377ms
initialization 30.8ms
interpretation 103ms
linting 1.34ms
module linting 0.00211ms
overlappingInstancesLinter 0.893ms
parsing 0.357ms
tacticAnalysis 8.87ms
real 0.95
user 0.59
sys 0.39
LeanPool/PFR/AddCombi/Mathlib/Algebra/Notation/Indicator.lean
import took 347ms
cumulative profiling times:
attribute application 0.725ms
blocked (unaccounted) 65.5ms
compilation (IR) 1.29ms
compilation (LCNF base) 31.7ms
compilation (LCNF impure) 4.88ms
compilation (LCNF mono) 8.91ms
elaboration 1.1ms
fix level params 0.0901ms
import 347ms
initialization 32ms
instantiate metavars 0.0435ms
interpretation 143ms
let-to-have transformation 0.0642ms
linting 2.82ms
module linting 0.00182ms
overlappingInstancesLinter 1.85ms
parsing 1ms
process pre-definitions 2.93ms
share common exprs 0.606ms
tacticAnalysis 7.56ms
type checking 1.77ms
typeclass inference 34.2ms
real 1.08
user 0.76
sys 0.36
LeanPool/PFR/AddCombi/Mathlib/Algebra/Order/GroupWithZero/Indicator.lean
import took 350ms
cumulative profiling times:
attribute application 1.28ms
congr simp thm 0.876ms
elaboration 12.3ms
fix level params 0.424ms
import 350ms
initialization 30.4ms
instantiate metavars 0.0204ms
interpretation 108ms
let-to-have transformation 0.0425ms
linting 2.77ms
module linting 0.00264ms
overlappingInstancesLinter 4.12ms
parsing 1.82ms
process pre-definitions 0.571ms
share common exprs 0.373ms
simp 27.6ms
tactic execution 2.51ms
tacticAnalysis 7.68ms
type checking 4.32ms
typeclass inference 35.3ms
real 0.97
user 0.68
sys 0.36
LeanPool/PFR/AddCombi/Mathlib/Algebra/Order/Ring/NNRat.lean
import took 468ms
cumulative profiling times:
attribute application 0.288ms
congr simp thm 0.212ms
elaboration 4.65ms
fix level params 0.0418ms
import 468ms
initialization 31.8ms
instantiate metavars 0.0177ms
interpretation 118ms
let-to-have transformation 0.0185ms
linting 1.57ms
module linting 0.00185ms
overlappingInstancesLinter 2.66ms
parsing 0.618ms
process pre-definitions 0.295ms
share common exprs 0.146ms
simp 0.424ms
tactic execution 12ms
tacticAnalysis 3.91ms
type checking 2.05ms
typeclass inference 18.8ms
real 1.08
user 0.69
sys 0.41
LeanPool/PFR/AddCombi/Mathlib/Algebra/Star/Pi.lean
import took 441ms
cumulative profiling times:
attribute application 0.499ms
congr simp thm 0.378ms
elaboration 4.61ms
fix level params 0.0521ms
import 441ms
initialization 34.1ms
instantiate metavars 0.0108ms
interpretation 117ms
let-to-have transformation 0.0196ms
linting 1.35ms
module linting 0.002ms
overlappingInstancesLinter 2.63ms
parsing 0.682ms
process pre-definitions 0.191ms
share common exprs 0.132ms
simp 3.66ms
tactic execution 0.59ms
tacticAnalysis 5.5ms
type checking 1.31ms
typeclass inference 6.96ms
real 1.04
user 0.69
sys 0.38
LeanPool/PFR/AddCombi/Mathlib/Combinatorics/Additive/Energy.lean
import took 522ms
cumulative profiling times:
aesop 28.2ms
attribute application 1.96ms
blocked (unaccounted) 171ms
compilation (IR) 1.95ms
compilation (LCNF base) 58.7ms
compilation (LCNF impure) 7.71ms
compilation (LCNF mono) 17.7ms
congr simp thm 8.49ms
elaboration 30.8ms
fix level params 1.45ms
import 522ms
initialization 33.2ms
instantiate metavars 0.788ms
interpretation 343ms
let-to-have transformation 0.186ms
linting 15.6ms
module linting 0.00173ms
overlappingInstancesLinter 9.13ms
parsing 7.71ms
process pre-definitions 9.02ms
share common exprs 4.85ms
simp 313ms
tactic execution 70.6ms
tacticAnalysis 35.3ms
to_additive 57.6ms
type checking 36.1ms
typeclass inference 279ms
real 1.99
user 1.93
sys 0.47
LeanPool/PFR/AddCombi/Mathlib/Data/Finset/Density.lean
import took 487ms
cumulative profiling times:
attribute application 0.943ms
congr simp thm 1.09ms
elaboration 17ms
fix level params 0.232ms
import 487ms
initialization 35.9ms
instantiate metavars 0.0954ms
interpretation 146ms
let-to-have transformation 0.058ms
linting 4.42ms
module linting 0.0016ms
overlappingInstancesLinter 6.94ms
parsing 2.46ms
process pre-definitions 1.15ms
share common exprs 0.756ms
simp 37.5ms
tactic execution 31ms
tacticAnalysis 10.6ms
type checking 5.12ms
typeclass inference 111ms
real 1.22
user 0.92
sys 0.44
LeanPool/PFR/ApproxHomPFR.lean
import took 954ms
simp took 151ms
simp took 331ms
typeclass inference of Nonempty took 153ms
simp took 102ms
cumulative profiling times:
aesop 87.5ms
attribute application 0.0837ms
congr simp thm 25.3ms
elaboration 69.1ms
fix level params 6.26ms
grind 15.4ms
grind mark subsingleton 1.66ms
grind simp 3.11ms
import 954ms
initialization 31.6ms
instantiate metavars 10.9ms
interpretation 975ms
let-to-have transformation 0.218ms
linting 60.9ms
module linting 0.00179ms
norm_num 20.1ms
overlappingInstancesLinter 9.12ms
parsing 17.7ms
process pre-definitions 29.7ms
ring 15.3ms
share common exprs 28.3ms
simp 1.6s
sym canon 4.45ms
sym typeclass inference 91.6ms
tactic execution 948ms
tacticAnalysis 66.9ms
type checking 168ms
typeclass inference 4.23s
real 6.55
user 9.32
sys 0.62
LeanPool/PFR/BoundingMutual.lean
import took 947ms
typeclass inference of Nonempty took 106ms
typeclass inference of Nonempty took 106ms
lazy discriminator import initialization took 802ms
tactic execution of Lean.Parser.Tactic.congr took 155ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 128ms
cumulative profiling times:
aesop 24.4ms
attribute application 0.158ms
blocked (unaccounted) 9.55s
build module discriminator tree 0.715ms
compilation (IR) 0.334ms
compilation (LCNF base) 2.09ms
compilation (LCNF impure) 1.42ms
compilation (LCNF mono) 1.78ms
congr simp thm 26.2ms
dsimp 3.23ms
elaboration 104ms
fix level params 7.86ms
import 947ms
initialization 32.1ms
instantiate metavars 14.2ms
interpretation 2.31s
lazy discriminator import initialization 802ms
lazy discriminator local search 0.0486ms
let-to-have transformation 1.67ms
librarySearch 24.5ms
linting 103ms
module linting 0.00186ms
norm_num 13.9ms
overlappingInstancesLinter 12.3ms
parsing 40.7ms
process pre-definitions 44.8ms
ring 25.7ms
share common exprs 39.8ms
simp 1.35s
tactic execution 1.79s
tacticAnalysis 114ms
type checking 333ms
typeclass inference 4.08s
real 10.03
user 19.98
sys 1.51
LeanPool/PFR/Endgame.lean
import took 988ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 163ms
type checking took 265ms
cumulative profiling times:
aesop 303ms
attribute application 4.31ms
blocked (unaccounted) 4.54s
compilation (IR) 10.9ms
compilation (LCNF base) 303ms
compilation (LCNF impure) 37.9ms
compilation (LCNF mono) 92.3ms
congr simp thm 20.7ms
dsimp 0.876ms
elaboration 638ms
fix level params 12.5ms
grind 43.6ms
grind ac 0.332ms
grind cutsat 0.063ms
grind linarith 0.115ms
grind mark subsingleton 6.78ms
grind ring 0.108ms
grind simp 11.4ms
import 988ms
initialization 33.2ms
instantiate metavars 19.3ms
interpretation 3.05s
let-to-have transformation 1.22ms
linting 170ms
module linting 0.00143ms
norm_num 275ms
overlappingInstancesLinter 44.5ms
parsing 32.5ms
process pre-definitions 103ms
ring 191ms
share common exprs 74.8ms
simp 1.03s
sym canon 8.6ms
sym typeclass inference 179ms
tactic execution 1.06s
tacticAnalysis 382ms
type checking 537ms
typeclass inference 2.55s
real 10.01
user 12.34
sys 0.64
LeanPool/PFR/EntropyPFR.lean
import took 955ms
cumulative profiling times:
attribute application 0.0256ms
congr simp thm 1.13ms
elaboration 27.5ms
fix level params 1.32ms
import 955ms
initialization 31.3ms
instantiate metavars 1.09ms
interpretation 316ms
let-to-have transformation 0.0651ms
linting 10.5ms
module linting 0.00148ms
norm_num 33.9ms
overlappingInstancesLinter 4.09ms
parsing 2.85ms
process pre-definitions 3.82ms
ring 11.3ms
share common exprs 3.96ms
simp 0.848ms
tactic execution 100ms
tacticAnalysis 14.1ms
type checking 35.4ms
typeclass inference 77.5ms
real 1.98
user 1.57
sys 0.55
LeanPool/PFR/Fibring.lean
import took 950ms
tactic execution of Lean.Parser.Tactic.refine took 160ms
cumulative profiling times:
attribute application 0.106ms
blocked (unaccounted) 463ms
congr simp thm 12ms
elaboration 91ms
fix level params 4.31ms
import 950ms
initialization 37.3ms
instantiate metavars 5.83ms
interpretation 557ms
let-to-have transformation 0.311ms
linting 30.4ms
module linting 0.00184ms
norm_num 2.51ms
overlappingInstancesLinter 9.36ms
parsing 17.8ms
process pre-definitions 19.8ms
share common exprs 12.8ms
simp 62.4ms
tactic execution 618ms
tacticAnalysis 39.3ms
type checking 77.5ms
typeclass inference 479ms
real 2.22
user 2.83
sys 0.61
LeanPool/PFR/FirstEstimate.lean
import took 955ms
cumulative profiling times:
aesop 37.8ms
attribute application 0.554ms
blocked (unaccounted) 69.2ms
compilation (IR) 1.53ms
compilation (LCNF base) 32.6ms
compilation (LCNF impure) 5.47ms
compilation (LCNF mono) 10.9ms
congr simp thm 3.86ms
elaboration 164ms
fix level params 4.39ms
import 955ms
initialization 34.3ms
instantiate metavars 4.5ms
interpretation 924ms
let-to-have transformation 0.422ms
linting 36.8ms
module linting 0.00164ms
norm_num 107ms
overlappingInstancesLinter 14.1ms
parsing 16.1ms
process pre-definitions 31.4ms
ring 60ms
share common exprs 23.1ms
simp 47.1ms
tactic execution 392ms
tacticAnalysis 84.3ms
type checking 104ms
typeclass inference 523ms
real 3.05
user 3.53
sys 0.60
LeanPool/PFR/ForMathlib/AffineSpaceDim.lean
import took 662ms
cumulative profiling times:
attribute application 0.354ms
congr simp thm 0.225ms
elaboration 13.6ms
fix level params 0.0927ms
import 662ms
initialization 36.7ms
instantiate metavars 0.022ms
interpretation 145ms
let-to-have transformation 0.0316ms
linting 2.85ms
module linting 0.00161ms
overlappingInstancesLinter 4.37ms
parsing 1.41ms
process pre-definitions 0.589ms
share common exprs 0.21ms
simp 2.08ms
tactic execution 1.66ms
tacticAnalysis 7.2ms
type checking 1.99ms
typeclass inference 42.1ms
real 1.35
user 0.93
sys 0.46
LeanPool/PFR/ForMathlib/Entropy/Group.lean
import took 940ms
to_additive took 121ms
cumulative profiling times:
attribute application 1.22ms
blocked (unaccounted) 385ms
congr simp thm 1.29ms
elaboration 145ms
fix level params 1.64ms
import 940ms
initialization 32.1ms
instantiate metavars 0.64ms
interpretation 349ms
let-to-have transformation 0.325ms
linting 34.2ms
module linting 0.00178ms
norm_num 1.13ms
overlappingInstancesLinter 16.6ms
parsing 19.2ms
process pre-definitions 8.66ms
share common exprs 3.51ms
simp 29.7ms
tactic execution 97.8ms
tacticAnalysis 52.3ms
to_additive 321ms
type checking 63.9ms
typeclass inference 297ms
real 2.62
user 2.35
sys 0.58
LeanPool/PFR/ForMathlib/Entropy/Kernel/Group.lean
import took 951ms
to_additive took 117ms
cumulative profiling times:
attribute application 0.298ms
blocked (unaccounted) 181ms
congr simp thm 1.05ms
elaboration 67.5ms
fix level params 0.74ms
import 951ms
initialization 36ms
instantiate metavars 0.43ms
interpretation 248ms
let-to-have transformation 0.161ms
linting 16.6ms
module linting 0.00176ms
overlappingInstancesLinter 8.18ms
parsing 7.3ms
process pre-definitions 3.63ms
share common exprs 2.03ms
simp 13.4ms
tactic execution 73.5ms
tacticAnalysis 19.7ms
to_additive 207ms
type checking 31.3ms
typeclass inference 113ms
real 2.18
user 1.76
sys 0.54
LeanPool/PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean
import took 930ms
cumulative profiling times:
attribute application 0.878ms
blocked (unaccounted) 38.3ms
compilation (IR) 0.768ms
compilation (LCNF base) 20.1ms
compilation (LCNF impure) 2.71ms
compilation (LCNF mono) 5.03ms
congr simp thm 17.3ms
elaboration 144ms
fix level params 6.87ms
import 930ms
initialization 29.7ms
instantiate metavars 9.82ms
interpretation 702ms
let-to-have transformation 0.324ms
linting 48.9ms
module linting 0.00198ms
norm_num 32.6ms
overlappingInstancesLinter 17ms
parsing 26.8ms
process pre-definitions 29.9ms
ring 41.5ms
share common exprs 21.3ms
simp 590ms
tactic execution 754ms
tacticAnalysis 71.6ms
type checking 154ms
typeclass inference 792ms
real 2.65
user 4.35
sys 0.58
LeanPool/PFR/ForMathlib/Entropy/RuzsaDist.lean
import took 946ms
aesop took 240ms
simp took 101ms
cumulative profiling times:
aesop 801ms
attribute application 7.65ms
blocked (unaccounted) 8.94s
compilation (IR) 4.85ms
compilation (LCNF base) 133ms
compilation (LCNF impure) 18.6ms
compilation (LCNF mono) 39.9ms
congr simp thm 88.6ms
dsimp 57.5ms
elaboration 658ms
fix level params 30.1ms
import 946ms
initialization 36.5ms
instantiate metavars 40.4ms
interpretation 2.97s
let-to-have transformation 1.58ms
linting 284ms
module linting 0.00183ms
norm_num 202ms
overlappingInstancesLinter 63.3ms
parsing 107ms
process pre-definitions 136ms
ring 154ms
share common exprs 96ms
simp 3s
tactic execution 3.51s
tacticAnalysis 395ms
type checking 601ms
typeclass inference 5.72s
real 8.46
user 19.51
sys 0.80
LeanPool/PFR/ForMathlib/Entropy/RuzsaSetDist.lean
import took 932ms
cumulative profiling times:
aesop 45.9ms
attribute application 0.481ms
blocked (unaccounted) 47.1ms
compilation (IR) 0.664ms
compilation (LCNF base) 16.2ms
compilation (LCNF impure) 2.51ms
compilation (LCNF mono) 4.51ms
congr simp thm 4.2ms
elaboration 35.6ms
fix level params 2.13ms
import 932ms
initialization 30.1ms
instantiate metavars 1.95ms
interpretation 410ms
let-to-have transformation 0.114ms
linting 12.9ms
module linting 0.00167ms
overlappingInstancesLinter 7.39ms
parsing 6.56ms
process pre-definitions 6.92ms
share common exprs 3.88ms
simp 161ms
tactic execution 64.2ms
tacticAnalysis 21.9ms
type checking 20.2ms
typeclass inference 427ms
real 2.24
user 2.12
sys 0.58
LeanPool/PFR/ForMathlib/FiniteRange/IdentDistrib.lean
import took 889ms
cumulative profiling times:
aesop 20.1ms
attribute application 0.0439ms
compilation (IR) 0.0442ms
compilation (LCNF base) 0.409ms
compilation (LCNF impure) 0.163ms
compilation (LCNF mono) 0.255ms
congr simp thm 1.89ms
elaboration 33.2ms
fix level params 1.69ms
import 889ms
initialization 31.1ms
instantiate metavars 2.91ms
interpretation 299ms
let-to-have transformation 0.0864ms
linting 14.4ms
module linting 0.00164ms
overlappingInstancesLinter 3.99ms
parsing 5.99ms
process pre-definitions 5.93ms
share common exprs 3.76ms
simp 36.5ms
tactic execution 136ms
tacticAnalysis 20.3ms
type checking 23.6ms
typeclass inference 68.7ms
real 1.76
user 1.53
sys 0.54
LeanPool/PFR/ForMathlib/FourVariables.lean
import took 719ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 225ms
type checking took 237ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 227ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 245ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 229ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 227ms
type checking took 205ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 227ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 229ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 229ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 227ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 227ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 228ms
type checking took 131ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 228ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 222ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 223ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_FinCases___elabRules_Lean_Elab_Tactic_finCases_1._boxed took 223ms
type checking took 132ms
cumulative profiling times:
attribute application 0.686ms
blocked (unaccounted) 2.07s
compilation (IR) 0.285ms
compilation (LCNF base) 2.9ms
compilation (LCNF impure) 1.25ms
compilation (LCNF mono) 2.17ms
elaboration 188ms
fix level params 7.98ms
import 719ms
initialization 30.1ms
instantiate metavars 32.3ms
interpretation 4.36s
let-to-have transformation 0.333ms
linting 22.3ms
module linting 0.0015ms
overlappingInstancesLinter 11.2ms
parsing 11.8ms
process pre-definitions 70.5ms
share common exprs 30.2ms
tactic execution 695ms
tacticAnalysis 44.1ms
type checking 1.12s
typeclass inference 124ms
real 3.95
user 7.44
sys 0.52
LeanPool/PFR/ForMathlib/ThreeVariables.lean
import took 748ms
cumulative profiling times:
attribute application 0.545ms
blocked (unaccounted) 75.6ms
compilation (IR) 0.212ms
compilation (LCNF base) 2.15ms
compilation (LCNF impure) 0.917ms
compilation (LCNF mono) 1.53ms
elaboration 82.2ms
fix level params 0.981ms
import 748ms
initialization 30.9ms
instantiate metavars 3.73ms
interpretation 357ms
let-to-have transformation 0.0666ms
linting 6.9ms
module linting 0.00161ms
overlappingInstancesLinter 4.27ms
parsing 3.39ms
process pre-definitions 8.95ms
share common exprs 2.86ms
tactic execution 90.2ms
tacticAnalysis 14.9ms
type checking 45.1ms
typeclass inference 50.6ms
real 1.79
user 1.45
sys 0.52
LeanPool/PFR/HomPFR.lean
import took 950ms
cumulative profiling times:
attribute application 0.0276ms
congr simp thm 4.95ms
elaboration 28.4ms
fix level params 3.41ms
import 950ms
initialization 29.2ms
instantiate metavars 4.31ms
interpretation 543ms
let-to-have transformation 0.071ms
linting 17.3ms
module linting 0.0017ms
norm_num 25ms
overlappingInstancesLinter 4.52ms
parsing 9.01ms
process pre-definitions 7.82ms
ring 8.19ms
share common exprs 10.5ms
simp 144ms
tactic execution 466ms
tacticAnalysis 22.5ms
type checking 58.4ms
typeclass inference 1.39s
real 4.05
user 3.67
sys 0.56
LeanPool/PFR/HundredPercent.lean
import took 925ms
cumulative profiling times:
attribute application 0.785ms
blocked (unaccounted) 3.8ms
compilation (IR) 0.0386ms
compilation (LCNF base) 0.524ms
compilation (LCNF impure) 0.144ms
compilation (LCNF mono) 0.161ms
congr simp thm 4.31ms
dsimp 3.39ms
elaboration 51.3ms
fix level params 1.81ms
import 925ms
initialization 32ms
instantiate metavars 2.17ms
interpretation 481ms
let-to-have transformation 0.127ms
linting 21.8ms
module linting 0.00176ms
norm_num 19.1ms
overlappingInstancesLinter 7.18ms
parsing 11.5ms
process pre-definitions 6.16ms
ring 9.36ms
share common exprs 6.33ms
simp 107ms
tactic execution 206ms
tacticAnalysis 33.9ms
type checking 47.1ms
typeclass inference 418ms
real 2.35
user 2.31
sys 0.57
LeanPool/PFR/ImprovedPFR.lean
import took 923ms
tactic execution of Lean.Parser.Tactic.exact took 101ms
simp took 196ms
tactic execution of Lean.Parser.Tactic.refine took 103ms
tactic execution of Lean.Parser.Tactic.exact took 102ms
tactic execution of Lean.Parser.Tactic.exact took 101ms
tactic execution of Lean.Parser.Tactic.refine took 112ms
tactic execution of Lean.Parser.Tactic.refine took 111ms
tactic execution of Lean.Parser.Tactic.refine took 113ms
tactic execution of Lean.Parser.Tactic.refine took 112ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 188ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 100ms
tactic execution of Lean.Parser.Tactic.refine took 101ms
tactic execution of Lean.Parser.Tactic.refine took 103ms
tactic execution of Lean.Parser.Tactic.refine took 100ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 173ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 101ms
cumulative profiling times:
aesop 91.5ms
attribute application 4.27ms
blocked (unaccounted) 2.88s
compilation (IR) 11.4ms
compilation (LCNF base) 313ms
compilation (LCNF impure) 38.5ms
compilation (LCNF mono) 93.9ms
congr simp thm 25.9ms
dsimp 1.4ms
elaboration 668ms
fix level params 23.9ms
grind 33.5ms
grind ac 0.192ms
grind cutsat 0.0538ms
grind linarith 1.41ms
grind mark subsingleton 3.98ms
grind ring 0.174ms
grind simp 7.1ms
import 923ms
initialization 31.5ms
instantiate metavars 33.6ms
interpretation 3.93s
let-to-have transformation 1.57ms
linting 204ms
module linting 0.00138ms
norm_num 463ms
overlappingInstancesLinter 47.7ms
parsing 68.7ms
process pre-definitions 132ms
ring 463ms
share common exprs 133ms
simp 1.27s
sym canon 7.15ms
sym typeclass inference 148ms
tactic execution 4.58s
tacticAnalysis 420ms
type checking 609ms
typeclass inference 4.31s
real 10.16
user 19.09
sys 0.68
LeanPool/PFR/Kullback.lean
import took 927ms
simp took 159ms
cumulative profiling times:
aesop 111ms
attribute application 2.34ms
blocked (unaccounted) 647ms
compilation (IR) 2.7ms
compilation (LCNF base) 75.1ms
compilation (LCNF impure) 10.3ms
compilation (LCNF mono) 19.5ms
congr simp thm 21.3ms
elaboration 154ms
fix level params 5.61ms
import 927ms
initialization 35.5ms
instantiate metavars 8.47ms
interpretation 710ms
let-to-have transformation 0.461ms
linting 65ms
module linting 0.00165ms
norm_num 1.9ms
overlappingInstancesLinter 18ms
parsing 30.4ms
process pre-definitions 25.6ms
share common exprs 16.3ms
simp 732ms
tactic execution 488ms
tacticAnalysis 95.8ms
type checking 110ms
typeclass inference 1.15s
real 3.27
user 4.69
sys 0.60
LeanPool/PFR/Main.lean
import took 953ms
cumulative profiling times:
aesop 36ms
attribute application 0.274ms
blocked (unaccounted) 12ms
compilation (IR) 0.324ms
compilation (LCNF base) 5.7ms
compilation (LCNF impure) 1.27ms
compilation (LCNF mono) 1.89ms
congr simp thm 9.28ms
dsimp 6.94ms
elaboration 135ms
fix level params 6.39ms
import 953ms
initialization 30.3ms
instantiate metavars 10.4ms
interpretation 1.27s
let-to-have transformation 0.411ms
linting 72.2ms
module linting 0.00191ms
norm_num 228ms
overlappingInstancesLinter 15.1ms
parsing 33ms
process pre-definitions 33ms
ring 60.1ms
share common exprs 30.7ms
simp 367ms
tactic execution 965ms
tacticAnalysis 90.9ms
type checking 155ms
typeclass inference 2.39s
real 3.79
user 6.78
sys 0.60
LeanPool/PFR/Mathlib/Algebra/BigOperators/Fin.lean
import took 500ms
cumulative profiling times:
attribute application 0.0147ms
congr simp thm 0.763ms
elaboration 4.75ms
fix level params 0.0967ms
import 500ms
initialization 30.1ms
instantiate metavars 0.129ms
interpretation 131ms
let-to-have transformation 0.022ms
linting 1.1ms
module linting 0.00166ms
overlappingInstancesLinter 1.73ms
parsing 0.846ms
process pre-definitions 0.488ms
share common exprs 0.556ms
simp 12.8ms
tactic execution 1.54ms
tacticAnalysis 7.78ms
type checking 2.22ms
typeclass inference 19ms
real 1.14
user 0.77
sys 0.39
LeanPool/PFR/Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean
import took 361ms
cumulative profiling times:
attribute application 0.0301ms
blocked (unaccounted) 1.5ms
elaboration 5.53ms
fix level params 0.0188ms
import 361ms
initialization 30.1ms
instantiate metavars 0.0084ms
interpretation 105ms
let-to-have transformation 0.017ms
linting 1.84ms
module linting 0.00164ms
overlappingInstancesLinter 4.39ms
parsing 0.819ms
process pre-definitions 0.162ms
share common exprs 0.0379ms
tacticAnalysis 10.4ms
to_additive 23ms
type checking 0.68ms
typeclass inference 3.15ms
real 0.95
user 0.62
sys 0.36
LeanPool/PFR/Mathlib/Data/Fin/Basic.lean
import took 392ms
cumulative profiling times:
attribute application 0.0222ms
congr simp thm 0.18ms
elaboration 6.31ms
fix level params 0.0318ms
import 392ms
initialization 30ms
instantiate metavars 0.0474ms
interpretation 84.5ms
let-to-have transformation 0.0284ms
linting 1.11ms
module linting 0.00162ms
overlappingInstancesLinter 0.976ms
parsing 0.888ms
process pre-definitions 0.37ms
share common exprs 0.133ms
simp 0.753ms
tactic execution 1.04ms
tacticAnalysis 2.01ms
type checking 0.884ms
typeclass inference 1.09ms
real 0.95
user 0.62
sys 0.35
LeanPool/PFR/Mathlib/Data/Finset/Basic.lean
import took 413ms
cumulative profiling times:
attribute application 0.457ms
elaboration 3.1ms
fix level params 0.0192ms
import 413ms
initialization 29.4ms
instantiate metavars 0.00709ms
interpretation 106ms
let-to-have transformation 0.0172ms
linting 1.02ms
module linting 0.0017ms
overlappingInstancesLinter 2.1ms
parsing 0.581ms
process pre-definitions 0.129ms
share common exprs 0.0287ms
tacticAnalysis 6.44ms
type checking 0.278ms
typeclass inference 0.578ms
real 0.99
user 0.63
sys 0.38
LeanPool/PFR/Mathlib/LinearAlgebra/Basis/VectorSpace.lean
import took 601ms
cumulative profiling times:
attribute application 0.0227ms
elaboration 19.1ms
fix level params 1.55ms
import 601ms
initialization 36.8ms
instantiate metavars 2.85ms
interpretation 134ms
let-to-have transformation 0.0979ms
linting 4.39ms
module linting 0.00161ms
overlappingInstancesLinter 3.62ms
parsing 3.43ms
process pre-definitions 4.38ms
share common exprs 4.52ms
tactic execution 288ms
tacticAnalysis 8.99ms
type checking 41.5ms
typeclass inference 162ms
real 1.77
user 1.36
sys 0.43
LeanPool/PFR/Mathlib/LinearAlgebra/Dimension/Finrank.lean
import took 564ms
cumulative profiling times:
attribute application 0.0393ms
elaboration 1.95ms
fix level params 0.0241ms
import 564ms
initialization 41.7ms
instantiate metavars 0.00581ms
interpretation 101ms
let-to-have transformation 0.013ms
linting 0.642ms
module linting 0.00195ms
overlappingInstancesLinter 2.45ms
parsing 0.39ms
process pre-definitions 0.291ms
share common exprs 0.0401ms
tacticAnalysis 1.02ms
type checking 0.302ms
typeclass inference 5.96ms
real 1.17
user 0.77
sys 0.41
LeanPool/PFR/Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
import took 639ms
cumulative profiling times:
attribute application 0.0195ms
elaboration 8.47ms
fix level params 0.0768ms
import 639ms
initialization 30.5ms
instantiate metavars 0.0234ms
interpretation 134ms
let-to-have transformation 0.0225ms
linting 2.23ms
module linting 0.00172ms
overlappingInstancesLinter 3.39ms
parsing 0.9ms
process pre-definitions 0.403ms
share common exprs 0.189ms
tactic execution 12.6ms
tacticAnalysis 4.42ms
type checking 1.75ms
typeclass inference 32.5ms
real 1.28
user 0.88
sys 0.44
LeanPool/PFR/Mathlib/LinearAlgebra/Quotient/Basic.lean
import took 517ms
cumulative profiling times:
attribute application 0.333ms
elaboration 2.15ms
fix level params 0.0294ms
import 517ms
initialization 29ms
instantiate metavars 0.033ms
interpretation 96.1ms
let-to-have transformation 0.00792ms
linting 0.812ms
module linting 0.00172ms
overlappingInstancesLinter 3.67ms
parsing 0.329ms
process pre-definitions 0.253ms
share common exprs 0.0564ms
tactic execution 0.846ms
tacticAnalysis 2.87ms
type checking 0.788ms
typeclass inference 4.78ms
real 1.11
user 0.71
sys 0.42
LeanPool/PFR/Mathlib/MeasureTheory/Group/Arithmetic.lean
import took 679ms
cumulative profiling times:
attribute application 1.66ms
blocked (unaccounted) 9.95ms
congr simp thm 0.136ms
elaboration 4.3ms
fix level params 0.0532ms
import 679ms
initialization 35.9ms
instantiate metavars 0.00992ms
interpretation 140ms
let-to-have transformation 0.0195ms
linting 1.64ms
module linting 0.00192ms
overlappingInstancesLinter 1.4ms
parsing 0.76ms
process pre-definitions 0.26ms
share common exprs 0.125ms
simp 1.81ms
tactic execution 0.554ms
tacticAnalysis 2.5ms
to_additive 85.3ms
type checking 2.36ms
typeclass inference 7.94ms
real 1.41
user 0.97
sys 0.46
LeanPool/PFR/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
import took 897ms
cumulative profiling times:
attribute application 0.32ms
blocked (unaccounted) 0.169ms
congr simp thm 3.31ms
elaboration 34.7ms
fix level params 0.503ms
import 897ms
initialization 30.5ms
instantiate metavars 0.336ms
interpretation 295ms
let-to-have transformation 0.0828ms
linting 6.1ms
module linting 0.0015ms
overlappingInstancesLinter 6.28ms
parsing 5.07ms
process pre-definitions 2.19ms
share common exprs 1.35ms
simp 46.3ms
tactic execution 19.5ms
tacticAnalysis 13.8ms
type checking 11.1ms
typeclass inference 151ms
real 1.72
user 1.46
sys 0.55
LeanPool/PFR/Mathlib/Order/Interval/Finset/Defs.lean
import took 449ms
cumulative profiling times:
elaboration 1.28ms
import 449ms
initialization 29.4ms
interpretation 111ms
linting 0.808ms
module linting 0.00319ms
overlappingInstancesLinter 0.693ms
parsing 0.19ms
tacticAnalysis 6.43ms
typeclass inference 0.427ms
real 1.02
user 0.66
sys 0.37
LeanPool/PFR/Mathlib/Order/Interval/Finset/Fin.lean
import took 449ms
cumulative profiling times:
attribute application 2.33ms
elaboration 5.6ms
fix level params 0.0126ms
import 449ms
initialization 39.1ms
instantiate metavars 0.00893ms
interpretation 107ms
let-to-have transformation 0.0313ms
linting 0.832ms
module linting 0.0014ms
overlappingInstancesLinter 1.13ms
parsing 0.391ms
process pre-definitions 0.159ms
share common exprs 0.0381ms
tacticAnalysis 5.4ms
type checking 0.888ms
typeclass inference 0.895ms
real 1.03
user 0.66
sys 0.39
LeanPool/PFR/MoreRuzsaDist.lean
import took 920ms
tactic execution of Lean.Parser.Tactic.refine took 153ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 2.32s
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 124ms
simp took 163ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 241ms
aesop took 108ms
simp took 158ms
simp took 125ms
simp took 132ms
typeclass inference of Nonempty took 105ms
typeclass inference of Nonempty took 109ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 172ms
tacticAnalysis took 137ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 1.44s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 414ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 107ms
tactic execution of Congr!.congr! took 622ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 123ms
type checking took 140ms
simp took 149ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 168ms
tactic execution of Lean.Parser.Tactic.refine took 127ms
tactic execution of Lean.Parser.Tactic.refine took 229ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 116ms
type checking took 115ms
cumulative profiling times:
aesop 721ms
attribute application 2.43ms
blocked (unaccounted) 23.3s
compilation (IR) 3.1ms
compilation (LCNF base) 47.4ms
compilation (LCNF impure) 13.5ms
compilation (LCNF mono) 19.9ms
congr simp thm 120ms
dsimp 67ms
elaboration 816ms
fix level params 51.7ms
grind 11.7ms
grind mark subsingleton 1.37ms
grind simp 7.23ms
import 920ms
initialization 34ms
instantiate metavars 134ms
interpretation 9.95s
let-to-have transformation 6.39ms
linting 581ms
module linting 0.00163ms
norm_num 115ms
overlappingInstancesLinter 71.6ms
parsing 186ms
process pre-definitions 296ms
ring 206ms
share common exprs 214ms
simp 8.53s
sym canon 1.93ms
sym typeclass inference 7.67ms
tactic execution 12.8s
tacticAnalysis 746ms
type checking 1.4s
typeclass inference 15.7s
real 19.42
user 52.92
sys 0.96
LeanPool/PFR/MultiTauFunctional.lean
import took 959ms
cumulative profiling times:
attribute application 0.174ms
blocked (unaccounted) 223ms
congr simp thm 6.44ms
dsimp 5.3ms
elaboration 103ms
fix level params 3.06ms
import 959ms
initialization 41.7ms
instantiate metavars 2.22ms
interpretation 640ms
let-to-have transformation 0.27ms
linting 34.7ms
module linting 0.00174ms
norm_num 6.83ms
overlappingInstancesLinter 15.6ms
parsing 22.3ms
process pre-definitions 13.2ms
ring 18.5ms
share common exprs 9.19ms
simp 97.9ms
tactic execution 756ms
tacticAnalysis 51ms
type checking 83.5ms
typeclass inference 763ms
real 2.50
user 3.49
sys 0.58
LeanPool/PFR/RhoFunctional.lean
import took 951ms
tactic execution of Lean.Parser.Tactic.refine took 630ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 539ms
simp took 100ms
simp took 105ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 341ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 344ms
simp took 107ms
tactic execution of Lean.Parser.Tactic.exact took 153ms
tactic execution of Lean.Parser.Tactic.exact took 102ms
tactic execution of Lean.Parser.Tactic.exact took 164ms
tactic execution of Lean.Parser.Tactic.exact took 165ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_linarith_1._boxed took 130ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 131ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 493ms
cumulative profiling times:
aesop 201ms
attribute application 7.49ms
blocked (unaccounted) 7.73s
compilation (IR) 8.17ms
compilation (LCNF base) 230ms
compilation (LCNF impure) 28.6ms
compilation (LCNF mono) 56.6ms
congr simp thm 78.1ms
dsimp 18.3ms
elaboration 1.02s
fix level params 51.2ms
import 951ms
initialization 34.3ms
instantiate metavars 75ms
interpretation 8.36s
let-to-have transformation 4.46ms
linting 575ms
module linting 0.0018ms
norm_num 1s
overlappingInstancesLinter 84.5ms
parsing 181ms
process pre-definitions 267ms
ring 644ms
share common exprs 230ms
simp 3.38s
tactic execution 6.95s
tacticAnalysis 674ms
type checking 1.15s
typeclass inference 12.5s
real 16.57
user 38.59
sys 0.78
LeanPool/PFR/SecondEstimate.lean
import took 954ms
cumulative profiling times:
attribute application 0.703ms
blocked (unaccounted) 102ms
compilation (IR) 1.98ms
compilation (LCNF base) 49.2ms
compilation (LCNF impure) 6.81ms
compilation (LCNF mono) 15.4ms
congr simp thm 2.28ms
elaboration 78.9ms
fix level params 3.26ms
import 954ms
initialization 37.1ms
instantiate metavars 3.4ms
interpretation 743ms
let-to-have transformation 0.219ms
linting 30.7ms
module linting 0.00185ms
norm_num 84.8ms
overlappingInstancesLinter 11.1ms
parsing 6.82ms
process pre-definitions 21.1ms
ring 45.3ms
share common exprs 16.2ms
simp 11.4ms
tactic execution 518ms
tacticAnalysis 70.3ms
type checking 88.9ms
typeclass inference 489ms
real 2.83
user 3.24
sys 0.56
LeanPool/PFR/Solution.lean
import took 916ms
cumulative profiling times:
attribute application 0.135ms
congr simp thm 4.69ms
elaboration 107ms
fix level params 2.66ms
import 916ms
initialization 39.5ms
instantiate metavars 3.96ms
interpretation 572ms
let-to-have transformation 0.381ms
linting 30.1ms
module linting 0.00162ms
norm_num 15ms
overlappingInstancesLinter 9.74ms
parsing 14.5ms
process pre-definitions 9.89ms
ring 21.7ms
share common exprs 9.35ms
simp 129ms
tactic execution 230ms
tacticAnalysis 40.4ms
type checking 72.3ms
typeclass inference 1.72s
real 2.79
user 3.88
sys 0.55
LeanPool/PFR/TauFunctional.lean
import took 945ms
aesop took 142ms
cumulative profiling times:
aesop 142ms
attribute application 1.01ms
blocked (unaccounted) 72.1ms
compilation (IR) 1.31ms
compilation (LCNF base) 37.6ms
compilation (LCNF impure) 5.11ms
compilation (LCNF mono) 9.54ms
congr simp thm 7.41ms
elaboration 157ms
fix level params 2.44ms
import 945ms
initialization 37.2ms
instantiate metavars 2.37ms
interpretation 467ms
let-to-have transformation 0.276ms
linting 43.8ms
module linting 0.0027ms
norm_num 0.77ms
overlappingInstancesLinter 14.3ms
parsing 15.8ms
process pre-definitions 14.7ms
ring 17.7ms
share common exprs 8.04ms
simp 97.4ms
tactic execution 207ms
tacticAnalysis 72.9ms
type checking 56.8ms
typeclass inference 554ms
real 2.49
user 2.87
sys 0.56
LeanPool/PFR/TorsionEndgame.lean
import took 936ms
interpretation of Mathlib.Notation3._aux_Mathlib_Util_Notation3___elabRules_Mathlib_Notation3_notation3_1._boxed took 126ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 105ms
simp took 286ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 126ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 125ms
tactic execution of Lean.Parser.Tactic.contradiction took 172ms
tactic execution of Lean.Parser.Tactic.contradiction took 176ms
tactic execution of Lean.Parser.Tactic.contradiction took 196ms
simp took 272ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 111ms
simp took 107ms
simp took 510ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 114ms
cumulative profiling times:
aesop 75.9ms
attribute application 2.23ms
blocked (unaccounted) 32.5s
compilation (IR) 6.87ms
compilation (LCNF base) 159ms
compilation (LCNF impure) 23.5ms
compilation (LCNF mono) 53.6ms
congr simp thm 55.7ms
dsimp 3.89ms
elaboration 500ms
fix level params 29.5ms
grind 65.5ms
grind mark subsingleton 4.99ms
grind simp 65ms
import 936ms
initialization 29.3ms
instantiate metavars 47.3ms
interpretation 6.34s
let-to-have transformation 1.44ms
linting 257ms
module linting 0.013ms
norm_num 437ms
overlappingInstancesLinter 35ms
parsing 98.4ms
process pre-definitions 164ms
ring 316ms
share common exprs 155ms
simp 4.2s
sym canon 8.84ms
sym typeclass inference 154ms
tactic execution 4.86s
tacticAnalysis 378ms
type checking 803ms
typeclass inference 13.4s
real 12.85
user 33.13
sys 0.82
LeanPool/PFR/WeakPFR.lean
import took 934ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 296ms
simp took 286ms
simp took 127ms
simp took 214ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1._boxed took 120ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 308ms
type checking took 121ms
simp took 470ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 106ms
simp took 101ms
cumulative profiling times:
aesop 45.2ms
attribute application 0.343ms
blocked (unaccounted) 2.31s
compilation (IR) 0.217ms
compilation (LCNF base) 1.62ms
compilation (LCNF impure) 0.811ms
compilation (LCNF mono) 1.22ms
congr simp thm 43.5ms
elaboration 338ms
fix level params 23.7ms
import 934ms
initialization 37.4ms
instantiate metavars 79.8ms
interpretation 4.05s
let-to-have transformation 6.54ms
linting 236ms
module linting 0.0014ms
norm_num 214ms
overlappingInstancesLinter 26.5ms
parsing 75.9ms
process pre-definitions 137ms
ring 188ms
share common exprs 113ms
simp 2.43s
tactic execution 4.65s
tacticAnalysis 287ms
type checking 600ms
typeclass inference 8.74s
real 8.24
user 22.93
sys 0.76
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All six headline declarations match their card informals, including the hypotheses, cardinality bounds, exponents, and covering conclusions. |
| Novelty | ✅ pass |
None of the six headline results is already formalized in Mathlib or the pool. |
| Significance | ✅ pass |
The project formalizes a major research-level theorem in additive combinatorics and develops the entropic and additive-combinatorial theory supporting several quantitative variants. |
| Sources | ✅ pass |
The arXiv citation and pinned teorth/pfr and leanprover-community/add-combi revisions consistently credit the mathematical result and the prior Lean developments imported here. |
| Code quality (advisory) | 🤔 discuss |
The core is competent, but large copy-pasted proof families and dead pruning scaffolding create avoidable maintenance debt. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | The results assume the disclosed torsion, finiteness, nonemptiness, doubling, free finite-rank module, defect-containment, positivity, and approximate-additivity hypotheses; no undisclosed mathematical input is bundled into a headline. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | additive combinatorics and information theory |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The declarations prove the exponent-two bounds with exponents 12 and 9, the m-torsion bound with exponent 256 m³ + 1, the stated weak affine-dimension bound, and the two quantitative homomorphism results.
The contribution proves the polynomial Freiman–Ruzsa theorem, including characteristic-two, bounded-torsion, weak integer, homomorphism, and approximate-homomorphism forms, within a substantial theory of entropic Ruzsa distance and additive energy.
Code quality findings (3)
- agent-slop —
LeanPool/PFR/ImprovedPFR.lean:519
dist_diff_bound_1anddist_diff_bound_2manually assemble two symmetric normalization proofs using 61 one-use facts namedC1throughC30/C31. Changes to the distribution and entropy APIs will require parallel edits, and the symmetry is not represented in the Lean. Generalize the first bound over the reference variable/package orientation and derive the second by swappingX₁withX₂, or extract the shared normalization identities into reusable lemmas.
Evidence:dist_diff_bound_1containshave C1 : U + X₂' + X₁' = S := by abeland concludes withsimp only [C1, C2, C3, C4, C5, C7, C8, C9, C10, C11, C12, C13, C14, C15, C16, C17, C18, C19, C20, C21, C22, C23, C24, C25, C26, C27, C28, C29, C30] at I1 I2 I3 I4 I5 I6 ⊢. The mirrored theorem addshave C31 : d[X₂ # X₂'] = d[X₂ # X₂] := h₂.symm.rdist_congr_right hX₂.aemeasurableand concludes withsimp only [C1, C2, C3, C4, C5, C6, C7, C8, C9, C10, C11, C12, C13, C14, C15, C16, C17, C18, C19, C20, C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31] at I1 I2 I3 I4 I5 I6 ⊢. - duplicate-proof —
LeanPool/PFR/ForMathlib/FourVariables.lean:27
The sixteenreindex_four_*declarations repeat the same explicit-equivalence proof, changing only two permutation vectors. Define one private reindexing lemma for an arbitraryFin 4permutation and discharge each named convenience lemma with that helper; this centralizes the independence reindexing argument.
Evidence: The repeated family isreindex_four_abcd,reindex_four_abdc,reindex_four_acbd,reindex_four_acdb,reindex_four_adbc,reindex_four_adcb,reindex_four_bacd,reindex_four_badc,reindex_four_bcad,reindex_four_bcda,reindex_four_bdac,reindex_four_bdca,reindex_four_cadb,reindex_four_cabd,reindex_four_cbad, andreindex_four_dacb. A representative implementation ispublic lemma reindex_four_abdc : iIndepFun ![Z₁, Z₂, Z₄, Z₃] := by let σ : Fin 4 ≃ Fin 4 := { toFun := ![0, 1, 3, 2] invFun := ![0, 1, 3, 2] left_inv i := by fin_cases i <;> rfl right_inv i := by fin_cases i <;> rfl } refine .of_precomp σ.symm.surjective ?_ convert h_indep using 1 ext i fin_cases i <;> rfl. - agent-slop — PR-wide
The pruning left empty section shells with variables and opens but no declarations. Remove them rather than retaining dead structural residue.
Evidence:LeanPool/PFR/AddCombi/Mathlib/Combinatorics/Additive/Energy.leancontains `section CommGroup
variable [CommGroup G]
end CommGroupand then another emptysection CommGroup. LeanPool/PFR/ImprovedPFR.leanends withsection PFR
open Pointwise Set MeasureTheory ProbabilityTheory Real Fintype Function
variable {G Ω : Type*} [AddCommGroup G] [Module (ZMod 2) G] [Finite G]
{A B : Set G} {K : ℝ}
end PFR`.
Tokens: 1,732,617 in / 19,343 out across 5 rubric calls · Tier: flex / standard · Effort: xhigh · Cost: $14.6543
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.
Owner
Author
|
/review |
Contributor
|
LLM review skipped: Lean Action CI conclusion was |
Vilin97
added
the
needs-maintainer
Owner
Author
|
Automation disposition: needs-maintainer Reviewed exact head 623b5ed after a verified repair pass that removed 217 lines of dead compatibility scaffolding; all affected modules build. The mirrored thirty-step normalization proofs and repeated finite-permutation wrappers remain substantial design-level duplication, so the project is still below the 4/5 maintenance target. |
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
# Conflicts: # LeanPool/projects.yml
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
1 participant
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.
Summary
Imports the completed Polynomial Freiman–Ruzsa formalization and preserves all six closed
Palomar headlines:
Marton.pfr_conjectureMarton.pfr_conjecture_nineMarton.torsion_pfr_conjectureMarton.weak_pfr_intMarton.homomorphism_pfrMarton.approx_hom_pfrThe core development is human-written and the thin Palomar bridges were AI-assisted, so the
project is registered as
provenance: mix. The registry and entry module credit all 25formalization contributors recorded by upstream.
Authoritative sources:
teorth/pfrat07839bddb1395c8808fa47db821ce2e4fff9362eleanprover-community/add-combiat2d061f437c1ba00ba9b16d7cba1c7603ba4807a4PFRPalomar/Challenge.leanand its six deliberate holes are not imported.Closure and optimization
899 reachable declarations among 1,318 upstream declarations; the conservative pruning pass
removed 11 irrelevant modules and 239 dead declaration commands while retaining
elaboration-only instances and attributes needed by downstream files.
LeanPool.ZhangYeungInequality.PFRfor the shared entropy, finite-range,independence, probability-kernel, and Mathlib compatibility cone. This deletes 26 duplicate
modules totaling 5,681 source lines. The direct reused entry APIs are
ForMathlib.Entropy.Basic,ForMathlib.Entropy.Kernel.MutualInfo,ForMathlib.FiniteRange.Defs,ForMathlib.Pair,Mathlib.Analysis.SpecialFunctions.NegMulLog,Mathlib.Probability.IdentDistrib, andMathlib.Probability.Independence.Basic.AddCombi.BSGcone: 10 files / 1,264 lines.PFR/Tactic/RPowSimp.lean, its forbiddenpartialmetaprogram, and all 18 call sites;each use is now a direct terminating algebraic proof. Removed every upstream
set_option.The final largest file has 2,360 non-comment code lines, and every proof is below 200.
privatedeclarations and retained documented publicdeclarations where cross-module consumers require them.
Physical Lean source is 23,257 -> 16,777 lines: 6,480 lines removed (27.86%). The final
endpoint cone has 51 modules and 13,776 non-comment code lines.
Compile profile
With Mathlib dependencies warm and project artifacts removed:
Final wall times were 62.27 / 66.16 / 71.21 seconds on the shared host. The median is 2.0%
faster and peak memory is 30.5% lower; CPU time is 5.7% higher, reported here rather than hidden
by wall-clock variance. The deterministic heartbeat pass found
phiMinimizer_exists_rdist_eq_zeroas the hotspot at 163 heartbeat units, far below the200,000-unit limit.
Verification
lake build LeanPool.PFR(project-artifact-clean, warning count 0)lake exe runLinter LeanPool.PFRlake exe lint-style LeanPool.PFR <all 50 leaf modules>lake exe mk_all --checksizes, registry, generated card, and registered declarations
LeanPool.PFR#checkfor all six headlines#print axiomsfor all six headlines: exactlypropext,Classical.choice, andQuot.sound