Skip to content

chore: bump Lean and Mathlib to v4.34.0-rc1 - #336

Merged
Vilin97 merged 14 commits into
mainfrom
bump/v4.34.0-rc1
Aug 14, 2026
Merged

chore: bump Lean and Mathlib to v4.34.0-rc1#336
Vilin97 merged 14 commits into
mainfrom
bump/v4.34.0-rc1

Conversation

@github-actions

@github-actions github-actions Bot commented Aug 11, 2026 •
edited by Vilin97
Loading

Copy link
Copy Markdown
Contributor

Migration

  • pin Lean and Mathlib to v4.34.0-rc1
  • repair affected formalizations across the pool
  • update lean4export for the matching Lean toolchain
  • migrate Lean 4.34 conditional and deprecation aliases
  • remove newly detected no-op tactics and unused hypotheses/arguments

The exposition parser fix from #337 and complement-mask frame-checker optimization from #338 are now on main; this PR contains only the Lean/Mathlib migration diff on top of them.

Validation

  • exact-head Lean Action CI: all ten shards, assembly, linters, quality gates, and final project gate green
  • exact-head Exposition Verify: declaration extraction and minimal-file validation green
  • exact-head Documentation: Mathlib data, doc-gen4 site, and exposition site green; deployment-only jobs expected-skipped
  • current-head LLM review: approved, no tech debt, improved maintainability, greater robustness, low risk
  • current-head Greptile: 5/5, no findings

A fresh proof profile against the updated main base is being rerun before merge.

@github-actions

github-actions Bot commented Aug 12, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

🤖 LLM review — refactor (gpt-5.6-sol)

Reviewed head: a53fad629f2d590d303d80d268ad7e9f1d16bd9f

Verdict: ✅ approve

This is a pool-wide Lean and Mathlib migration: most edits replace deprecated conditional, equivalence, linear-equivalence, and polynomial APIs, remove no-op tactics and unused instance assumptions, and make a few elaboration-sensitive proofs more explicit. The changes retain existing proof structure and do not introduce broader automation or dead compatibility layers.

Aspect Value
Scope toolchain and API migration
Introduces tech debt ✅ no
Maintainability ✅ improved
Brittleness ✅ more_robust
Risk ✅ low

The migration removes dependencies on deprecated APIs and unnecessary instance arguments without making the proofs more opaque or automation-dependent.

Tokens: 351,053 in / 1,732 out · Tier: flex · Effort: xhigh · Cost: $1.7942 (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

@Vilin97
Vilin97 marked this pull request as ready for review August 13, 2026 03:21
@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/profile

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/review

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

@greptileai review this draft

@greptile-apps

greptile-apps Bot commented Aug 13, 2026 •
edited
Loading

Copy link
Copy Markdown

Greptile Summary

This PR upgrades the repository, documentation build, and challenge tooling to Lean and Mathlib v4.34.0-rc1.

  • Updates toolchain and dependency pins consistently across the main and documentation builds.
  • Applies repository-wide compatibility repairs for conditional aliases, changed APIs, and newly redundant proof steps.
  • Keeps the challenge exporter pin aligned with the upgraded Lean toolchain.

Confidence Score: 5/5

The PR appears safe to merge.

No blocking failure remains.

Important Files Changed
Filename Overview
lean-toolchain Pins the primary build to the new Lean release candidate as part of the repository-wide migration.
lakefile.toml Updates the primary Mathlib and supporting dependency configuration for the new toolchain.
lake-manifest.json Regenerates the primary dependency lock data to match the upgraded package set.
docbuild/lean-toolchain Keeps the documentation build on the same Lean release candidate.
scripts/challenge/pins.env Aligns challenge-export infrastructure with the upgraded Lean toolchain.
LeanPool/AndersonConjecture/Jensen/Avoidance.lean Repairs proof terms for changed Mathlib APIs and removes an unused intermediate hypothesis.
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean Migrates deprecated conditional-rewrite aliases and removes redundant simplification steps.

Reviews (4): Last reviewed commit: "Merge remote-tracking branch 'origin/fix..." | Re-trigger Greptile

greptile-apps[bot]
greptile-apps Bot reviewed Aug 13, 2026
View reviewed changes
Comment thread lean-toolchain
@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/profile

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/review

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

@greptileai review this pull request

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

The proof_* declarations are intentionally separate but unsupported implementation details, not supported API:

  • I tested moving them to local have chains. Lean then exceeded the 200,000-heartbeat per-declaration limit at four separate certificate steps. Raising maxHeartbeats would be a forbidden waiver, so the expensive checks must remain separately budgeted declarations.
  • Stable names are required here: exposition re-elaborates the source against an already-loaded environment, and stable declarations let it reject them before recomputing the expensive Boolean validations.
  • The proof_n prefix is the Lean implementation-detail convention (Name.isInternalDetail). doc-gen filters such names, and Lean Pool exposition uses the same filter. A targeted extraction test on this head produced only the seven booster_0_valid through booster_6_valid certificates from this namespace; none of the proof_* declarations entered the public graph.
  • The module builds at the normal heartbeat limit, both Lean linters pass, and full repository quality checks pass.

So these names are technically addressable in Lean, as implementation-detail names are, but they are explicitly isolated from the supported/documented API. I am treating this repeated finding as non-actionable.

@github-actions

github-actions Bot commented Aug 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 5535.68 s (= 92.26 min) — user 20469.25 s, sys 1384.65 s.

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.

Base→head comparison skipped: this PR changes the toolchain, manifest, or lakefile, so the two sides would not be comparable.

Statement changes

⚠️ 147 declarations changed their statement across 50 files — a statement change is more than a refactor. Confirm each one is intended.

⚠️ Statements changed (147)
  • close_up_aux_factor_intersection_large — LeanPool/AndersonConjecture/Jensen/CloseUp/IntersectionHelpers.lean
  • close_up_aux_factor_intersection_large_proof — LeanPool/AndersonConjecture/Jensen/CloseUp/IntersectionHelpers.lean
  • heitmann_prop1_surj_pow — LeanPool/AndersonConjecture/Jensen/Construction/HeitmannProp.lean
  • map_maxIdeal_eq_of_surj_closed — LeanPool/AndersonConjecture/Jensen/Construction/HeitmannProp.lean
  • map_maxIdeal_le_of_closed — LeanPool/AndersonConjecture/Jensen/Construction/HeitmannProp.lean
  • mk_union_nsub_aux — LeanPool/AndersonConjecture/Jensen/Construction/Transfinite.lean
  • jensen_map_maxIdeal_eq_of_surj_closed — LeanPool/AndersonConjecture/Jensen/Jensen.lean
  • build_height_bound_proof — LeanPool/AndersonConjecture/Jensen/KrullDomain/HeightBound.lean
  • normalClosure_isSeparable — LeanPool/BrauerGroupNew/Subfield/Separable.lean
  • RelativeBrGroup.crossProduct_F_smul_eq_K_smul — LeanPool/BrauerGroupNew/ToSecond.lean
  • ChannelCapacity.exists_unique_capacity_achieving_prior_of_finite_aux — LeanPool/ChannelCapacity/Finite.lean
  • PeriodPair.Fm_isElliptic — LeanPool/Chudnovsky/DivisionValues.lean
  • CircuitComplexity.ShannonUpper.andLayerSem_eq — LeanPool/CircuitComplexity/Internal/ShannonUpper.lean
  • CircuitComplexity.ShannonUpper.andLayerSem_ne — LeanPool/CircuitComplexity/Internal/ShannonUpper.lean
  • CircuitComplexity.ShannonUpper.colFun_at_actual_bits — LeanPool/CircuitComplexity/Internal/ShannonUpper.lean
  • CircuitComplexity.ShannonUpper.or_andLayerSem_eq_f — LeanPool/CircuitComplexity/Internal/ShannonUpper.lean
  • CircuitComplexity.ShannonUpper.shannonGateArray — LeanPool/CircuitComplexity/Internal/ShannonUpper.lean
  • CircuitComplexity.size_complexity_cast — LeanPool/CircuitComplexity/Nondeterminism.lean
  • VML.aestronglyMeasurable_fderiv_apply — LeanPool/Clawristotle/CoulombFluxDiff.lean
  • CutAndProject.cumulative_hits_mono — LeanPool/CutAndProject/Basic.lean
  • CutAndProject.cumulative_hits_unit_mono — LeanPool/CutAndProject/Basic.lean
  • CutAndProject.sorted_multiset_of_lt_N — LeanPool/CutAndProject/Basic.lean
  • CutAndProject.sorted_multiset_unit_of_lt_N — LeanPool/CutAndProject/Basic.lean
  • good_on_support_gives_row_response — LeanPool/FormalLearningTheory/Complexity/Compression.lean
  • growth_exp_le_delta — LeanPool/FormalLearningTheory/Complexity/Symmetrization.lean
  • growth_exp_le_delta_large_v — LeanPool/FormalLearningTheory/Complexity/Symmetrization.lean
  • adviceValidationUniformBound — LeanPool/FormalLearningTheory/Theorem/Extended.lean
  • usedPrefix — LeanPool/FormalLearningTheory/Theorem/Extended.lean
  • boosted_sample_error_le_of_good_blocks — LeanPool/FormalLearningTheory/Theorem/Separation.lean
  • majority_error_le_seven_rate_of_good_fraction — LeanPool/FormalLearningTheory/Theorem/Separation.lean
  • HypergraphLowerBound.EdgesNonempty.map — LeanPool/FrontierMathOpenHypergraphs/Uniform.lean
  • HypergraphLowerBound.mapHypergraph — LeanPool/FrontierMathOpenHypergraphs/Uniform.lean
  • HypergraphLowerBound.mapHypergraph_card — LeanPool/FrontierMathOpenHypergraphs/Uniform.lean
  • irreducible_dim_zero_vanishing — LeanPool/GrothendieckVanishing/GrothendieckVanishing.lean
  • LO.FirstOrder.DerivabilityCondition.goedel_specAux₂ — LeanPool/Incompleteness/DC/Basic.lean
  • RS.Finiteness.sixterm_rank2 — LeanPool/JacobianDiffgeo/Finiteness/Chi.lean
  • Lean4Itree.tacticTestPredicate — LeanPool/Lean4Itree/Paco/PacoTactics.lean
  • HeckeRing.GLn.ker_entry_dvd — LeanPool/LeanModularForms/HeckeRIngs/GLn/Basic.lean
  • slTransvecG_mul_entry — LeanPool/LeanModularForms/HeckeRIngs/GLn/SLnTransvection.lean
  • slTransvecG_mul_right_entry — LeanPool/LeanModularForms/HeckeRIngs/GLn/SLnTransvection.lean
  • MisereGames.Form.Misere.Preservation.mem_of_mem_closedUnderDicoticClosure_of_isEndLike — LeanPool/MisereGames/Misere/Preservation.lean
  • MisereGames.Form.Misere.Preservation.not_isEndLike_of_mem_closedUnderDicoticClosure_of_not_mem — LeanPool/MisereGames/Misere/Preservation.lean
  • Qam.mul'_adjoint_commutes_with_innerAut_lm — LeanPool/Monlib4/QuantumGraph/Iso.lean
  • commutes_with_mul''_adjoint — LeanPool/Monlib4/QuantumGraph/Iso.lean
  • qamA.iso_iff — LeanPool/Monlib4/QuantumGraph/QamA.lean
  • qamA.isometric_starAlgEquiv_conj — LeanPool/Monlib4/QuantumGraph/QamA.lean
  • star_alg_equiv.is_isometry_iff — LeanPool/Monlib4/QuantumGraph/QamA.lean
  • GaussianField.NuclearTensorProduct.finsetSup_seminorm_ball_mem_nhds — LeanPool/OSforGFF/GaussianField/Nuclear/NuclearTensorProduct.lean
  • charFun_eq_GJGeneratingFunctional — LeanPool/OSforGFF/Measure/Construct.lean
  • boundedPaths_tail_bound — LeanPool/OSforGFF/Minlos/MeasurableModification.lean
  • … +97 more

Also: 1 declaration added, 0 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another.

➕ Declarations added (1)
  • Lean4GlCoalgebras.prover_sequent_eq_of_inl — LeanPool/Lean4GlCoalgebras/General/Completeness.lean

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Total heartbeats: 680,708 maxHeartbeats units across 448 files (2,378 added LOC).

Sum of lean --profile: 6471345.7 ms (= 6471.35 s). Import-excluded time: 5861935.7 ms (= 5861.94 s).

Count-heartbeats wall-clock total: 6541.58 s. Repeated import cost inside lean --profile: 609410.0 ms (= 609.41 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File LOC Heartbeats (maxHB) Count wall (s) lean --profile (s) Without import (s) Import (s) Decls Errors
LeanPool/BrauerGroupNew/IsoSecond.lean 1 273,709 164.46 85.32 83.36 1.96 62 18
LeanPool/Neukirch/HilbertRamificationTheory.lean 2 68,773 42.72 28.45 26.86 1.59 139 0
LeanPool/DirectedTopologyLean4/DirectedVanKampen.lean 5 28,686 20.04 16.64 15.47 1.17 68 0
LeanPool/BrauerGroupNew/Subfield/Separable.lean 2 19,198 25.66 14.14 12.36 1.78 23 0
LeanPool/Monlib4/LinearAlgebra/LmulRmul.lean 1 16,371 10.40 5.45 4.39 1.06 31 0
LeanPool/Monlib4/LinearAlgebra/PosMapIsReal.lean 2 15,035 31.38 33.21 31.56 1.65 78 0
LeanPool/RlTheoryInLean/Data/Matrix/Stochastic.lean 1 14,099 22.23 12.30 10.80 1.50 43 0
LeanPool/JacobianDiffgeo/Forms/Finiteness.lean 1 9,628 10.05 7.41 5.85 1.56 20 0
LeanPool/Monlib4/QuantumGraph/PiMat.lean 2 8,860 102.89 141.35 139.69 1.66 96 0
LeanPool/BruhatTits/Cartan/Existence.lean 1 8,827 25.97 19.37 17.90 1.47 45 0
LeanPool/BrauerGroupNew/ToSecond.lean 2 8,545 39.20 27.24 25.38 1.86 68 0
LeanPool/OSforGFF/GaussianField/Nuclear/NuclearTensorProduct.lean 5 8,495 24.92 17.46 16.01 1.45 78 0
LeanPool/Monlib4/LinearAlgebra/Ips/Pos.lean 3 7,083 14.31 12.30 10.74 1.56 40 0
LeanPool/AharoniKorman/Counterexample.lean 9 6,577 16.73 23.19 22.27 0.92 101 0
LeanPool/JacobianDiffgeo/CanonicalForms/Differential.lean 15 6,370 8.02 6.67 5.05 1.62 27 0
LeanPool/JacobianDiffgeo/JacFunctorial/Trace.lean 2 6,196 9.92 10.04 8.40 1.64 32 0
LeanPool/JacobianDiffgeo/Dbar/Form01.lean 2 5,932 9.90 4.15 2.53 1.62 25 0
LeanPool/GrothendieckVanishing/ZeroOutside.lean 7 5,808 13.53 13.52 12.17 1.35 25 0
LeanPool/JacobianDiffgeo/Dbar/Operator.lean 1 5,409 7.54 4.95 3.32 1.63 30 0
LeanPool/JacobianDiffgeo/CanonicalForms/MForm.lean 4 5,362 6.90 3.66 2.04 1.62 20 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/BuildStrategies.lean 3 5,245 5.64 6.42 5.46 0.96 50 0
LeanPool/Monlib4/LinearAlgebra/Ips/MatIps.lean 16 4,989 33.84 33.62 31.97 1.65 79 0
LeanPool/BrauerGroupNew/BrauerOverR.lean 5 4,939 13.20 10.00 8.21 1.79 16 0
LeanPool/OSforGFF/Minlos/MeasurableModification.lean 11 4,830 17.15 18.37 16.68 1.69 21 0
LeanPool/DirectedTopologyLean4/DihomotopyCover.lean 2 3,704 6.23 5.53 4.37 1.16 28 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Coding.lean 4 3,347 11.36 10.38 9.42 0.96 141 0
LeanPool/BruhatTits/Lattice/Construction.lean 1 3,145 14.14 15.74 14.27 1.47 72 0
LeanPool/Monlib4/QuantumGraph/Matrix.lean 4 3,017 81.83 67.76 66.09 1.67 47 0
LeanPool/JacobianDiffgeo/LaurentTail/Comparison.lean 9 2,995 23.25 42.32 40.71 1.61 28 0
LeanPool/Monlib4/QuantumGraph/Example.lean 4 2,912 16.53 12.99 11.31 1.68 47 0
LeanPool/SardMoreira/ContDiff.lean 1 2,721 12.76 7.24 5.80 1.44 23 0
LeanPool/BrauerGroupNew/SplittingOfCSA.lean 1 2,623 8.47 6.65 5.18 1.47 19 0
LeanPool/ConnesKreimer/Core.lean 8 2,247 24.95 31.28 29.92 1.36 157 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/One/Lift.lean 5 1,964 20.46 19.68 18.61 1.07 57 0
LeanPool/DemazureOperatorsLean/Demazure.lean 1 1,908 9.65 5.97 4.36 1.61 43 0
LeanPool/ZFLean/Rationals.lean 2 1,863 5.46 3.92 3.08 0.84 103 0
LeanPool/OSforGFF/Minlos/MinlosConcentration.lean 6 1,844 32.81 45.45 43.79 1.66 10 0
LeanPool/Duality/LinearProgramming.lean 2 1,749 20.10 23.12 22.05 1.07 50 0
LeanPool/OSforGFF/Bochner/FejerPD.lean 3 1,690 11.19 8.67 7.07 1.60 13 0
LeanPool/RamanujanTauMissesPrimes/Solution.lean 6 1,554 52.24 75.29 73.89 1.40 526 0
LeanPool/ZFLean/Naturals.lean 8 1,462 5.47 6.11 5.27 0.84 225 0
LeanPool/QuasiBorelSpaces/Sigma.lean 2 1,445 5.79 3.77 2.57 1.20 33 0
LeanPool/QuasiBorelSpaces/RoseTree/Basic.lean 1 1,372 3.41 1.93 1.12 0.81 35 0
LeanPool/JacobianDiffgeo/Cech/SixTerm.lean 3 1,355 22.90 45.33 43.71 1.62 16 0
LeanPool/Duality/FarkasSpecial.lean 3 1,298 18.40 17.98 16.91 1.07 29 0
LeanPool/DirectedTopologyLean4/PathCover.lean 6 1,284 6.94 7.67 6.52 1.15 23 0
LeanPool/UnconditionalSchauderBasis.lean 1 1,267 15.17 12.99 11.67 1.32 37 0
LeanPool/DomainTheory/ContinuousLattice/InverseLimits.lean 2 1,242 4.87 3.68 2.78 0.90 62 0
LeanPool/JacobianDiffgeo/CanonicalForms/LinearSystems.lean 1 1,240 6.81 4.96 3.33 1.63 16 0
LeanPool/JacobianDiffgeo/Finiteness/BddHolo.lean 1 1,236 6.70 5.71 4.10 1.61 16 0
LeanPool/Circuitlib/Circuit/Category/Combinational.lean 5 1,182 22.36 17.14 16.33 0.81 72 0
LeanPool/Monlib4/QuantumGraph/ToProjections.lean 1 1,132 49.80 35.88 34.20 1.68 50 0
LeanPool/OSforGFF/Minlos/PietschBridge.lean 4 1,120 15.43 13.20 11.55 1.65 25 0
LeanPool/SardMoreira/ContDiffMoreiraHolder.lean 56 1,120 17.61 12.88 11.42 1.46 26 0
LeanPool/JacobianDiffgeo/LaurentTail/Truncation.lean 2 1,084 9.99 3.62 2.00 1.62 13 0
LeanPool/JacobianDiffgeo/Cech/Cochains.lean 2 1,051 11.96 5.91 4.31 1.60 13 0
LeanPool/JacobianDiffgeo/Meromorphic/OrderEval.lean 13 1,038 5.41 3.65 2.05 1.60 23 0
LeanPool/LatticeTriangle/Solution.lean 14 1,034 73.34 116.82 115.08 1.74 517 0
LeanPool/CircuitComplexity/Internal/Simulation.lean 3 1,027 10.41 7.26 6.42 0.84 77 0
LeanPool/Incompleteness/DC/Basic.lean 2 1,000 6.86 5.02 4.11 0.92 30 0
LeanPool/OSforGFF/Covariance/Momentum.lean 3 941 25.99 33.31 31.66 1.65 85 0
LeanPool/LeanQuantumAlg/Core/Gate.lean 3 940 4.02 3.34 2.21 1.13 53 0
LeanPool/QuasiBorelSpaces/SeparatesPoints.lean 1 929 3.11 1.66 0.44 1.22 9 0
LeanPool/Flean/IntRounding.lean 4 923 6.68 6.76 5.88 0.88 44 0
LeanPool/JacobianDiffgeo/Meromorphic/Divisor.lean 4 905 6.08 4.01 2.40 1.61 22 0
LeanPool/Circuitlib/Circuit/Category/Sequential.lean 2 870 20.69 16.09 15.27 0.82 65 0
LeanPool/JacobianDiffgeo/Cech/Window.lean 4 857 11.01 3.99 2.37 1.62 11 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/Lift.lean 5 855 13.18 11.60 10.56 1.04 49 0
LeanPool/BrauerGroupNew/Wedderburn.lean 1 846 13.48 10.79 9.44 1.35 29 0
LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/IFT.lean 1 792 16.65 17.28 15.82 1.46 8 0
LeanPool/Monlib4/LinearAlgebra/InnerAut.lean 1 787 19.54 16.48 14.92 1.56 95 0
LeanPool/Monlib4/QuantumGraph/Iso.lean 4 751 18.89 18.39 16.73 1.66 22 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean 7 748 128.97 225.36 223.60 1.76 374 0
LeanPool/Monlib4/QuantumGraph/QamA.lean 5 744 44.47 54.11 52.45 1.66 39 4
LeanPool/DomainTheory/Neighborhood/Theorem75.lean 26 736 7.73 8.11 7.21 0.90 122 0
LeanPool/ZhangYeungInequality/PFR/Mathlib/Probability/Kernel/Disintegration.lean 1 724 9.43 11.36 10.19 1.17 63 0
LeanPool/JacobianDiffgeo/MeromorphicTrace/FunctionTrace.lean 2 720 5.72 3.34 1.71 1.63 5 0
LeanPool/Desargues/Basic.lean 4 715 8.04 7.09 6.18 0.91 42 0
LeanPool/DomainTheory/Neighborhood/Exercise617.lean 4 715 5.13 4.70 3.82 0.88 58 0
LeanPool/ZhangYeungInequality/Theorem2.lean 2 712 17.13 24.83 23.18 1.65 34 0
LeanPool/LeanModularForms/Modularforms/Derivative.lean 4 692 12.34 14.43 13.09 1.34 58 0
LeanPool/Chudnovsky/Ramanujan.lean 1 672 25.24 36.28 34.50 1.78 53 0
LeanPool/Burkholder/Majorants/MajorantPG2.lean 7 664 87.06 123.43 121.94 1.49 332 0
LeanPool/Burkholder/Majorants/MajorantPL2.lean 8 662 88.29 130.83 129.34 1.49 331 0
LeanPool/DemazureProduct/AspPerm.lean 2 655 12.80 16.06 15.14 0.93 171 0
LeanPool/QuasiBorelSpaces/MeasureTheory/Quantile.lean 4 655 4.38 3.34 1.81 1.53 13 0
LeanPool/JacobianDiffgeo/LaurentTail/TailSpace.lean 2 625 10.09 3.35 1.74 1.61 8 0
LeanPool/Brouwer/Brouwer.lean 1 624 8.61 9.11 7.71 1.40 28 0
LeanPool/Monlib4/LinearAlgebra/Ips/Functional.lean 6 604 12.67 12.48 10.84 1.64 48 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/CoveringClosedGame.lean 1 597 12.39 11.58 10.55 1.03 59 0
LeanPool/LeanModularForms/ValenceFormula/ModularInvariance.lean 3 594 7.17 5.86 4.24 1.62 27 0
LeanPool/CriticalPortraits/Portraits.lean 2 583 3.88 2.27 1.27 1.00 32 0
LeanPool/DirectedTopologyLean4/DirectedPathHomotopy.lean 1 553 9.53 7.14 5.99 1.15 46 0
LeanPool/JacobianDiffgeo/CechCount/Mul.lean 1 542 20.79 30.82 29.21 1.61 7 0
LeanPool/Monlib4/LinearAlgebra/Matrix/Basic.lean 6 540 9.30 10.39 8.85 1.54 51 0
LeanPool/LeanModularForms/ValenceFormula/OrbitSum.lean 1 528 6.66 5.17 3.55 1.62 24 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/GaleStewart.lean 1 521 4.09 1.97 1.01 0.96 9 0
LeanPool/LeanModularForms/HeckeRIngs/GL2/HeckeModularForm.lean 3 514 11.43 6.90 5.23 1.67 16 0
LeanPool/LeanQuantumAlg/Core/State.lean 1 508 3.97 1.73 0.62 1.11 21 0
LeanPool/PLAcceleratedNesterovLean/MorseBott/IFTProof.lean 1 495 18.95 16.67 15.21 1.46 5 0
LeanPool/DemazureOperatorsLean/StrongExchange.lean 8 474 7.34 5.83 4.79 1.04 40 0
LeanPool/Monsky/SegmentCounting.lean 2 473 20.03 29.74 28.27 1.47 94 0
LeanPool/JacobianDiffgeo/ResidueCalculus/MittagLeffler.lean 4 472 5.00 2.91 1.51 1.40 26 0
LeanPool/MinModulusUniqueMultisetSum/UniqueSums.lean 14 460 11.20 11.52 10.60 0.92 41 0
LeanPool/DomainTheory/Neighborhood/Theorem74.lean 5 418 8.27 6.09 5.24 0.85 40 0
LeanPool/CriticalPortraits/Forward.lean 3 415 8.56 5.92 4.94 0.99 75 0
LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/Defs.lean 23 410 8.48 7.32 6.09 1.23 41 0
LeanPool/Turan3/Turans3rdProof.lean 28 405 22.72 23.34 22.02 1.32 55 0
LeanPool/JacobianDiffgeo/Meromorphic/LinearSystem.lean 9 401 5.41 4.87 3.25 1.62 5 0
LeanPool/SemicircleLaw/SemicircleDistribution.lean 2 400 9.45 13.54 11.89 1.65 78 0
LeanPool/QuasiBorelSpaces/Rose.lean 1 391 5.43 4.47 2.92 1.55 17 0
LeanPool/FelConjecture/Solution.lean 7 388 15.32 23.49 22.08 1.41 194 0
LeanPool/Chudnovsky/Clausen.lean 12 387 40.86 48.04 46.27 1.77 46 0
LeanPool/SelbergSieve4/Applications/BrunTitchmarsh.lean 2 366 7.68 5.15 3.59 1.56 18 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean 16 362 74.69 92.61 90.95 1.66 181 0
LeanPool/Chudnovsky/DivisionValues.lean 15 361 40.93 51.84 50.09 1.75 139 0
LeanPool/Monlib4/Preq/StarAlgEquiv.lean 1 360 4.63 2.74 1.79 0.95 28 0
LeanPool/JacobianDiffgeo/Abel/UpgradeDischarge.lean 11 342 11.22 7.77 6.02 1.75 4 0
LeanPool/BrauerGroupNew/MoritaEquivalence.lean 2 334 16.85 10.36 9.17 1.19 17 0
LeanPool/DomainTheory/Neighborhood/Proposition77.lean 6 333 6.69 6.63 5.78 0.85 64 0
LeanPool/JacobianDiffgeo/PeriodLattice/Discreteness.lean 3 329 12.09 10.18 8.44 1.74 4 0
LeanPool/LeanModularForms/ValenceFormula/PVChain/ResidueSideInfra.lean 5 328 14.80 14.66 12.84 1.82 10 0
LeanPool/Odlyzko/ExplicitFormula/RegularizedPoitouContourLimit.lean 2 325 22.10 48.83 47.38 1.45 101 0
LeanPool/Chudnovsky/Liouville.lean 10 320 28.11 31.97 30.19 1.78 53 0
LeanPool/JacobianDiffgeo/CechCount/Count.lean 2 320 15.48 7.64 5.95 1.69 4 0
LeanPool/JacobianDiffgeo/AbelWeak/GeneralChain.lean 5 316 8.25 6.97 5.39 1.58 4 0
LeanPool/Monlib4/RepTheory/AutMat.lean 4 310 23.03 17.26 15.74 1.52 65 0
LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/Defs.lean 1 297 5.31 5.85 4.39 1.46 3 0
LeanPool/ComputableReal/ComputableRSeq.lean 12 293 42.90 46.66 45.74 0.92 133 0
LeanPool/ZFLean/Functions.lean 20 292 68.28 50.80 49.94 0.86 146 0
LeanPool/ZhangYeungInequality/PFR/Mathlib/Probability/Independence/Basic.lean 1 291 6.76 4.20 3.21 1.00 19 0
LeanPool/DemazureProduct/InvSet.lean 1 286 5.93 4.54 3.60 0.94 71 0
LeanPool/MisereGames/Misere/Comparison.lean 4 286 3.70 2.42 1.72 0.70 39 0
LeanPool/CriticalPortraits/Surjectivity.lean 4 282 11.59 13.48 12.49 0.98 84 0
LeanPool/LeanModularForms/ValenceFormula/CoreIdentity.lean 3 280 11.52 12.91 11.09 1.82 10 0
LeanPool/CutAndProject/Basic.lean 26 278 20.68 31.19 29.89 1.30 139 0
LeanPool/BooleanIsoperimetry/Compression.lean 30 274 17.62 18.87 17.90 0.97 137 0
LeanPool/FrontierMathOpenHypergraphs/Uniform.lean 9 274 23.96 37.39 36.46 0.93 128 0
LeanPool/Monlib4/LinearAlgebra/ToMatrixOfEquiv.lean 3 266 10.38 8.27 6.72 1.55 34 0
LeanPool/MisereGames/Ruleset/Strip.lean 3 265 8.41 10.16 9.41 0.76 76 0
LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/PhiN.lean 4 260 7.36 7.23 5.90 1.33 26 0
LeanPool/DomainTheory/Neighborhood/Recursive.lean 8 254 6.40 5.81 4.96 0.85 110 0
LeanPool/JacobianDiffgeo/ResidueTheorem/Reduction.lean 1 254 6.16 4.28 2.62 1.66 3 0
LeanPool/BrauerGroupNew/CentralSimple.lean 4 252 11.23 12.36 11.01 1.35 18 0
LeanPool/JacobianDiffgeo/Finiteness/Chi.lean 2 252 10.83 9.97 8.31 1.66 3 0
LeanPool/JacobianDiffgeo/CanonicalForms/Existence.lean 2 249 5.34 2.95 1.30 1.65 4 0
LeanPool/JacobianDiffgeo/ResidueCalculus/Residue.lean 3 248 5.11 4.34 2.96 1.38 22 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean 2 244 9.85 8.99 8.03 0.96 41 0
LeanPool/DemazureProduct/Submodular.lean 7 235 8.34 9.13 8.17 0.96 85 0
LeanPool/ABCExceptions/Section2.lean 4 232 27.15 34.35 33.05 1.30 99 0
LeanPool/JacobianDiffgeo/Path/Perturb.lean 4 232 5.89 4.55 2.93 1.62 3 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/DiagonalCosets.lean 14 231 26.47 26.91 25.60 1.31 57 0
LeanPool/FoZfc/Axioms.lean 6 230 8.28 7.36 6.47 0.89 115 0
LeanPool/JacobianDiffgeo/SerrePairing/TailSpace.lean 3 226 4.49 2.24 0.64 1.60 3 0
LeanPool/DomainTheory/Neighborhood/Theorem56Full.lean 8 225 5.60 3.70 2.80 0.90 76 0
LeanPool/Egrs75/CentralBinomialDigits.lean 4 225 5.11 2.74 1.78 0.95 18 0
LeanPool/Vlasov/OT/WeakToLagrangian.lean 11 224 77.54 178.56 176.90 1.66 28 0
LeanPool/JacobianDiffgeo/Meromorphic/Field.lean 1 218 4.46 2.22 0.63 1.59 8 0
LeanPool/Sundogcert/Certificate.lean 1 217 6.09 2.14 1.12 1.02 24 0
LeanPool/Monlib4/LinearAlgebra/Matrix/IncludeBlock.lean 6 212 11.85 9.91 8.37 1.54 72 0
LeanPool/Vlasov/OT/CharacteristicFlow.lean 12 212 69.51 84.67 82.98 1.69 94 0
LeanPool/Odlyzko/DedekindZeta/PrimeIdealEulerProduct.lean 1 210 5.47 5.08 3.67 1.41 46 0
LeanPool/JacobianDiffgeo/ResidueCalculus/TaylorCoeff.lean 4 204 4.91 3.25 1.90 1.35 21 0
LeanPool/LeanBooleanfun/Arrow.lean 1 204 10.33 5.21 3.76 1.45 19 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/HomologicalCauchy/DixonProof.lean 4 204 9.78 13.16 11.44 1.72 34 0
LeanPool/LeanQuantumAlg/Util/TrigPolynomial.lean 10 204 4.05 3.35 2.25 1.10 44 0
LeanPool/DomainTheory/Neighborhood/Exercise629.lean 7 202 3.91 2.53 1.73 0.80 47 0
LeanPool/OSforGFF/GaussianField/SchwartzNuclear/HermiteTensorProduct.lean 1 202 25.92 35.46 33.80 1.66 101 0
LeanPool/DemazureOperatorsLean/Matsumoto.lean 16 200 8.56 4.82 3.76 1.06 32 0
LeanPool/SteinhausThreeGap/Basic.lean 9 200 13.21 15.76 14.86 0.91 100 0
LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean 14 199 11.48 13.12 11.35 1.77 70 0
LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/Derivative.lean 1 198 29.17 14.38 12.88 1.50 2 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean 2 198 34.51 39.98 38.26 1.72 99 0
LeanPool/TwoColoringOneRound/LowerBound/N1000000IntersectionCounting.lean 2 198 17.87 12.15 11.03 1.12 42 0
LeanPool/Biswal/Theorem23.lean 1 196 15.90 15.78 14.29 1.49 98 0
LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean 9 196 9.15 9.26 7.49 1.77 56 0
LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/Residue.lean 4 190 8.46 8.88 7.60 1.28 19 0
LeanPool/JacobianDiffgeo/Dbar/SolveDisk.lean 1 189 7.21 6.44 4.87 1.57 27 0
LeanPool/JacobianDiffgeo/ResidueCalculus/LaurentCoeff.lean 6 189 4.89 5.37 4.00 1.37 21 0
LeanPool/LeanModularForms/Modularforms/SummableLems.lean 0 186 30.74 40.55 39.29 1.26 90 0
LeanPool/PolynomialMethodRestrictedSums/ANRPolynomialMethod.lean 14 186 24.90 32.15 31.01 1.14 31 0
LeanPool/ThreeGap/LinftyThreeTorusNine.lean 1 186 23.32 23.73 22.27 1.46 93 0
LeanPool/Lean4GlCoalgebras/Split/Completeness.lean 7 184 46.60 68.47 67.54 0.93 87 0
LeanPool/AndersonConjecture/Jensen/Avoidance.lean 5 182 11.56 12.56 11.07 1.49 17 0
LeanPool/PCFTheory/ClubGuessing.lean 4 175 4.53 1.85 0.86 0.99 21 0
LeanPool/CircuitComplexity/Internal/ShannonUpper.lean 47 174 60.34 67.77 66.83 0.94 87 0
LeanPool/LeanModularForms/HeckeRIngs/GL2/MultiplicationTable.lean 8 174 24.47 41.29 39.92 1.37 50 0
LeanPool/AndersonConjecture/CompleteDomain/LocalRing.lean 31 173 18.46 16.57 15.02 1.55 26 0
LeanPool/DirectedTopologyLean4/SplitPath/SplitProperties.lean 2 172 8.65 8.99 7.93 1.06 43 0
LeanPool/ErdosTuzaValtr/Etv/AlphaBeta.lean 4 172 3.34 2.62 1.73 0.90 22 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/PVInfrastructure/SingularAnnulus.lean 4 168 14.19 12.43 10.85 1.58 27 0
LeanPool/DomainTheory/Neighborhood/Exercise618.lean 2 166 4.07 2.59 1.72 0.87 49 0
LeanPool/Sabidussi/OrdinaryCircuit.lean 1 162 10.68 4.53 3.37 1.16 17 0
LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/RPoly.lean 12 160 8.99 10.43 9.11 1.32 16 0
LeanPool/JacobianDiffgeo/MeromorphicTrace/PlanarTrace.lean 15 160 7.49 6.61 5.08 1.53 16 0
LeanPool/Lean4GlCoalgebras/Logic/Syntax.lean 4 159 9.51 11.19 10.26 0.93 78 0
LeanPool/ZetaH123/H2.lean 33 156 25.37 35.69 34.47 1.22 78 0
LeanPool/HSDInteriorPointLP/LocalNeighborhoodEstimates.lean 6 154 13.79 19.36 17.89 1.47 77 0
LeanPool/MisereGames/Misere/Preservation.lean 2 154 4.33 3.58 2.88 0.70 50 0
LeanPool/OSforGFF/KolmogorovExtension4/CompactSystem.lean 3 154 8.48 3.45 2.29 1.16 24 0
LeanPool/Vlasov/OT/WellPosedness.lean 86 154 47.44 49.28 47.61 1.67 74 0
LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean 0 152 6.67 4.28 2.97 1.31 28 0
LeanPool/KaltonRoberts/Recombination.lean 1 152 17.28 15.09 13.59 1.50 18 0
LeanPool/ChannelCapacity/Finite.lean 3 151 9.19 8.15 6.49 1.66 12 0
LeanPool/JacobianDiffgeo/Meromorphic/LinSysMulEquiv.lean 1 151 5.03 2.76 1.15 1.61 2 0
LeanPool/JacobianDiffgeo/Meromorphic/Gluing.lean 1 150 4.16 2.05 0.44 1.61 2 0
LeanPool/LeanQuantumAlg/Core/Tensor.lean 3 150 4.54 3.76 2.60 1.16 50 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/PVInfrastructure/AnnulusBounds.lean 1 148 8.86 8.35 6.82 1.53 17 0
LeanPool/LeanQuantumAlg/Primitives/WalshHadamard.lean 2 144 5.71 3.34 2.21 1.13 48 0
LeanPool/Lean4GlCoalgebras/General/Completeness.lean 18 140 50.94 46.22 45.27 0.95 66 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/CoprimeMul.lean 1 137 21.84 16.08 14.73 1.35 18 0
LeanPool/BooleanIsoperimetry/Macaulay.lean 4 135 10.34 9.22 8.28 0.93 66 0
LeanPool/LeanQuantumAlg/Primitives/QSP/Fourier.lean 4 133 10.25 13.30 12.18 1.12 50 0
LeanPool/JacobianDiffgeo/JacFunctorial/TraceCoeff.lean 1 132 5.29 2.84 1.23 1.61 15 0
LeanPool/BooleanIsoperimetry/Cube.lean 1 130 13.40 16.14 15.20 0.94 65 0
LeanPool/LeanModularForms/SpherePacking/ViazovskaMagicFunction.lean 5 130 22.96 17.42 15.51 1.91 65 0
LeanPool/PCFTheory/Background/Topology.lean 1 130 5.90 2.45 1.47 0.98 16 0
LeanPool/Odlyzko/ExplicitFormula/GaussDigammaEqDigamma.lean 1 128 9.46 21.80 20.60 1.20 64 0
LeanPool/LeanModularForms/HeckeRIngs/AbstractHeckeRing/Module.lean 2 126 7.92 3.90 2.66 1.24 21 0
LeanPool/Sabidussi/CyclicWord.lean 6 126 10.63 4.69 3.69 1.00 21 0
LeanPool/Burkholder/MartingaleTransforms.lean 4 125 13.65 12.77 11.13 1.64 46 0
LeanPool/DemazureProduct/Transpositions.lean 23 124 6.67 6.42 5.48 0.94 62 0
LeanPool/OSforGFF/GaussianField/SchwartzNuclear/HermiteFunctions.lean 2 124 22.57 30.29 28.63 1.66 62 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/Basic.lean 1 123 7.49 5.38 4.07 1.31 25 0
LeanPool/LeanQuantumAlg/Primitives/QNN/VarianceFormula.lean 1 123 5.22 5.52 4.39 1.13 23 0
LeanPool/WhiteheadTheorem/Shapes/Pushout.lean 3 123 5.18 3.30 2.34 0.95 9 0
LeanPool/Chudnovsky/SingularModuli/JFunction.lean 2 122 16.58 14.98 13.22 1.76 61 0
LeanPool/Erdos132N14/Basic.lean 5 122 6.66 4.57 3.34 1.23 31 0
LeanPool/Lean4GlCoalgebras/Pdl/Game.lean 6 121 3.71 2.12 1.36 0.76 42 0
LeanPool/Lean4GlCoalgebras/Interpolation/PartialInterpolation.lean 8 120 93.06 62.02 61.08 0.94 60 0
LeanPool/Sundogcert/Degradation.lean 7 120 5.90 2.43 1.19 1.24 20 0
LeanPool/Chudnovsky/SigmaZeta.lean 7 118 18.03 17.66 15.89 1.77 40 0
LeanPool/JacobianDiffgeo/ResidueCalculus/PrincipalPart.lean 6 116 4.69 3.29 1.92 1.37 10 0
LeanPool/BooleanIsoperimetry/SimplicialCompression.lean 9 114 5.55 5.39 4.41 0.98 57 0
LeanPool/Erdos367/PellLimsup.lean 1 112 23.85 25.60 23.68 1.92 56 0
LeanPool/LeanQuantumAlg/Primitives/QSP/Chebyshev.lean 5 112 12.91 14.09 12.97 1.12 47 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/Games.lean 4 109 4.88 3.25 2.31 0.95 28 0
LeanPool/LeanQuantumAlg/Primitives/QKernel/Fourier.lean 11 108 4.89 3.62 2.54 1.08 34 0
LeanPool/TwoColoringOneRound/UpperBound/Recursive3Param/Bound.lean 1 108 19.25 31.47 29.94 1.53 54 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/ModulusRigidity.lean 2 104 45.88 50.57 48.90 1.67 52 0
LeanPool/BooleanIsoperimetry/Cascade.lean 4 102 11.46 13.06 12.10 0.96 51 0
LeanPool/LeanQuantumAlg/Util/Polynomial.lean 8 101 4.77 3.18 2.16 1.02 37 0
LeanPool/ZFLean/Isomorphisms.lean 40 101 33.46 36.62 35.76 0.86 25 0
LeanPool/SelbergSieve4/Applications/PrimeCountingUpperBound.lean 15 100 8.60 11.49 9.93 1.56 50 0
LeanPool/SardMoreira/LebesgueDensity.lean 1 99 11.37 21.35 19.77 1.58 23 0
LeanPool/FormalLearningTheory/Complexity/Generalization/Core.lean 17 98 22.31 30.98 29.33 1.65 49 0
LeanPool/LeanModularForms/ValenceFormula/RectHomotopy/AngleAnalysis.lean 2 98 10.11 11.08 9.29 1.79 49 0
LeanPool/CriticalPortraits/Denominator.lean 2 96 7.24 7.48 6.49 0.99 44 0
LeanPool/GrothendieckVanishing/FinitelyGeneratedVanishing.lean 1 96 23.24 12.87 11.51 1.36 6 0
LeanPool/Erdos97ConvexOctagon/CoverageCertificateChecker.lean 2 92 5.07 2.64 1.20 1.44 43 0
LeanPool/FormalLearningTheory/Complexity/Compression.lean 6 92 15.18 20.98 19.27 1.71 46 0
LeanPool/JacobianDiffgeo/Abel/LinkData.lean 4 90 8.38 5.18 3.51 1.67 4 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/BlockLocalization.lean 12 90 36.67 31.94 30.26 1.68 45 0
LeanPool/RamanujanNagell/Helpers.lean 1 90 13.46 12.67 11.43 1.24 45 0
LeanPool/ZetaH123/H1.lean 69 90 39.60 40.92 39.70 1.22 45 0
LeanPool/AndersonConjecture/AdicNoetherian.lean 3 89 21.96 15.01 13.57 1.44 5 0
LeanPool/ZFLean/Sum.lean 10 89 4.02 2.72 1.86 0.86 32 0
LeanPool/BannaiBannaiStanton/BoundOnDistanceSet.lean 5 88 14.04 13.86 12.39 1.47 30 0
LeanPool/ConnesKreimer/PowerSeriesLogMul.lean 1 88 5.99 4.02 2.75 1.27 8 0
LeanPool/LeanQuantumAlg/Algorithms/BernsteinVazirani.lean 1 87 4.33 2.32 1.20 1.12 29 0
LeanPool/KrafftSieve/OptimalWeights.lean 4 84 15.37 16.46 14.78 1.68 42 0
LeanPool/LeanModularForms/ValenceFormula/PVChain/ArcContribution.lean 8 84 11.89 13.58 11.76 1.82 3 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean 2 84 21.23 12.98 11.24 1.74 28 0
LeanPool/FormalLearningTheory/Complexity/Rademacher.lean 12 82 42.06 50.25 48.60 1.65 41 0
LeanPool/JacobianDiffgeo/Dbar/DiskAcyclic.lean 4 82 13.91 7.61 5.97 1.64 1 0
LeanPool/Monlib4/LinearAlgebra/PiDirectSum.lean 2 82 6.80 6.32 5.27 1.05 22 0
LeanPool/WhiteheadTheorem/RelHomotopyGroup/Algebra.lean 6 82 5.19 1.30 0.41 0.89 7 0
LeanPool/JacobianDiffgeo/GenusSphereHeadline/Basic.lean 2 81 6.56 2.71 0.98 1.73 2 0
LeanPool/CircuitComplexity/Internal/Schnorr.lean 9 80 25.38 30.94 30.03 0.90 40 0
LeanPool/JacobianDiffgeo/Abel/LogPiece.lean 7 80 7.32 5.99 4.38 1.61 27 0
LeanPool/LeanModularForms/ValenceFormula/RectHomotopy/PolygonProps.lean 5 79 10.00 8.85 7.06 1.79 38 0
LeanPool/LeanModularForms/HeckeRIngs/AbstractHeckeRing/Associativity.lean 7 78 10.97 9.85 8.60 1.25 13 0
LeanPool/LeanModularForms/HeckeRIngs/GL2/Basic.lean 2 78 5.98 4.09 2.73 1.36 21 0
LeanPool/PolynomialMethodRestrictedSums/CompressedSizesRestrictedSum.lean 1 78 14.61 9.80 8.60 1.20 13 0
LeanPool/IsTranscendentalPi/SubsetSumPolynomial.lean 1 76 7.30 8.22 6.63 1.59 38 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/SectorCurveLemma.lean 15 76 10.93 17.67 15.93 1.74 38 0
LeanPool/OSforGFF/Spacetime/TimeTranslation.lean 1 76 19.05 14.04 12.35 1.69 38 0
LeanPool/Vlasov/OT/Coupling.lean 18 76 17.92 14.13 12.49 1.64 29 0
LeanPool/AndersonConjecture/Jensen/CloseUp/CloseUp.lean 2 75 8.10 3.71 2.16 1.55 3 0
LeanPool/AndersonConjecture/Jensen/CloseUp/CoprimeSplit.lean 1 75 7.70 4.81 3.28 1.53 3 0
LeanPool/AndersonConjecture/Jensen/CloseUp/IntersectionHelpers.lean 0 75 6.49 3.69 2.21 1.48 3 0
LeanPool/AndersonConjecture/Jensen/CloseUp/IntersectionStep.lean 1 75 7.50 4.50 2.96 1.54 3 0
LeanPool/DomainTheory/ContinuousLattice/Constructions.lean 4 75 4.00 2.68 1.80 0.89 21 0
LeanPool/LeanModularForms/ValenceFormula/RectHomotopy/HomotopyDef.lean 3 74 15.37 18.98 17.19 1.79 37 0
LeanPool/SelbergSieve4/Selberg.lean 15 74 9.39 7.07 5.52 1.55 25 0
LeanPool/ThreeGap/EuclideanFiveDistanceSharpArith.lean 2 74 12.29 12.46 10.99 1.47 37 0
LeanPool/ArchonFirstProofResults/FirstProof6/Problem6.lean 17 73 19.78 20.72 19.16 1.56 18 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/SectorCurve.lean 16 72 9.37 10.29 8.56 1.73 36 0
LeanPool/FoZfc/BoundedFormulaOps.lean 5 71 3.76 2.85 1.97 0.89 18 0
LeanPool/PhaseRetrieval/Constant/Internal/MainTheorem.lean 1 70 25.49 26.17 24.53 1.64 35 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ProductBasisAndAnnuli.lean 6 70 14.21 12.95 11.27 1.68 35 0
LeanPool/Erdos137/BlockFramework.lean 6 68 7.83 7.83 6.45 1.38 34 0
LeanPool/KaltonRoberts/Intersections.lean 4 68 10.94 9.98 8.47 1.51 11 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/FlatnessTransfer/HigherOrderAssembly.lean 7 68 7.81 8.34 6.56 1.78 34 0
LeanPool/RootSystem/An.lean 2 68 92.94 111.10 109.64 1.46 31 0
LeanPool/LeanModularForms/Modularforms/Generators/Injectivity.lean 7 66 10.33 11.91 10.56 1.35 31 0
LeanPool/PLAcceleratedNesterovLean/Core/EmbeddedManifold.lean 4 66 30.57 30.51 29.02 1.49 22 0
LeanPool/FormalLearningTheory/Theorem/Separation.lean 5 64 10.41 11.73 10.04 1.69 32 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue.lean 1 64 6.77 7.03 5.28 1.75 32 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/SLnTransvection.lean 4 64 10.14 7.54 6.37 1.17 32 0
LeanPool/Erdos1196/Preliminaries.lean 2 62 14.92 14.08 12.51 1.57 31 0
LeanPool/Erdos137/Base.lean 8 62 5.05 3.65 2.26 1.39 31 0
LeanPool/Erdos97ConvexOctagon/CoverageSummaryValidity.lean 4 62 5.12 2.58 1.10 1.48 16 0
LeanPool/Erdos97ConvexOctagon/PairStateExactness.lean 1 61 4.25 3.12 1.67 1.45 22 0
LeanPool/PolyaEnumerationTheorem/PermutationAuxiliary.lean 4 61 5.66 2.40 1.37 1.03 22 0
LeanPool/CircuitComplexity/Internal/Valiant.lean 2 60 5.10 4.31 3.42 0.88 18 0
LeanPool/Erdos1196/HitMass.lean 1 60 7.22 7.45 5.90 1.55 30 0
LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean 1 60 16.76 19.33 17.70 1.63 30 0
LeanPool/ThreeGap/LinftyFiveDistanceSharpArith.lean 1 60 13.44 9.34 7.85 1.49 30 0
LeanPool/ZetaH123/Lem41.lean 17 60 11.78 15.39 13.81 1.58 30 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/CosetDecomposition.lean 2 59 9.23 5.15 3.84 1.31 20 0
LeanPool/FormalLearningTheory/Theorem/Extended.lean 2 58 26.32 18.03 16.35 1.68 29 0
LeanPool/LeanModularForms/ValenceFormula/RectHomotopy/PolygonSlope.lean 7 58 11.23 8.15 6.37 1.78 29 0
LeanPool/Lean4GlCoalgebras/Interpolation/Interpolants.lean 4 57 29.44 20.20 19.27 0.94 24 0
LeanPool/ZhangYeungInequality/Theorem5.lean 3 57 21.98 22.30 20.64 1.66 9 0
LeanPool/DomainTheory/Neighborhood/Exercise118.lean 4 56 3.74 1.89 1.01 0.88 23 0
LeanPool/MisereGames/Form/Adjoint.lean 1 56 4.40 2.64 1.93 0.71 19 0
LeanPool/AndersonConjecture/Main.lean 2 54 14.22 19.25 17.67 1.58 27 0
LeanPool/ComputableReal/SpecialFunctions/Pi.lean 1 54 10.92 11.66 10.20 1.46 27 0
LeanPool/LeanQuantumAlg/Algorithms/QPE.lean 1 53 4.32 2.32 1.19 1.13 18 0
LeanPool/AndersonConjecture/Jensen/Construction/Transfinite.lean 6 52 27.51 15.32 13.77 1.55 3 0
LeanPool/Erdos137/SquarefreeCapacity.lean 12 52 4.75 2.83 1.46 1.37 26 0
LeanPool/PartialCombinatoryAlgebras/PartialCombinatoryAlgebra.lean 5 52 5.09 1.99 1.21 0.78 15 0
LeanPool/SingularModuli/QuadraticOrder/RootCounting.lean 2 52 17.01 22.30 20.95 1.35 10 0
LeanPool/AndersonConjecture/Jensen/KrullDomain/HeightBound.lean 2 51 17.34 11.41 9.92 1.49 1 0
LeanPool/Erdos97ConvexOctagon/CoverageCertificateSemanticSoundness.lean 2 51 6.18 3.33 1.81 1.52 24 0
LeanPool/PumpingCfg/Pumping.lean 1 51 9.74 4.75 3.85 0.89 12 0
LeanPool/Sundogcert/Scaling.lean 10 51 3.92 2.19 1.07 1.12 17 0
LeanPool/AndersonConjecture/Jensen/CloseUp/Factor.lean 4 50 6.06 4.23 2.70 1.53 2 0
LeanPool/AndersonConjecture/Jensen/CloseUp/FactorDivisibility.lean 3 50 8.09 6.67 5.16 1.51 2 0
LeanPool/AndersonConjecture/Jensen/Construction/HeitmannProp.lean 0 50 7.55 7.24 5.89 1.35 2 0
LeanPool/Erdos1196/NormalizationCore.lean 6 50 9.34 7.89 6.31 1.58 25 0
LeanPool/LeanQuantumAlg/Core/Components/Kets.lean 6 50 3.79 2.36 1.24 1.12 25 0
LeanPool/LeanQuantumAlg/Primitives/QFT.lean 1 49 3.49 2.71 1.57 1.14 23 0
LeanPool/ComputableReal/SpecialFunctions/Sqrt.lean 6 48 11.58 17.04 15.69 1.35 24 0
LeanPool/OSforGFF/Measure/Construct.lean 1 48 12.65 4.64 2.91 1.73 24 0
LeanPool/Sundogcert/Looseness.lean 22 48 4.00 2.88 1.64 1.24 24 0
LeanPool/Sundogcert/Instance.lean 2 47 3.20 1.64 0.51 1.13 15 0
LeanPool/TwoColoringOneRound/LowerBound/N1000000BCompressionForB.lean 5 47 6.22 5.93 4.67 1.26 18 0
LeanPool/Chudnovsky/SingularModuli/Kronecker.lean 3 46 5.82 5.31 3.55 1.76 15 0
LeanPool/Chudnovsky/SingularModuli/Valence.lean 2 46 13.98 13.00 11.23 1.77 23 0
LeanPool/FormalLearningTheory/Complexity/Symmetrization.lean 2 46 41.28 43.39 41.71 1.68 23 0
LeanPool/LeanModularForms/ValenceFormula/Boundary/Winding/UnitArcHelpers.lean 3 46 18.99 17.92 16.13 1.79 23 0
LeanPool/PhaseRetrieval/Constant/Internal/BlockDecomposition.lean 1 46 7.49 6.16 4.51 1.65 23 0
LeanPool/TwoColoringOneRound/LowerBound/N1000000CorrAvgMatrixSymmDecompose.lean 4 46 15.08 17.35 16.08 1.27 23 0
LeanPool/LeanQuantumAlg/Util/HilbertSchmidt.lean 1 45 4.45 1.78 0.91 0.86 15 0
LeanPool/Vlasov/ForMathlib/PicardLindelof.lean 4 45 7.74 2.10 0.54 1.56 1 0
LeanPool/AndersonConjecture/CompleteDomain/Domain.lean 7 44 11.56 8.68 7.43 1.25 22 0
LeanPool/GKPCarry/UnitCarryCounting.lean 1 44 5.73 2.81 1.47 1.34 22 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/PhaseStability.lean 2 44 15.77 13.39 11.66 1.73 22 0
LeanPool/SelbergSieve4/AuxResults.lean 9 44 7.59 5.53 3.96 1.57 22 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/FlatnessTransfer/PerTermVanishing.lean 19 42 7.61 7.80 6.04 1.76 21 0
LeanPool/LeanModularForms/ValenceFormula/RectHomotopy/RadialHomotopy.lean 5 42 10.90 11.40 9.57 1.83 21 0
LeanPool/TwoColoringOneRound/UpperBound/Recursive3Param/Basic.lean 1 42 5.83 3.28 1.76 1.52 21 0
LeanPool/DeadEnds/InclusionExclusion.lean 1 40 7.77 3.13 1.57 1.56 20 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/WindingNumber/CrossingAnalysis.lean 10 40 16.99 19.10 17.34 1.76 20 0
LeanPool/AndersonConjecture/Jensen/Application.lean 4 38 7.18 9.74 8.15 1.59 19 0
LeanPool/DistanceGeometry/SchoenbergHard.lean 5 38 5.90 2.53 1.36 1.17 6 0
LeanPool/Erdos97ConvexOctagon/CoverageSearchRowChoiceSoundness.lean 2 38 32.84 22.98 21.54 1.44 19 0
LeanPool/FormalLearningTheory/Theorem/Online.lean 2 38 5.72 5.12 3.47 1.65 17 0
LeanPool/IsTranscendentalPi/NivenPolynomials.lean 3 38 5.37 3.93 2.34 1.59 19 0
LeanPool/PhaseRetrieval/Constant/Internal/AnnulusLocalEstimate.lean 3 38 10.18 14.56 12.93 1.63 19 0
LeanPool/ZetaH123/H3.lean 7 38 8.34 6.25 5.09 1.16 19 0
LeanPool/PolynomialMethodRestrictedSums/CauchyDavenportTheorem.lean 2 36 7.82 3.45 2.19 1.26 5 0
LeanPool/Odlyzko/TestFunction/Basic.lean 1 35 4.34 1.60 0.61 0.98 13 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/MeromorphicPrincipalPart.lean 7 34 6.03 6.24 4.49 1.75 17 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/MultipointPV/DominatedConvergence.lean 4 34 7.50 7.74 6.01 1.73 17 0
LeanPool/LeanModularForms/ValenceFormula/OnCurvePV/EndpointCorner.lean 9 34 18.11 16.89 15.08 1.81 17 0
LeanPool/PLAcceleratedNesterovLean/Convergence/MainTheoremInternal.lean 9 34 10.31 9.53 8.00 1.53 17 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/DegreeBookkeeping.lean 2 34 17.24 10.01 8.34 1.67 17 0
LeanPool/CencovPetz/PermutationInvariance.lean 2 32 5.41 3.05 1.72 1.33 8 0
LeanPool/Egrs75/DigitVector.lean 2 32 5.42 2.08 1.12 0.97 16 0
LeanPool/EcTateLean/Algebra/EllipticCurve/Kronecker.lean 5 30 3.92 1.52 0.74 0.78 15 0
LeanPool/FormalLearningTheory/Complexity/Littlestone.lean 1 30 5.91 1.74 0.55 1.19 9 0
LeanPool/ThreeGap/FiveDistance.lean 3 30 13.47 19.39 17.94 1.45 15 0
LeanPool/Erdos97ConvexOctagon/Incidence.lean 1 29 3.66 1.61 0.69 0.92 13 0
LeanPool/FoZfc/Replacement.lean 2 28 3.42 2.01 1.12 0.89 14 0
LeanPool/CircuitComplexity/Nondeterminism.lean 1 27 4.34 1.54 0.61 0.93 9 0
LeanPool/Sensitivity/Subcube.lean 1 27 2.35 1.26 0.42 0.84 10 0
LeanPool/Erdos137/RoughPartStructure.lean 6 26 4.33 2.35 0.95 1.40 13 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/HomologicalCauchy/Meromorphic.lean 1 26 9.90 6.66 4.90 1.76 13 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/FlatnessTransfer/CutoffInfrastructure.lean 2 26 18.65 17.12 15.37 1.75 13 0
LeanPool/AndersonConjecture/Jensen/CombinedStep.lean 5 25 13.90 14.20 12.67 1.53 1 0
LeanPool/AndersonConjecture/Jensen/Jensen.lean 4 24 9.21 11.59 10.00 1.59 12 0
LeanPool/Clawristotle/NewtonianPotential.lean 3 24 19.72 17.72 16.14 1.58 12 0
LeanPool/Erdos1196/Markov.lean 1 24 7.90 8.06 6.48 1.58 12 0
LeanPool/MisereGames/AugmentedForm/Lift.lean 2 24 2.41 1.64 0.92 0.72 12 0
LeanPool/Sabidussi/Parity.lean 1 24 7.26 2.34 1.35 0.99 12 0
LeanPool/ThreeGap/ChevallierCount.lean 1 24 3.01 1.75 0.82 0.93 8 0
LeanPool/AndersonConjecture/QuasiCompleteRing/QuasiCompleteRing.lean 3 23 11.19 15.00 13.50 1.50 10 0
LeanPool/AndersonConjecture/CompleteDomain/CompleteDomain.lean 1 21 10.60 8.97 7.42 1.55 9 0
LeanPool/LeanQuantumAlg/Core/Components/Oracle.lean 1 21 3.63 1.57 0.44 1.13 7 0
LeanPool/ThreeGap/TorusReduction.lean 1 21 5.26 1.99 0.85 1.14 7 0
LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/Transport.lean 2 20 5.11 2.88 1.56 1.32 2 0
LeanPool/Erdos137/RefinedOverlap.lean 11 20 7.60 6.35 4.96 1.39 10 0
LeanPool/JacobianDiffgeo/MappingDegree/RootCounting.lean 1 20 5.67 2.11 0.72 1.39 10 0
LeanPool/Lean4GlCoalgebras/Logic/FixedPointTheorem.lean 2 20 8.53 8.81 7.90 0.91 10 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/FlatnessTransfer/PerTermVanishing/CPVHelpers.lean 3 20 7.30 5.63 3.86 1.77 10 0
LeanPool/PhaseRetrieval/Constant/Internal/LocalHelpers.lean 2 20 11.62 4.93 3.30 1.63 10 0
LeanPool/Egrs75/MuFinish.lean 9 18 9.36 8.58 7.26 1.32 9 0
LeanPool/FormalLearningTheory/Learner/VersionSpace.lean 5 18 8.77 1.89 0.71 1.18 9 0
LeanPool/JacobianDiffgeo/Dbar/PlanarCousin.lean 1 18 4.71 2.36 0.81 1.55 2 0
LeanPool/JacobianDiffgeo/ResidueCalculus/ChangeOfVariables.lean 4 18 5.11 2.60 1.22 1.38 3 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/OnCurvePV/Basic.lean 1 18 8.43 6.91 5.15 1.76 9 0
LeanPool/Monlib4/LinearAlgebra/Matrix/IsAlmostHermitian.lean 1 18 5.55 2.95 1.44 1.51 9 0
LeanPool/Erdos97ConvexOctagon/CoverageCertificateNodeSoundness.lean 10 17 7.12 2.57 1.07 1.50 7 0
LeanPool/LeanModularForms/ValenceFormula/RectHomotopy/WindingProof.lean 2 16 8.68 5.60 3.81 1.79 8 0
LeanPool/SpectralPositivity/Matrix/MetzlerExp.lean 1 16 4.60 2.68 1.22 1.46 4 0
LeanPool/FormalLearningTheory/Complexity/FiniteSupportUC.lean 3 15 14.79 7.73 6.04 1.69 6 0
LeanPool/Clawristotle/CoulombPSDHelpers.lean 1 14 10.17 15.17 13.59 1.58 7 0
LeanPool/FormalLearningTheory/Complexity/DualVC.lean 6 14 4.53 2.24 1.05 1.19 5 0
LeanPool/GKPCarry/ModularPrefix.lean 2 14 3.62 1.54 0.60 0.93 7 0
LeanPool/JacobianDiffgeo/ResidueTheorem/RationalOnP1.lean 2 14 5.64 3.88 2.23 1.65 7 0
LeanPool/Odlyzko/TestFunction/Bounds.lean 3 14 6.31 3.90 2.69 1.21 7 0
LeanPool/Erdos1196/FirstEntryRowTerm.lean 2 12 5.17 2.21 0.60 1.61 6 0
LeanPool/Sundogcert/SATReductionForward.lean 8 12 13.26 9.13 8.06 1.07 1 0
LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/InvPhiN.lean 1 10 6.82 2.73 1.14 1.59 5 0
LeanPool/ArchonFirstProofResults/FirstProof4/Auxiliary/ObreschkoffTransport.lean 2 10 13.35 7.82 6.21 1.61 1 0
LeanPool/JacobianDiffgeo/ResidueTheorem/P1Assembly.lean 1 10 5.82 4.16 2.51 1.65 5 0
LeanPool/Monlib4/Preq/Ites.lean 2 10 3.82 1.33 0.40 0.94 4 0
LeanPool/ZFLean/IsomorphismsFunsToPowRel.lean 21 10 25.97 15.90 15.05 0.85 5 0
LeanPool/ZFLean/IsomorphismsZFNatIso.lean 5 10 3.73 2.09 1.23 0.85 5 0
LeanPool/Erdos97ConvexOctagon/CoverageCertificateLookup.lean 4 8 3.05 1.94 0.48 1.46 4 0
LeanPool/GrothendieckVanishing/GrothendieckVanishing.lean 1 8 11.18 6.18 4.82 1.36 4 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/PVInfrastructure/UniformStepBound.lean 10 8 6.69 3.48 1.93 1.55 4 0
LeanPool/ThreeGap/EuclideanNN.lean 1 8 4.76 2.16 0.70 1.46 4 0
LeanPool/Clawristotle/CoulombFluxDiff.lean 1 6 12.55 7.59 6.03 1.56 3 0
LeanPool/MinModulusUniqueMultisetSum/ElemAbelian2.lean 8 6 5.84 2.93 1.50 1.43 3 0
LeanPool/Erdos1196/Normalization.lean 3 4 9.27 6.00 4.44 1.56 2 0
LeanPool/FormalLearningTheory/Theorem/Gold.lean 4 4 5.21 2.88 1.70 1.18 2 0
LeanPool/LeanModularForms/ContourIntegral/CrossingLimit.lean 2 4 14.65 6.86 5.13 1.73 2 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/FlatnessTransfer/CPVExistence.lean 5 4 30.13 19.27 17.51 1.76 2 0
LeanPool/TwoColoringOneRound/LowerBound/N1000000BCompressionComputeSi.lean 3 4 9.77 4.76 3.51 1.25 2 0
LeanPool/LeanModularForms/ContourIntegral/PVSplit.lean 3 2 7.20 3.92 2.18 1.74 1 0
LeanPool/Sensitivity/Main.lean 2 2 4.75 2.30 1.03 1.27 1 0
LeanPool/Circuitlib/Circuit/Wires.lean 1 0 2.56 0.88 0.45 0.44 0 2
LeanPool/DomainTheory/Neighborhood/Exercise123.lean 8 0 2.49 1.27 0.69 0.58 0 2
LeanPool/DomainTheory/Neighborhood/Exercise316.lean 4 0 2.24 1.54 0.95 0.59 0 2
LeanPool/DomainTheory/Neighborhood/Exercise424.lean 2 0 2.00 0.91 0.36 0.56 0 2
LeanPool/JacobianDiffgeo/AbelWeak/SingleChart.lean 8 0 5.91 3.54 1.95 1.59 0 0
LeanPool/JacobianDiffgeo/ResidueCalculus/IntegralBridge.lean 2 0 5.17 2.93 1.40 1.53 0 0
LeanPool/Lean4Itree/Paco/PacoTactics.lean 3 0 2.54 2.96 2.15 0.81 0 2
LeanPool/LeanModularForms/ValenceFormula/PVChain/Assembly.lean 5 0 16.94 13.40 11.54 1.86 0 0
LeanPool/Lentil/ProofMode/Tactics/PurePred.lean 1 0 2.84 1.28 0.32 0.96 0 2
LeanPool/Lentil/ProofMode/Tactics/RCases.lean 1 0 2.66 2.89 1.96 0.94 0 2
LeanPool/Lentil/ProofMode/Tactics/Revert.lean 1 0 2.63 1.54 0.59 0.94 0 2
LeanPool/MRiscX/AbstractSyntax/Map.lean 2 0 1.50 0.68 0.47 0.21 0 2
LeanPool/Odlyzko/CompletedZeta/UnitSlabTranslation.lean 1 0 21.05 9.90 8.51 1.39 0 0
Total 2,378 680,708 6541.58 6471.35 5861.94 609.41 16715 40

Aggregate phase totals

Phase Time
typeclass inference 1544659.9 ms (= 1544.66 s)
tactic execution 1112245.7 ms (= 1112.25 s)
simp 953211.1 ms (= 953.21 s)
interpretation 855145.7 ms (= 855.15 s)
import 609410.0 ms (= 609.41 s)
blocked (unaccounted) 343025.1 ms (= 343.03 s)
type checking 325582.5 ms (= 325.58 s)
elaboration 198649.2 ms (= 198.65 s)
tacticAnalysis 80604.6 ms (= 80.60 s)
norm_num 67337.9 ms (= 67.34 s)
linting 51185.4 ms (= 51.19 s)
ring 48904.7 ms (= 48.90 s)

Slowest changed modules (from lake build)

Changed module Lake time
LeanPool.BrauerGroupNew.IsoSecond 181.00 s
LeanPool.PhaseRetrieval.DimdPoly.Internal.ExactModulusRecovery 149.00 s
LeanPool.Monlib4.QuantumGraph.PiMat 145.00 s
LeanPool.RootSystem.An 136.00 s
LeanPool.Burkholder.Majorants.MajorantPL2 131.00 s
LeanPool.Burkholder.Majorants.MajorantPG2 129.00 s
LeanPool.Lean4GlCoalgebras.Interpolation.PartialInterpolation 111.00 s
LeanPool.ZFLean.Functions 105.00 s
LeanPool.LatticeTriangle.Solution 103.00 s
LeanPool.PhaseRetrieval.DimdPoly.Internal.Hermitek.TrueLevelBasis 90.00 s
LeanPool.Vlasov.OT.WeakToLagrangian 87.00 s
LeanPool.Monlib4.QuantumGraph.Matrix 81.00 s

Comment truncated to fit GitHub's 64 KB limit. This PR profiles 448 files; the per-file table shows only the 448 hottest by heartbeats. The full table and raw lean --profile output for every file are in the run's step summary and proof-profile artifact.

Advisory only — never blocks merge.

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

Profile triage for run 31673664047: no unresolved source issue found.

  • The base→head comparison is correctly skipped because this PR changes the toolchain and manifest. The reported statement changes are the intentional v4.34 API-compatibility migrations already covered by the fresh full build and LLM review.
  • LeanPool.FrontierMathOpenHypergraphs.Uniform.FrameBoosters is the slowest changed module in the parallel profile run, but it built in 1099s on the latest-head Lean CI versus 1136s on the prior head; local before/after measurements were 307s/308s. The review fix did not introduce a compile-time regression.
  • The reported profile errors are artifacts of the profiler invoking raw lake env lean without Lake’s per-module --setup. Most are the missing linter.countHeartbeats option; the only proof diagnostics are in IsoSecond.lean and QamA.lean, and both reproduce only on that raw path. Both files pass when invoked with their Lake-generated setup JSON, matching the green normal Lake build.

So the profile is complete and does not identify a genuine issue requiring a source change.

@Vilin97
Vilin97 changed the base branch from main to fix/exposition-syntax-replay August 13, 2026 16:55
@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/profile

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/profile

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

Follow-up: this finding was valid, and the earlier rationale no longer describes the PR head. I removed the exposition-specific certificate refactor entirely: FrameBoosters.lean and FrameExact.lean are now unchanged from the stack base, so the private helpers remain private and no proof_* API is introduced. The actual replay bug is fixed in #337 by parsing declaration syntax without re-elaborating compiled declaration bodies.

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/profile

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/review

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

@greptileai

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

Removed the contributor-controlled merge-handling sentence from the PR description. The code review itself is approved: no tech debt, improved maintainability, and no source findings.

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/review

@Vilin97 Vilin97 mentioned this pull request Aug 13, 2026
Merged
@Vilin97
Vilin97 changed the base branch from fix/exposition-syntax-replay to fix/frame-complement-checker August 13, 2026 20:20
@Vilin97
Vilin97 changed the base branch from fix/frame-complement-checker to bump/frame-complement-checker August 13, 2026 20:22
@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/profile

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

/review

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

@greptileai

@Vilin97

Vilin97 commented Aug 13, 2026

Copy link
Copy Markdown
Collaborator

Fresh-head proof-profile triage (run 31740593428): no new source issue is identified.

  • The changed-module dependency build completed successfully in 3804.68s (63.41m), down from 4098.04s (68.30m) on the prior head.
  • The four frame-checker files are inherited byte-for-byte from Reduce frame validation to complement masks #338, so they correctly do not appear among this migration diff’s 448 profiled files or its slowest changed modules. Reduce frame validation to complement masks #338 independently validates the real FrameBoosters improvement with green CI and valid base/head timing.
  • The 147 statement changes across 50 files are the intentional Lean 4.34 API migrations already covered by the fresh green ten-shard build and current-head LLM/Greptile approvals.
  • The 40 raw profiler diagnostics are the same setup-path artifacts previously triaged (chiefly raw lean lacking Lake module setup); normal Lake compilation, assembly, linters, and repository quality checks are all green.

No profiling finding remains that calls for a change to this migration diff.

@Vilin97
Vilin97 changed the base branch from bump/frame-complement-checker to main August 14, 2026 04:24
@Vilin97

Vilin97 commented Aug 14, 2026

Copy link
Copy Markdown
Collaborator

/profile

@Vilin97
Vilin97 merged commit a7dc4d1 into main Aug 14, 2026
37 of 39 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Vilin97 Vilin97 Vilin97 left review comments
@greptile-apps greptile-apps[bot] greptile-apps[bot] left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Vilin97