Skip to content

Bump Lean and Mathlib to v4.34.0 - #436

Merged
Vilin97 merged 13 commits into
mainfrom
bump/v4.34.0
Sep 18, 2026
Merged

Bump Lean and Mathlib to v4.34.0#436
Vilin97 merged 13 commits into
mainfrom
bump/v4.34.0

Conversation

@github-actions

@github-actions github-actions Bot commented Sep 15, 2026 •
edited by Vilin97
Loading

Copy link
Copy Markdown
Contributor

Upgrade the root and documentation workspaces to Lean/Mathlib v4.34.0, align doc-gen4 and the challenge exporter, and repair affected formalizations. Integrate current main, preserving its polynomial-method optimizations and the Chvatal, ExpChaotic, FourAP, LanguageGeneration, MassFormula, MooreBound, SumDifferenceExponent, Schoenflies, and PDL additions.

The diff against current main contains no added or deleted files. Challenge McKay changes only its Complex import; its statement is unchanged. Solution files, workflows, gates, and linter settings are unchanged.

Main separately removed Forward Euler and Special Numbers in #422. This integration preserves that explicit curation decision: exactly six source files and five registered export targets were retired, with no additional loss. The resulting orphaned attribution metadata was repaired separately in #449; metadata changes are excluded from the upgrade diff.

Preserved mathematics and compatibility

The migration preserves the inspected projects' principal mathematical claims. This is a source/API preservation audit, not a kernel-checked equivalence comparison of every old and new declaration. The narrower auxiliary hypotheses below are explicit compatibility changes.

  • Local replacements for deprecated stdSimplex preserve (∀ i, 0 ≤ f i) ∧ ∑ i, f i = 1, the function-space subtype and topology, and existing helper/theorem names, including Brouwer compactness.
  • RiemannRochFunctionFields preserves finiteIdealWeight and infiniteIdealWeight as quotient dimensions for all ideals. Comparison lemmas connect them to modern inertia degrees at maximal ideals without changing principal-divisor claims.
  • Neukirch retains general quotient positivity as NumberField.quotient_finrank_pos_of_lies_over. The restored Ideal.quotient_finrank_algebra_tower_of_eq preserves the quotient-dimension tower law when the upstairs ideal is not prime; the modern inertia-degree theorem remains separately available. inertiaDeg_eq_of_isGalois derives downstairs maximality internally.
  • Incompleteness factors two identity-substitution proofs before instantiating large formulas, preventing excessive kernel expansion while preserving public statements, formula definitions, and computational fields.
  • SumDifferenceExponent retains the explicit 10⁻⁹⁹⁹ witness and the same enormous power-of-two index. A private powerOfTwo definition and generic lemmas prevent kernel conversion from evaluating that closed power; the witness is neither reduced nor replaced by an existential result.
  • MassFormula preserves every public statement while extracting generic algebra and valuation arguments to avoid default-heartbeat regressions; no limits or linter settings were raised.
  • PolynomialMethodRestrictedSums retains main's optimized proofs while adapting coefficient APIs. Its main ANR statement explicitly qualifies AddMonoidAlgebra.coeff for standalone minimal exports.
  • PDL retains all 1,998 explicit declaration commands and names. Its theorem statements and computational definitions are unchanged; six files adapt split imports, conversion proofs, and well-foundedness APIs. instIsWellFoundedSequentLt retains the same relation and witness while replacing the deprecated IsWellFounded wrapper with WellFounded.
  • Collision-driven renames retain the implementations: BruhatTits' Matrix.GeneralLinearGroup.smul_def becomes smul_submodule_def; SardMoreira's Submodule.prodEquiv becomes prodEquiv'. Mathlib now occupies the original names.
Auxiliary API Compatibility change
NavierStokesAndEuler: eLpNorm_localized_le, eLpNorm_le_rpow_mul Add AEStronglyMeasurable; modern eLpNorm assigns infinity without it.
ZhangYeungInequality: FiniteRange.null_of_compl, FiniteRange.ae_mem_toFinset Add AEMeasurable X μ; a nonmeasurable pushforward can now be an arbitrary Dirac measure outside the function's range.
SardMoreira: IsLocallyFiniteMeasure.prod; ZetaZeros: memLp_tensor_two Add SFinite for the second measure, matching the current product APIs. Existing applications provide it.
Neukirch: NumberField.inertiaDeg_pos Add upstairs maximality for modern Ideal.inertiaDeg, which is zero for nonprime ideals. General quotient positivity is retained separately.

Local finiteness alone does not imply SFinite. No concrete counterexample to unrestricted product local finiteness was established, and neither the product nor tensor helper's added assumption is claimed minimal.

Validation

Candidate: 20fb00c51334c79a2b75ed548dea093774ad62b0, incorporating main 2048b8ad557e3da77c826f876205d0d216069f77 and the merged metadata-only repair #449. Lean sources and build inputs are byte-identical to the fully checked b32aeac47 snapshot; the final merge changes only NOTICE and README. The final metadata receipt revalidates complete API coverage and source links, preserves all search/export outcomes, and refreshes exposition commit metadata without recompiling unchanged targets.

  • Full warning-free pool build: 12,408 jobs. Generated roots, environment/style linters for all three libraries, and Challenge/Solution warning gate pass.
  • Full repository quality audit passes with no skip flags. The pinned sandboxed comparator passes for every registered solved challenge, with actual default-kernel acceptance.
  • API documentation: all 6,688 current modules and 511,784 search entries are covered. Current source links and retained search/navigation/dependency data are verified. The same three prior declaration omissions remain, with none added. The 147 prior equation-display warning identities remain; PDL adds one warning for PDL.instDecidableEqPdlRule.decEq, which is still searchable.
  • Exposition: all 199 root sections, 198 registered projects, and 173,091 declarations are covered, including 2,088 PDL declarations and its three main results. Every old project payload is identical except commit metadata.
  • Minimal files: all 311 registered targets are accounted for: 269 pass, the same 40 prior failures remain, and both newly added PDL targets fail standalone export. The 309 retained results are reused only after exact source, dependency, verifier, and payload identity checks. PDL's failures arise when the unchanged exporter erases computational by definition bodies; both reproduce with the upstream rc1 compiler and matching Mathlib using reconstructed baseline skeletons, with the same 19 ordered error headlines per target. This is explicitly not an untouched baseline extraction/verifier run. These export failures do not affect the complete project build and remain disclosed as failures.
  • Independent source/API audits account for every incoming source and the explicit upstream retirements. These bounded checks do not claim universal kernel equivalence of old and new declarations.

Native Build project, Content / non-content separation, and Documentation preflight checks all pass on this exact candidate. The Lean CI run passes all ten build shards, the combined build, environment and text-style linters, and repository quality checks. Native challenge verification also passes. The optional native full-documentation jobs are still running; the complete local API/exposition checks above are separate from those jobs.

@Vilin97 Vilin97 changed the title chore: bump Lean and Mathlib to v4.34.0 Bump Lean and Mathlib to v4.34.0 Sep 15, 2026
@Vilin97
Vilin97 marked this pull request as ready for review September 15, 2026 21:34
@Vilin97

Vilin97 commented Sep 16, 2026

Copy link
Copy Markdown
Collaborator

@greptileai review this PR

@greptile-apps

greptile-apps Bot commented Sep 16, 2026

Copy link
Copy Markdown

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

Retrigger

The PR appears safe to merge based on the complete migration diff and the preserved contracts of the substantive repairs.

Summary

Upgrades the root and documentation workspaces from Lean/Mathlib v4.34.0-rc1 to v4.34.0 and updates the challenge exporter accordingly.

  • Migrates renamed, relocated, and signature-adjusted Mathlib APIs throughout the pool.
  • Reintroduces project-local function-valued simplex APIs where Mathlib now provides an incompatible bundled representation.
  • Preserves quotient-based ideal weights while adopting modern inertia-degree APIs at maximal ideals.
  • Adds required measurability and SFinite hypotheses where current measure semantics make the former unrestricted statements invalid.
  • Refactors two Incompleteness proofs to avoid excessive kernel expansion and explicitly qualifies the ANR coefficient operation for minimal exports.

Reviews (1) · Last reviewed commit: "Preserve coefficient references in minim..."

@Vilin97 Vilin97 added the needs-maintainer Actual human decision required: licensing, mathematical scope, policy, or reviewer disagreement. label Sep 16, 2026
@Vilin97

Vilin97 commented Sep 16, 2026

Copy link
Copy Markdown
Collaborator

Automated review disposition: needs-maintainer

Reviewed b78457bf01610d1d80228eae2da861bf2148c12c as the sanctioned toolchain/refactor migration, including the complete saved diff and focused examination of the simplex compatibility layer, quotient-based ideal weights, measure-API changes, Incompleteness proof factoring, challenge statement and exporter pin. No policy/gate weakening or challenge-statement change was found. Required checks passed; the ten shards and assembly passed. The optional documentation cancellation is not a required-check failure. Greptile's detailed review is favorable.

The substantive compatibility decision is explicit: public auxiliary APIs acquire measurability/SFinite assumptions, while changed Mathlib definitions require corresponding adapters. Existing local build, full quality/trust, documentation and minimal-export comparisons provide strong evidence, but accepting the narrowed auxiliary API surface across this 129-project migration is a maintainer judgment. Please confirm that compatibility boundary and obtain the unavailable configured exact-head LLM review before protected merge. The workflow remains manually disabled, the branch is now behind main, and normal auto-merge is disabled. No further broad architectural rewrite was attempted.

@Vilin97

Vilin97 commented Sep 17, 2026

Copy link
Copy Markdown
Collaborator

Automated cycle 2026-09-17: status update at b78457bf01610d1d80228eae2da861bf2148c12c

Two facts changed since the last disposition:

Repairing this PR means re-running the probe/repair stages over the newly merged projects, which is a full bump cycle rather than a safe cycle repair, and .github/BUMP_AUTOMATION.md reserves the bump merge for a human. The decision is whether to close this PR in favour of #442 or to land v4.34.0 first. Retaining needs-maintainer.

@Vilin97

Vilin97 commented Sep 17, 2026

Copy link
Copy Markdown
Collaborator

/profile

@greptile-apps

greptile-apps Bot commented Sep 17, 2026

Copy link
Copy Markdown

PR author is in the excluded authors list.

@github-actions

github-actions Bot commented Sep 18, 2026

Copy link
Copy Markdown
Contributor Author

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 8608.58 s (= 143.48 min) — user 31527.43 s, sys 2283.49 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

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

⚠️ Statements changed (106)
  • Filter.eventuallyEq_set' — LeanPool/AFormalizationOfBorelDeterminacyInLean/Applications/General.lean
  • TT.CoestdSimplex — LeanPool/Brouwer/Brouwer.lean
  • TTtostdSimplex — LeanPool/Brouwer/Brouwer.lean
  • dominant_coords_tend_to_zero — LeanPool/Brouwer/Brouwer.lean
  • f_coords_ge_z_coords — LeanPool/Brouwer/Brouwer.lean
  • hpkgAux — LeanPool/Brouwer/Brouwer.lean
  • stdSimplex.pick — LeanPool/Brouwer/Brouwer.lean
  • stdSimplex.upidx — LeanPool/Brouwer/Brouwer.lean
  • tendsto_diam_to_zero — LeanPool/Brouwer/Brouwer.lean
  • mapMixedSEquiv — LeanPool/Brouwer/Nash.lean
  • mapSimplex — LeanPool/Brouwer/Nash.lean
  • mapSimplexEquiv — LeanPool/Brouwer/Nash.lean
  • map_simplex_apply — LeanPool/Brouwer/Nash.lean
  • reindex — LeanPool/Brouwer/Nash.lean
  • reindexInv — LeanPool/Brouwer/Nash.lean
  • reindex_left_inv — LeanPool/Brouwer/Nash.lean
  • stdSimplex.SInhabitedOfInhabited — LeanPool/Brouwer/Simplex.lean
  • stdSimplex.SNonempty_of_Inhabited — LeanPool/Brouwer/Simplex.lean
  • stdSimplex.funlike — LeanPool/Brouwer/Simplex.lean
  • stdSimplex.funlike_eval1 — LeanPool/Brouwer/Simplex.lean
  • stdSimplex.funlike_eval2 — LeanPool/Brouwer/Simplex.lean
  • stdSimplex.pure — LeanPool/Brouwer/Simplex.lean
  • stdSimplex.wsum_magic_ineq — LeanPool/Brouwer/Simplex.lean
  • PowerSeries.deriv_logOf_mul — LeanPool/ConnesKreimer/PowerSeriesLogMul.lean
  • PowerSeries.deriv_log_subst_mul — LeanPool/ConnesKreimer/PowerSeriesLogMul.lean
  • PowerSeries.one_add_X_mul_deriv_log — LeanPool/ConnesKreimer/PowerSeriesLogMul.lean
  • isTors' — LeanPool/FltRegular/NumberTheory/Hilbert92.lean
  • relativeUnitsMap_addMonoidEndRingEquivInt_apply — LeanPool/FltRegular/NumberTheory/Hilbert92.lean
  • chain_isCompatible_of_chain — LeanPool/GrothendieckVanishing/FlasqueVanishing.lean
  • exists_glued_lift_upper_bound — LeanPool/GrothendieckVanishing/FlasqueVanishing.lean
  • underMk — LeanPool/GrothendieckVanishing/FlasqueVanishing.lean
  • under_extend_by_one_open — LeanPool/GrothendieckVanishing/FlasqueVanishing.lean
  • FirstOrder.Combinatorics.EndHomogER.nodeChosen_eq_min — LeanPool/InfinitaryLogic/Combinatorics/EndHomogeneousErdosRado.lean
  • FirstOrder.Combinatorics.PairERGen.ehmrChosen_eq_min — LeanPool/InfinitaryLogic/Combinatorics/PairErdosRadoGeneral.lean
  • KoetheMultiProjective.coeff_balancedPart — LeanPool/Koethe/MultiProjective.lean
  • KoetheMultiProjective.exists_common_zero_of_coeff — LeanPool/Koethe/MultiProjective.lean
  • mvpoly_support_after_reduction — LeanPool/LeanModularForms/Modularforms/Generators/Injectivity.lean
  • whomog_unique_monomial — LeanPool/LeanModularForms/Modularforms/Generators/Injectivity.lean
  • MetricCodes.Spherical.HigherHarmonicYoung.ArbitraryRankMixedTraceRegularity.coeff_gramPairPolynomial_pivot — LeanPool/MetricCodes/Branching.lean
  • SpherePacking.Fischer.coeff_pderiv — LeanPool/MetricCodes/HarmonicAnalysis.lean
  • SpherePacking.Fischer.coefficientEmbedding_apply — LeanPool/MetricCodes/HarmonicAnalysis.lean
  • SpherePacking.Fischer.harmonicCoefficientEmbedding_apply — LeanPool/MetricCodes/HarmonicAnalysis.lean
  • SpherePacking.Fischer.harmonicInner_eq_sum — LeanPool/MetricCodes/HarmonicAnalysis.lean
  • SpherePacking.Fischer.homogeneousInner_eq_sum — LeanPool/MetricCodes/HarmonicAnalysis.lean
  • SpherePacking.Fischer.polynomialInner_monomial — LeanPool/MetricCodes/HarmonicAnalysis.lean
  • MetricCodes.Spherical.OrthogonalPolynomialTransport.coeff_zero_polynomialMap — LeanPool/MetricCodes/Representation.lean
  • MetricCodes.Spherical.HigherHarmonicYoung.UniversalBGGRootComplex.rootAction_X_coefficient — LeanPool/MetricCodes/RootComplex.lean
  • MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.coeff_ambientBinomialPolynomial_mul_gramEquationPolynomial — LeanPool/MetricCodes/Weyl.lean
  • MetricCodes.Spherical.HigherWeylGramAlternantCoefficient.coeff_ambientBinomialPolynomial_of_le — LeanPool/MetricCodes/Weyl.lean
  • MetricCodes.Spherical.HigherWeylReversedAlternantCoefficient.coeff_ambient_mul_gram_mul_reversedWeylPolynomial — LeanPool/MetricCodes/Weyl.lean
  • … +56 more

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

➕ Declarations added (38)
  • BollobasNikiforov.isClosed_stdSimplex — LeanPool/BollobasNikiforov/MS/Basic.lean
  • BollobasNikiforov.isCompact_stdSimplex — LeanPool/BollobasNikiforov/MS/Basic.lean
  • BollobasNikiforov.single_mem_stdSimplex — LeanPool/BollobasNikiforov/MS/Basic.lean
  • BollobasNikiforov.stdSimplex — LeanPool/BollobasNikiforov/MS/Basic.lean
  • BollobasNikiforov.stdSimplex_subset_Icc — LeanPool/BollobasNikiforov/MS/Basic.lean
  • Brouwer.isCompact_standardSimplex — LeanPool/Brouwer/Simplex.lean
  • Brouwer.standardSimplex — LeanPool/Brouwer/Simplex.lean
  • Matrix.GeneralLinearGroup.smul_submodule_def — LeanPool/BruhatTits/Utils/Matrix.lean
  • LeanEval.Topology.ClassificationOfSurfaces.convex_stdSimplex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.isClosed_stdSimplex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.isCompact_stdSimplex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.mem_Icc_of_mem_stdSimplex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.single_mem_stdSimplex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.add_eq_one — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.continuous_map — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.ext — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.image_linearMap — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.instCompactSpace_coe — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.le_one — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.map — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.map_coe — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.map_comp_apply — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.map_id_apply — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.map_vertex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.sum_eq_one — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.vertex — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.vertex_coe — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.vertex_injective — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex.zero_le — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex_eq_inter — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LeanEval.Topology.ClassificationOfSurfaces.stdSimplex_subset_Icc — LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean
  • LO.Arith.predicate_defined_identity_substitution — LeanPool/Incompleteness/Arith/Theory.lean
  • LO.Arith.Substs.defined_identity_substitution — LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Functions.lean
  • NumberField.quotient_finrank_pos_of_lies_over — LeanPool/Neukirch/HilbertRamificationTheory.lean
  • FunctionField.Chart.finiteIdealWeight_eq_inertiaDeg — LeanPool/RiemannRochFunctionFields/FunctionField/Divisor.lean
  • FunctionField.Chart.infiniteIdealWeight_eq_inertiaDeg — LeanPool/RiemannRochFunctionFields/FunctionField/Divisor.lean
  • Submodule.prodEquiv' — LeanPool/SardMoreira/Unused.lean
➖ Declarations removed (2)
  • Matrix.GeneralLinearGroup.smul_def — LeanPool/BruhatTits/Utils/Matrix.lean
  • Submodule.prodEquiv — LeanPool/SardMoreira/Unused.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: 1,765,662 maxHeartbeats units across 621 files (2,828 added LOC).

Sum of lean --profile: 7936039.9 ms (= 7936.04 s). Import-excluded time: 7152689.9 ms (= 7152.69 s).

Count-heartbeats wall-clock total: 7755.22 s. Repeated import cost inside lean --profile: 783350.0 ms (= 783.35 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/NavierStokesAndEuler/Euler/SourceCylinderPressureField.lean 2 348,981 78.74 61.71 60.55 1.16 39 0
LeanPool/BrauerGroupNew/IsoSecond.lean 11 248,157 77.99 54.44 52.10 2.34 62 16
LeanPool/NavierStokesAndEuler/Euler/ParentState.lean 7 78,601 37.02 30.17 28.90 1.27 78 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/SchurMul.lean 29 69,113 31.81 23.82 22.37 1.45 26 0
LeanPool/Neukirch/HilbertRamificationTheory.lean 39 63,837 33.14 22.70 21.29 1.41 139 0
LeanPool/NavierStokesAndEuler/Euler/TransverseForwardCoefficientGevrey.lean 2 59,234 20.47 12.45 11.31 1.14 16 0
LeanPool/MRiscX/Examples/Examples.lean 1 51,184 14.68 5.28 4.21 1.07 10 0
LeanPool/JacobianDiffgeo/Finiteness/Chain.lean 1 39,359 19.77 11.58 10.06 1.52 36 0
LeanPool/BrauerGroupNew/DoubleCentralizer.lean 4 38,344 27.98 29.35 27.68 1.67 22 0
LeanPool/ZhangYeungInequality/Test/Theorem5.lean 1 31,401 9.10 3.33 1.80 1.53 5 0
LeanPool/DirectedTopologyLean4/DirectedVanKampen.lean 11 28,821 12.33 12.10 11.00 1.10 68 0
LeanPool/SpherePacking/PackingBound.lean 3 28,341 48.65 62.38 61.13 1.25 249 0
LeanPool/Monlib4/QuantumGraph/PiMatFinTwo.lean 9 27,629 66.34 60.28 58.72 1.56 54 0
LeanPool/BrauerGroupNew/Morita/TensorProduct.lean 2 23,271 13.77 9.20 7.88 1.32 45 0
LeanPool/ClassificationOfSurfaces/Moise/ChartInduction.lean 2 22,337 51.00 60.09 58.50 1.59 173 0
LeanPool/BrauerGroupNew/AlgClosedUnion.lean 3 21,212 20.56 17.69 16.47 1.22 29 0
LeanPool/RiemannRochFunctionFields/Place.lean 5 18,494 20.81 10.78 9.63 1.15 54 0
LeanPool/WhiteheadTheorem/CWComplex/IProd/Def.lean 12 17,380 16.51 20.17 18.75 1.42 31 0
LeanPool/NavierStokesAndEuler/Euler/BaseEulerState.lean 2 16,788 42.83 49.98 48.60 1.38 372 0
LeanPool/BrauerGroupNew/Azumaya/Mul.lean 1 15,849 21.81 18.88 17.26 1.62 71 0
LeanPool/NavierStokesAndEuler/Euler/LpCylinderRegularCoefficient.lean 1 14,884 10.60 6.34 5.22 1.12 10 0
LeanPool/NavierStokesAndEuler/Euler/CylinderDirichletSobolev.lean 1 14,163 26.97 15.14 14.03 1.11 31 0
LeanPool/Monlib4/LinearAlgebra/LmulRmul.lean 1 12,183 5.90 3.57 2.59 0.97 31 0
LeanPool/RlTheoryInLean/Data/Matrix/Stochastic.lean 7 11,115 8.21 9.04 7.64 1.40 45 0
LeanPool/BruhatTits/Lattice/Basic.lean 2 10,655 8.11 5.71 4.33 1.38 29 0
LeanPool/InfiniteConnesRigidity/CarryAndCrossedProduct.lean 3 10,432 114.72 111.28 110.02 1.26 602 10
LeanPool/InfiniteConnesRigidity/SpectralAndPropertyT.lean 13 10,356 65.64 89.55 88.24 1.31 416 0
LeanPool/LowDimSolvClassification/Semidirect.lean 1 10,179 8.53 3.83 2.71 1.12 45 0
LeanPool/NavierStokesAndEuler/Euler/CoefficientPathSmooth.lean 1 8,702 12.75 7.58 6.47 1.11 12 0
LeanPool/FltRegular/NumberTheory/Hilbert92.lean 4 8,124 20.55 24.00 22.46 1.54 42 4
LeanPool/OSforGFF/GaussianField/Nuclear/NuclearTensorProduct.lean 1 7,828 16.19 12.43 11.10 1.33 78 0
LeanPool/Monlib4/LinearAlgebra/OfNorm.lean 1 7,595 9.52 9.16 7.75 1.41 56 0
LeanPool/InfiniteConnesRigidity/FactorAndRigidity.lean 1 7,389 61.59 60.78 59.41 1.37 357 0
LeanPool/BrauerGroupNew/SkolemNoether.lean 5 7,278 11.15 6.10 4.45 1.65 22 0
LeanPool/BruhatTits/Graph/Regular.lean 1 7,217 7.62 4.66 3.25 1.41 28 0
LeanPool/NonSoficGroup/Spectral.lean 2 7,085 49.29 75.84 74.51 1.33 480 0
LeanPool/AharoniKorman/Counterexample.lean 1 6,853 12.99 16.18 15.34 0.84 101 0
LeanPool/NavierStokesAndEuler/Euler/PhysicalGraphFlowBounds.lean 2 6,336 28.16 32.42 31.20 1.22 88 0
LeanPool/Monlib4/LinearAlgebra/Ips/Pos.lean 3 6,120 9.91 8.80 7.38 1.42 40 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/RellichKondrachovRiemannian/Chartwise.lean 2 5,902 29.61 25.44 23.89 1.55 11 0
LeanPool/MetricCodes/Representation.lean 14 5,415 63.51 70.37 68.81 1.56 578 0
LeanPool/MetricCodes/Branching.lean 16 5,296 64.68 70.28 68.69 1.59 332 0
LeanPool/MisereGames/Mathlib/NatOrdinal.lean 1 5,213 7.73 4.80 4.18 0.62 122 0
LeanPool/NavierStokesAndEuler/Euler/PhysicalGraphGevrey.lean 2 5,164 6.13 3.87 2.66 1.21 13 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Functions.lean 18 5,081 9.16 15.01 14.18 0.83 132 0
LeanPool/RiemannRochFunctionFields/EllipticCurve/Infinity.lean 8 4,785 15.28 13.87 12.69 1.18 11 0
LeanPool/ConnesRigidity/Foundation/OperatorAlgebra/PositiveSpectralMeasure.lean 8 4,733 21.63 30.18 28.61 1.57 97 0
LeanPool/RiemannRochFunctionFields/EllipticCurve/Instances.lean 1 4,673 12.11 6.69 5.53 1.16 19 0
LeanPool/BruhatTits/Utils/Matrix.lean 4 4,646 10.20 12.47 11.11 1.36 64 0
LeanPool/NavierStokesAndEuler/Euler/MeanGradientTestSpace.lean 1 4,353 6.24 4.32 3.22 1.10 18 0
LeanPool/OSforGFF/Minlos/MeasurableModification.lean 3 4,310 9.85 14.21 12.54 1.67 21 0
LeanPool/Monlib4/LinearAlgebra/Coalgebra/FiniteDimensional.lean 1 4,211 13.54 10.45 9.00 1.45 20 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/TensorProduct.lean 9 4,201 10.56 7.18 5.74 1.44 15 0
LeanPool/BrauerGroupNew/BrauerGroup.lean 12 4,158 18.41 14.24 12.68 1.56 70 0
LeanPool/NavierStokesAndEuler/NavierStokes/CurlClassBounds.lean 1 4,153 27.55 35.28 34.16 1.12 214 0
LeanPool/Incompleteness/Arithmetization/Basic/IOpen.lean 1 3,637 6.82 12.72 11.90 0.82 185 0
LeanPool/InfiniteConnesRigidity/GroupConstruction.lean 4 3,637 55.44 71.39 70.06 1.33 495 4
LeanPool/NavierStokesAndEuler/Euler/LinearDuhamel.lean 3 3,327 6.33 4.90 3.79 1.11 13 0
LeanPool/OSforGFF/Minlos/ProjectiveFamily.lean 5 3,268 7.09 3.38 1.75 1.63 16 0
LeanPool/Monlib4/LinearAlgebra/Ips/TensorHilbert.lean 0 3,260 6.59 4.10 2.66 1.44 19 0
LeanPool/BruhatTits/Lattice/Construction.lean 1 3,104 8.68 10.49 9.11 1.38 72 0
LeanPool/OSforGFF/General/FunctionalAnalysis.lean 4 3,092 11.13 10.63 9.05 1.58 39 0
LeanPool/BruhatTits/Graph/GroupAction.lean 0 3,012 8.59 9.51 8.03 1.48 17 0
LeanPool/NavierStokesAndEuler/Euler/InitialH1OperatorProduct.lean 1 2,906 5.28 3.53 2.42 1.11 5 0
LeanPool/RiemannRochFunctionFields/FunctionField/Divisor.lean 40 2,850 28.30 47.41 46.23 1.18 19 0
LeanPool/BollobasNikiforov/M/Schur.lean 1 2,789 16.88 24.76 23.31 1.45 168 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/QIso.lean 4 2,782 43.85 41.90 40.46 1.44 31 4
LeanPool/SardMoreira/ContDiff.lean 2 2,737 6.10 5.30 3.97 1.33 23 0
LeanPool/QuantumParallelRepetition/Part01.lean 3 2,639 32.15 43.47 41.95 1.52 342 0
LeanPool/BrauerGroupNew/BrauerOverR.lean 6 2,616 8.34 6.42 4.67 1.75 15 0
LeanPool/BruhatTits/Harmonic/Basic.lean 21 2,593 6.06 5.29 4.12 1.17 31 0
LeanPool/LeanModularForms/HeckeRIngs/AbstractHeckeRing/Basic.lean 1 2,496 5.67 3.94 2.80 1.14 50 0
LeanPool/NavierStokesAndEuler/NavierStokes/RadialPullback.lean 1 2,422 13.37 16.51 15.42 1.09 152 0
LeanPool/EhrhartVolumeInequality/Foundations.lean 1 2,420 30.79 40.69 39.53 1.16 499 0
LeanPool/NavierStokesAndEuler/Euler/CylinderPhysicalTensorLp.lean 8 2,400 5.38 3.17 2.08 1.09 3 0
LeanPool/PFR/RhoFunctional.lean 17 2,302 35.02 42.37 41.19 1.18 64 0
LeanPool/NavierStokesAndEuler/NavierStokes/PrimaryPulseBounds.lean 1 2,301 17.46 19.42 18.29 1.13 106 0
LeanPool/CompactnessAndDegeneracy/Compactness.lean 3 2,286 43.35 55.04 54.00 1.04 464 0
LeanPool/ClassificationOfSurfaces/Moise/GraphPolygonalization.lean 13 2,277 25.66 27.68 26.31 1.37 147 0
LeanPool/EhrhartVolumeInequality/Variation.lean 1 2,260 36.62 49.61 48.36 1.25 440 5
LeanPool/RamanujanTauMissesPrimes/Solution.lean 2 2,243 28.81 52.35 51.03 1.32 526 0
LeanPool/MetricCodes/HarmonicAnalysis.lean 57 2,238 92.33 93.30 91.77 1.53 558 0
LeanPool/MisereGames/Form.lean 4 2,230 8.94 5.16 4.60 0.55 130 0
LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean 1 2,218 10.88 11.50 10.06 1.44 73 0
LeanPool/NavierStokesAndEuler/NavierStokes/ActualCandidateAssembly.lean 0 2,192 16.45 17.18 15.93 1.25 316 0
LeanPool/GapCVP/Part01A.lean 1 2,187 17.93 24.71 23.22 1.49 498 0
LeanPool/NavierStokesAndEuler/NavierStokes/ConstructedSlowBase.lean 0 2,147 14.31 15.71 14.54 1.17 217 0
LeanPool/EhrhartVolumeInequality/FourierAnalysis.lean 2 2,107 39.94 50.85 49.64 1.21 431 0
LeanPool/PermanentFormulaLowerBound.lean 23 2,100 52.51 56.46 55.46 1.00 367 0
LeanPool/VirasoroProject/LieVerma.lean 1 2,086 8.07 2.86 1.80 1.06 21 0
LeanPool/DemazureOperatorsLean/Demazure.lean 6 2,024 4.90 4.57 3.08 1.49 43 0
LeanPool/MetricCodes/Weyl.lean 54 2,006 74.10 108.85 107.26 1.59 324 6
LeanPool/EhrhartVolumeInequality/Regularization.lean 3 1,957 54.40 58.90 57.70 1.20 425 0
LeanPool/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/L2Compactness/Approximation.lean 1 1,934 10.67 5.97 4.46 1.51 17 0
LeanPool/ZFLean/Naturals.lean 2 1,925 4.64 4.61 3.84 0.76 225 0
LeanPool/Duality/LinearProgramming.lean 0 1,875 16.38 15.94 14.83 1.11 50 0
LeanPool/ClassificationOfSurfaces/Moise/GeometricTriangulation.lean 177 1,784 5.55 4.55 3.51 1.04 79 0
LeanPool/NavierStokesAndEuler/Euler/LpCylinderRectangularRegularity.lean 1 1,779 13.00 13.20 12.08 1.12 18 0
LeanPool/SetTheory/Ordinals.lean 9 1,758 4.50 3.59 2.45 1.14 39 0
LeanPool/SpherePacking/Foundations.lean 4 1,708 45.65 57.50 56.30 1.20 424 0
LeanPool/MetricCodes/Hierarchy.lean 8 1,702 44.48 56.89 55.35 1.54 409 0
LeanPool/MetricCodes/Rigidity.lean 4 1,681 81.96 115.91 114.29 1.62 312 10
LeanPool/ZhangYeungInequality/PFR/ForMathlib/Entropy/Basic.lean 2 1,678 7.80 11.12 9.99 1.13 97 0
LeanPool/MetricCodes/Interlacing.lean 5 1,675 64.75 67.30 65.71 1.59 405 0
LeanPool/Monlib4/LinearAlgebra/InvariantSubmodule.lean 1 1,655 5.25 2.63 1.64 0.99 18 0
LeanPool/OSforGFF/Minlos/MinlosConcentration.lean 5 1,650 21.27 34.03 32.38 1.65 10 0
LeanPool/CompactnessAndDegeneracy/Degeneracy.lean 4 1,612 40.20 60.27 59.09 1.18 403 0
LeanPool/NavierStokesAndEuler/NavierStokes/ParametricODE.lean 1 1,612 13.68 10.87 9.73 1.14 41 0
LeanPool/QuasiBorelSpaces/MeasureTheory/Randomization.lean 3 1,586 8.95 3.82 2.39 1.43 24 0
LeanPool/PFR/MoreRuzsaDist.lean 4 1,564 36.93 70.69 69.56 1.13 55 0
LeanPool/RiemannRochFunctionFields/Genus/Ramification.lean 3 1,564 14.51 10.44 9.27 1.17 8 0
LeanPool/ClassificationOfSurfaces/DiskSquare.lean 1 1,535 17.95 25.47 23.34 2.13 221 0
LeanPool/ClassificationOfSurfaces/Moise/IntrinsicFaceExtension.lean 1 1,508 8.40 5.85 4.47 1.38 52 0
LeanPool/LeanModularForms/HeckeRIngs/AbstractHeckeRing/Multiplication.lean 1 1,495 5.77 6.49 5.34 1.15 39 0
LeanPool/Monlib4/QuantumGraph/Basic.lean 1 1,383 42.54 40.02 38.46 1.56 88 0
LeanPool/SpherePacking/MellinAnalysis.lean 1 1,324 43.36 55.10 53.87 1.23 331 0
LeanPool/PointwiseBirkhoff/Main.lean 3 1,321 6.65 4.46 2.97 1.49 31 0
LeanPool/MetricCodes/HighestWeights.lean 13 1,312 62.04 69.63 68.04 1.59 328 0
LeanPool/InfinitaryLogic/ModelTheory/HanfSpectrum/LadderSyntax.lean 2 1,307 3.03 1.79 0.98 0.81 26 0
LeanPool/BollobasNikiforov/M/Elim.lean 2 1,302 11.37 13.67 12.14 1.53 189 0
LeanPool/MetricCodes/RootComplex.lean 33 1,294 35.99 41.62 40.05 1.57 322 0
LeanPool/SpherePacking/SaddleAnalysis.lean 1 1,290 31.87 40.87 39.68 1.19 285 0
LeanPool/LongGapsBetweenPrimes/Main.lean 9 1,283 37.86 67.85 66.33 1.52 320 0
LeanPool/NavierStokesAndEuler/ForMathlib/SmoothCutoff.lean 1 1,283 5.95 2.95 1.89 1.06 37 0
LeanPool/NavierStokesAndEuler/NavierStokes/PulseAmplitude.lean 1 1,272 24.47 37.88 36.77 1.11 318 0
LeanPool/OSforGFF/General/SchwartzTranslationDecay.lean 1 1,254 9.73 14.07 12.54 1.53 11 0
LeanPool/Monlib4/QuantumGraph/ToProjections.lean 1 1,233 23.56 27.69 26.12 1.57 50 0
LeanPool/JacobianDiffgeo/Surface/Identity.lean 1 1,214 5.99 2.68 1.20 1.48 9 0
LeanPool/PFR/ForMathlib/Entropy/RuzsaDist.lean 16 1,186 13.69 24.34 23.19 1.15 49 0
LeanPool/QuadraticIterates/Mathlib/FieldTheory/Multiquadratic.lean 2 1,185 9.69 14.32 13.13 1.19 46 0
LeanPool/NavierStokesAndEuler/Euler/LpCylinderCoefficients.lean 1 1,161 27.54 22.22 21.06 1.16 14 0
LeanPool/PFR/AddCombi/BSG.lean 1 1,159 9.89 18.00 17.01 0.99 27 0
LeanPool/NavierStokesAndEuler/Euler/TransversePacketHistoryPressure.lean 2 1,140 9.12 8.57 7.37 1.20 20 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean 13 1,132 58.21 101.07 99.45 1.62 283 0
LeanPool/NavierStokesAndEuler/Euler/SmoothL2Series.lean 1 1,125 7.26 6.66 5.43 1.23 23 0
LeanPool/OSforGFF/Covariance/Momentum.lean 2 1,111 21.36 23.57 22.03 1.54 85 0
LeanPool/Incompleteness/Arith/Theory.lean 15 1,106 7.73 6.36 5.52 0.84 37 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean 3 1,097 26.52 29.52 28.06 1.46 77 0
LeanPool/PFR/WeakPFR.lean 4 1,068 18.99 23.59 22.47 1.12 22 0
LeanPool/OSforGFF/Measure/Minlos.lean 1 1,053 4.83 3.53 1.87 1.66 12 0
LeanPool/MetricCodes/Rates.lean 5 1,044 84.07 78.79 77.26 1.53 252 0
LeanPool/MetricCodes/Conclusion.lean 10 1,024 139.60 180.55 178.95 1.60 256 8
LeanPool/VirasoroProject/WittAlgebraCohomology.lean 1 1,008 7.31 4.74 3.52 1.22 9 0
LeanPool/PFR/AddCombi/Convolution/Finite/Defs.lean 2 1,005 6.02 3.98 2.99 0.99 22 0
LeanPool/NavierStokesAndEuler/Euler/SmoothTimeFieldComposition.lean 1 979 9.65 6.48 5.33 1.15 36 0
LeanPool/ClassificationOfSurfaces/Moise/PolygonalArc.lean 3 910 13.31 15.31 13.94 1.37 137 0
LeanPool/ArtinWedderburn/CornerRing.lean 1 894 6.87 4.05 2.99 1.06 50 0
LeanPool/ZhangYeungInequality/PFR/Mathlib/Probability/Kernel/Disintegration.lean 1 859 6.72 8.14 7.06 1.08 63 0
LeanPool/ZetaZeros/Hilbert/AlphaExpansion.lean 6 827 18.73 24.26 22.76 1.50 96 0
LeanPool/Monlib4/QuantumGraph/QamA.lean 1 822 30.04 39.32 37.74 1.58 39 4
LeanPool/NavierStokesAndEuler/Euler/Foundations/SmoothSobolev.lean 18 798 16.31 19.88 18.73 1.15 21 0
LeanPool/Monlib4/QuantumGraph/Iso.lean 8 795 17.46 24.89 23.33 1.56 22 0
LeanPool/QuasiBorelSpaces/PreProbabilityMeasure.lean 4 794 4.47 3.89 2.45 1.44 63 0
LeanPool/SpherePacking/HarmonicAnalysis.lean 2 793 44.74 63.48 62.26 1.22 196 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/CylinderSobolev.lean 4 790 6.85 6.30 5.18 1.12 49 0
LeanPool/ZhangYeungInequality/Theorem2.lean 2 782 12.54 17.32 15.80 1.52 34 0
LeanPool/NavierStokesAndEuler/Euler/FiniteGradeAlgebra.lean 1 780 3.11 1.47 0.85 0.62 10 0
LeanPool/Sundogcert/VarWheel.lean 1 773 4.08 1.10 0.36 0.74 11 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean 35 764 55.10 102.23 100.59 1.64 191 0
LeanPool/NavierStokesAndEuler/NavierStokes/R3/PressureFlux.lean 36 761 26.25 38.59 37.44 1.15 188 0
LeanPool/NavierStokesAndEuler/Euler/MeanPacketForcing.lean 1 752 16.74 22.73 21.56 1.17 40 0
LeanPool/HansonWright/Probability/Concentration/HansonWright.lean 7 746 26.49 52.39 50.79 1.60 146 0
LeanPool/ClassificationOfSurfaces/FiniteCyclicP2Realization.lean 3 743 9.20 7.71 6.16 1.55 185 0
LeanPool/FactorizationSystems/Orthogonality.lean 1 726 2.93 2.89 1.99 0.89 47 0
LeanPool/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateL2.lean 14 725 7.49 3.79 2.37 1.42 10 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean 1 724 50.56 63.59 62.00 1.59 181 0
LeanPool/NavierStokesAndEuler/Euler/GevreyGeneratingDerivatives.lean 1 720 5.74 5.51 4.36 1.15 36 0
LeanPool/NavierStokesAndEuler/NavierStokes/TangentODE.lean 1 714 12.17 7.07 5.99 1.08 25 0
LeanPool/ZhangYeungInequality/PFR/ForMathlib/Entropy/Measure.lean 15 691 9.78 13.60 12.46 1.14 54 0
LeanPool/Brouwer/Brouwer.lean 49 681 5.83 6.67 5.35 1.32 28 0
LeanPool/NavierStokesAndEuler/NavierStokes/EdgeWeightJets.lean 2 676 8.17 5.77 4.78 1.00 39 0
LeanPool/Chudnovsky/DivisionValues.lean 5 666 25.94 36.30 34.37 1.93 139 0
LeanPool/PLAcceleratedNesterovLean/MorseBott/TubularProjection/IFT.lean 1 656 9.85 12.20 10.81 1.39 8 0
LeanPool/SetTheory/KunenInconsistency.lean 5 650 6.06 5.02 3.85 1.17 55 0
LeanPool/Monlib4/LinearAlgebra/MyBimodule.lean 2 644 4.47 3.85 2.80 1.05 43 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Applications/Meager.lean 1 635 5.80 5.99 4.92 1.07 57 0
LeanPool/GrothendieckVanishing/PresheafFilteredColimit.lean 2 628 70.88 51.83 50.58 1.25 17 0
LeanPool/BrauerGroupNew/Azumaya/Basic.lean 1 626 8.95 7.36 5.64 1.72 19 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/BasicLemmas.lean 1 619 3.82 3.22 2.25 0.97 24 0
LeanPool/LocalComplexGeometry/ClassicalComplexWPT/WeightedSeries.lean 1 608 18.72 14.00 12.76 1.24 44 0
LeanPool/BollobasNikiforov/TN/Truncated.lean 2 603 11.70 14.81 13.60 1.21 113 0
LeanPool/Koethe/MultiProjective.lean 22 587 7.09 6.50 5.10 1.40 85 0
LeanPool/NavierStokesAndEuler/Euler/WholeSpaceGaussianFields.lean 1 587 7.38 5.38 4.24 1.14 18 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/SpatialSobolevInverse.lean 6 579 17.94 17.68 16.55 1.13 41 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/FiniteDimensional.lean 4 573 7.86 5.46 4.07 1.39 8 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/Sobolev.lean 3 570 10.91 7.14 5.96 1.18 15 0
LeanPool/NavierStokesAndEuler/Euler/OrdinarySmoothWords.lean 1 566 4.31 2.96 1.76 1.20 20 0
LeanPool/ComputableReal/ComputableRSeq.lean 1 559 27.46 32.95 32.09 0.87 133 0
LeanPool/SardMoreira/MainTheorem.lean 1 557 13.23 20.04 18.58 1.46 20 0
LeanPool/CutAndProject/Basic.lean 1 556 14.43 21.58 20.41 1.17 139 0
LeanPool/SemicircleLaw/SemicircleDistribution.lean 2 556 7.96 9.94 8.42 1.52 78 0
LeanPool/ClassificationOfSurfaces/Moise/IntrinsicGraphModel.lean 1 555 4.16 2.47 1.06 1.41 20 0
LeanPool/MisereGames/Ruleset/Hackenbush.lean 0 545 6.21 3.91 3.22 0.70 54 0
LeanPool/SardMoreira/Unused.lean 10 545 4.35 2.42 1.08 1.34 17 0
LeanPool/NavierStokesAndEuler/Euler/GevreyCorrectionForcing.lean 3 542 17.11 22.13 20.98 1.15 37 0
LeanPool/NavierStokesAndEuler/Euler/GevreyInverseMap.lean 1 541 5.82 4.75 3.79 0.96 25 0
LeanPool/QuantumParallelRepetition/Part10.lean 2 535 27.31 35.80 34.22 1.58 115 0
LeanPool/Vlasov/OT/Wasserstein.lean 1 533 9.24 4.95 3.57 1.38 29 0
LeanPool/Odlyzko/ExplicitFormula/RegularizedPoitouContourLimit.lean 1 530 20.67 34.86 33.52 1.34 101 0
LeanPool/Monlib4/LinearAlgebra/PiStarOrderedRing.lean 1 526 3.40 1.36 0.52 0.84 10 0
LeanPool/Monsky/SegmentTriangle.lean 6 516 25.21 37.67 36.32 1.35 129 0
LeanPool/LeanModularForms/Modularforms/QExpansionLems.lean 1 515 4.14 2.59 1.41 1.18 15 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Auxiliary.lean 15 507 11.56 10.60 8.97 1.63 44 0
LeanPool/FiniteGraphFundamentalGroup/TopologicalComparison.lean 26 504 5.08 6.38 5.17 1.21 93 0
LeanPool/RiemannMappingTheorem/ToMathlib.lean 1 497 4.17 3.54 2.09 1.45 21 0
LeanPool/JacobianDiffgeo/Surface/InverseFunction.lean 1 486 3.65 2.40 1.08 1.32 3 0
LeanPool/QuadraticIterates/Mathlib/RingTheory/MoebiusFactor.lean 1 483 4.86 4.04 3.04 1.00 13 0
LeanPool/ConcentrationInequalities/FreedmanBernstein.lean 16 468 5.23 4.09 2.43 1.66 25 0
LeanPool/NavierStokesAndEuler/Euler/OrdinaryWordBounds.lean 2 456 4.34 3.18 1.99 1.19 12 0
LeanPool/ClassificationOfSurfaces/Moise/PolygonalSchoenflies.lean 9 446 11.38 13.88 12.52 1.36 67 0
LeanPool/EhrhartVolumeInequality/Convergence.lean 1 444 8.53 11.00 9.55 1.45 46 0
LeanPool/Turan3/Turans3rdProof.lean 10 444 17.64 16.85 15.62 1.23 47 0
LeanPool/BruhatTits/Utils/RingHom.lean 0 441 3.90 2.29 1.18 1.11 18 0
LeanPool/DomainTheory/Neighborhood/Exercise222.lean 3 438 2.98 1.52 0.80 0.72 20 0
LeanPool/ZhangYeungInequality/PFR/Mathlib/Probability/IdentDistrib.lean 1 436 3.85 3.18 2.10 1.08 23 0
LeanPool/NavierStokesAndEuler/NavierStokes/AxisCoefficientSpace.lean 1 432 10.74 8.62 7.48 1.14 105 0
LeanPool/ABCExceptions/Section2.lean 8 430 18.79 25.49 24.30 1.19 99 0
LeanPool/OSforGFF/KolmogorovExtension4/KolmogorovExtension.lean 1 430 4.28 2.24 1.14 1.10 11 0
LeanPool/Duality/LinearProgrammingB.lean 1 427 3.68 2.36 1.37 0.99 19 0
LeanPool/GrothendieckVanishing/PresheafFilteredColimitCore.lean 1 424 49.39 32.77 31.53 1.24 26 0
LeanPool/Sabidussi/LoopMultigraph.lean 1 420 3.55 2.36 1.45 0.92 24 0
LeanPool/Odlyzko/Theta/PoissonSummation.lean 1 418 17.92 19.82 18.59 1.23 78 0
LeanPool/MisereGames/Ruleset/Strip.lean 1 417 7.89 7.24 6.55 0.69 76 0
LeanPool/Monlib4/Preq/StarAlgEquiv.lean 5 416 3.19 2.12 1.25 0.86 28 0
LeanPool/DirectedTopologyLean4/Dipath.lean 0 414 3.67 2.27 1.21 1.06 49 0
LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceExtension.lean 1 406 8.22 6.54 5.12 1.42 45 0
LeanPool/OSforGFF/GaussianField/SchwartzNuclear/HermiteTensorProduct.lean 3 404 22.88 25.12 23.57 1.55 101 0
LeanPool/SteinhausThreeGap/Basic.lean 1 400 15.11 11.09 10.27 0.82 100 0
LeanPool/Vlasov/OT/CharacteristicFlow.lean 3 400 46.18 60.27 58.73 1.54 94 0
LeanPool/BrauerGroupNew/ExtendScalar.lean 12 399 7.27 3.81 2.89 0.93 7 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean 7 396 20.80 27.79 26.13 1.66 99 0
LeanPool/SetTheory/Omega.lean 5 392 4.31 2.59 1.46 1.13 29 0
LeanPool/PFR/HundredPercent.lean 1 391 5.36 2.57 1.40 1.17 7 0
LeanPool/SardMoreira/LinearAlgebra.lean 1 384 4.07 2.15 1.10 1.05 3 0
LeanPool/PCFTheory/Background/Club.lean 2 374 3.27 2.71 1.77 0.94 32 0
LeanPool/PFR/TorsionEndgame.lean 4 365 30.10 58.78 57.66 1.12 10 0
LeanPool/Lean4GlCoalgebras/Split/Completeness.lean 0 358 39.86 49.82 48.88 0.94 87 0
LeanPool/ClassificationOfSurfaces/FiniteCyclicP2DegenerateRealization.lean 2 356 5.93 4.80 3.07 1.73 89 0
LeanPool/NavierStokesAndEuler/Euler/ExternalTransportCommutator.lean 2 356 5.97 6.39 5.29 1.10 26 0
LeanPool/ClassificationOfSurfaces/Moise/PLApproximation.lean 4 346 8.86 12.69 11.25 1.44 51 0
LeanPool/ZhangYeungInequality/PFR/ForMathlib/Entropy/Kernel/Basic.lean 0 345 4.54 3.50 2.36 1.14 38 0
LeanPool/JacobianDiffgeo/PeriodLattice/Discreteness.lean 3 340 10.47 7.71 6.08 1.63 4 0
LeanPool/BrauerGroupNew/MatrixEquivTensor.lean 0 330 7.60 3.81 2.87 0.94 15 0
LeanPool/MisereGames/GameGraph.lean 4 330 3.60 0.91 0.36 0.55 8 0
LeanPool/ClassificationOfSurfaces/Moise/LocallyFiniteFaceModel.lean 2 329 6.17 3.88 2.47 1.41 47 0
LeanPool/ZhangYeungInequality/PFR/Mathlib/Probability/Independence/Basic.lean 3 329 3.79 3.12 2.25 0.87 19 0
LeanPool/PFR/Kullback.lean 6 326 5.99 5.44 4.27 1.17 18 0
LeanPool/JacobianDiffgeo/Abel/OfCurveInj.lean 2 321 5.85 2.53 0.90 1.63 4 0
LeanPool/ClassificationOfSurfaces/Moise/GraphSubdivision.lean 4 320 10.23 9.04 7.66 1.38 65 0
LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean 1 308 9.42 7.08 5.40 1.68 56 0
LeanPool/NavierStokesAndEuler/NavierStokes/R3/WholeSpaceUniqueness.lean 2 308 13.68 17.39 16.28 1.11 77 0
LeanPool/FltRegular/NumberTheory/Unramified.lean 1 307 6.01 3.37 2.21 1.16 2 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/TensorBasis.lean 3 304 10.61 15.80 14.20 1.60 76 0
LeanPool/Vlasov/OT/WellPosedness.lean 20 302 30.51 35.00 33.46 1.54 74 0
LeanPool/RiemannRochFunctionFields/FundamentalIdentity.lean 4 298 3.29 1.50 0.41 1.09 2 0
LeanPool/ZhangYeungInequality/PFR/ForMathlib/FiniteRange/Defs.lean 11 295 3.61 1.66 0.84 0.82 26 0
LeanPool/ConnesRigidity/Foundation/OperatorAlgebra/Projection/ValuedSpectralMeasure.lean 1 294 11.81 7.45 5.90 1.55 4 0
LeanPool/InfinitaryLogic/Combinatorics/EndHomogeneousErdosRado.lean 2 292 4.11 3.83 3.00 0.83 49 0
LeanPool/OSforGFF/OS/OS0Analyticity.lean 3 289 10.17 6.69 4.99 1.70 22 0
LeanPool/NavierStokesAndEuler/Euler/OrdinaryEulerGradientControl.lean 1 284 7.98 8.88 7.71 1.17 35 0
LeanPool/QuasiBorelSpaces/Defs.lean 1 284 2.94 1.44 0.37 1.07 18 0
LeanPool/Monlib4/QuantumGraph/QamAExample.lean 1 283 6.08 4.76 3.20 1.56 34 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/MollifierRepresentative.lean 3 283 6.45 5.87 4.73 1.14 15 0
LeanPool/OSforGFF/Spacetime/DiscreteSymmetry.lean 1 282 4.59 2.74 1.08 1.66 15 0
LeanPool/LeanModularForms/HeckeRIngs/AbstractHeckeRing/Commutativity.lean 1 281 5.57 4.58 3.41 1.17 29 0
LeanPool/NavierStokesAndEuler/NavierStokes/R3/PairedKernelBound.lean 6 280 5.69 3.85 2.77 1.08 18 0
LeanPool/Vlasov/OT/WeakToLagrangian.lean 37 280 50.43 122.29 120.76 1.53 28 0
LeanPool/NavierStokesAndEuler/Euler/WeightedForcingTime.lean 1 278 5.58 3.90 2.76 1.14 15 0
LeanPool/LeanQuantumAlg/Primitives/QKernel/Concentration.lean 1 275 3.19 2.16 1.04 1.12 17 0
LeanPool/NavierStokesAndEuler/Euler/H6NonlinearProduct.lean 1 273 4.89 3.53 2.39 1.14 12 0
LeanPool/Lean4GlCoalgebras/General/Completeness.lean 0 272 31.12 34.00 33.10 0.90 66 0
LeanPool/Vlasov/Basic.lean 2 270 9.42 12.03 10.46 1.57 27 0
LeanPool/PartialRegularity/Extension.lean 1 268 6.22 7.78 6.04 1.74 67 0
LeanPool/FiniteGraphFundamentalGroup/Proof.lean 4 265 3.85 2.98 1.99 0.99 53 0
LeanPool/NavierStokesAndEuler/Euler/ChildParticleFieldBounds.lean 2 265 12.14 7.93 6.75 1.18 54 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/PressureSpatialRegularity.lean 0 262 11.69 13.73 12.59 1.14 22 0
LeanPool/BrauerGroupNew/CentralSimple.lean 5 261 9.49 8.87 7.63 1.24 18 0
LeanPool/NavierStokesAndEuler/NavierStokes/R3/WeightedInterpolation.lean 17 256 6.28 7.09 6.01 1.08 33 0
LeanPool/Odlyzko/ExplicitFormula/GaussDigammaEqDigamma.lean 2 256 11.81 15.61 14.46 1.15 64 0
LeanPool/NavierStokesAndEuler/Euler/LpSmoothField.lean 5 255 14.29 11.09 9.96 1.13 15 0
LeanPool/ChannelCapacity/Counterexample.lean 2 253 13.36 23.28 21.68 1.60 36 0
LeanPool/WhiteheadTheorem/CWComplex/Basic.lean 1 251 5.99 2.74 1.33 1.41 23 0
LeanPool/Brouwer/ScarfPath.lean 1 250 4.64 3.44 2.52 0.92 25 0
LeanPool/ClassificationOfSurfaces/Moise/FreeTriangleMove.lean 6 250 7.57 8.80 7.43 1.37 52 0
LeanPool/Redhill/Common/SubsumCondition.lean 2 249 4.12 3.07 2.25 0.82 22 0
LeanPool/NavierStokesAndEuler/Euler/OrdinarySobolevL4.lean 11 247 4.75 4.71 3.56 1.15 14 0
LeanPool/Feige/InsertionCommonLaw.lean 1 243 4.12 4.15 2.37 1.78 31 0
LeanPool/PolynomialMethodRestrictedSums/ANRPolynomialMethod.lean 91 242 22.04 23.44 22.39 1.05 31 0
LeanPool/NavierStokesAndEuler/Euler/ScalarEulerVorticity.lean 0 236 9.24 6.86 5.71 1.15 26 0
LeanPool/Brouwer/BrouwerProduct.lean 12 233 6.02 4.74 3.42 1.32 29 0
LeanPool/Flean/Rounding.lean 0 233 5.12 5.44 4.15 1.29 48 0
LeanPool/Rado/Surface/Assembly.lean 1 232 3.82 2.54 1.03 1.51 3 0
LeanPool/RellichKondrachov/MeasureTheory/Function/LpSpace/ChangeMeasureLeSmul.lean 4 232 5.67 3.71 2.41 1.30 8 0
LeanPool/Brouwer/Nash.lean 21 231 7.12 5.72 4.42 1.30 29 0
LeanPool/AndersonConjecture/Jensen/Adjoin/Transcendental.lean 1 230 11.42 16.62 15.26 1.36 10 0
LeanPool/DeadEnds/Basic.lean 1 230 6.26 4.48 3.04 1.44 33 0
LeanPool/NavierStokesAndEuler/Euler/LowerTransportSource.lean 2 230 4.91 4.90 3.75 1.15 17 0
LeanPool/OSforGFF/Spacetime/ComplexTestFunction.lean 1 230 6.15 4.94 3.30 1.64 22 0
LeanPool/ZhangYeungInequality/Theorem4.lean 4 228 7.47 6.56 5.04 1.52 57 0
LeanPool/Erdos367/PellLimsup.lean 3 224 15.47 19.19 17.27 1.92 56 0
LeanPool/LeanModularForms/Modularforms/ThetaDerivIdentities.lean 1 224 6.26 6.26 5.00 1.26 56 0
LeanPool/Redhill/General/Defs.lean 1 222 5.34 3.70 2.52 1.18 24 0
LeanPool/BooleanIsoperimetry/CoherentGap.lean 1 219 4.61 2.44 1.63 0.81 47 0
LeanPool/DomainTheory/Neighborhood/Exercise125.lean 1 218 2.46 1.16 0.47 0.69 17 0
LeanPool/Burkholder/MartingaleTransforms.lean 3 217 7.53 9.50 7.87 1.63 46 0
LeanPool/CompositionAlgebras/Octonions.lean 1 216 22.19 32.97 31.97 1.00 30 0
LeanPool/QuasiBorelSpaces/MeasureTheory/List.lean 1 216 4.68 1.17 0.38 0.80 9 0
LeanPool/InfinitaryLogic/Combinatorics/PairErdosRadoGeneral.lean 3 215 3.27 2.51 1.69 0.82 44 0
LeanPool/BollobasNikiforov/TN/Basic.lean 1 213 5.01 2.25 1.14 1.11 28 0
LeanPool/ConnesRigidity/Paper/Section3/DualShearMeasure.lean 2 212 10.56 6.44 4.66 1.78 53 0
LeanPool/NavierStokesAndEuler/NavierStokes/ExponentLedger.lean 1 212 6.42 4.38 3.75 0.63 53 0
LeanPool/NavierStokesAndEuler/Euler/GeneralCylinderAlgebra.lean 2 209 4.82 3.56 2.42 1.14 16 0
LeanPool/NavierStokesAndEuler/Euler/PacketTimeProfiles.lean 1 208 3.63 3.41 2.50 0.91 41 0
LeanPool/OSforGFF/GaussianField/SchwartzNuclear/SchwartzHermiteExpansion.lean 7 208 15.61 14.85 13.30 1.55 52 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/CylinderCoordinates.lean 9 202 4.75 3.54 2.46 1.08 19 0
LeanPool/SardMoreira/LocalEstimates.lean 1 201 8.22 6.70 5.23 1.47 7 0
LeanPool/Incompleteness/Foundation/Modal/Kripke/SimpleExtension.lean 1 200 3.36 1.37 0.53 0.84 11 0
LeanPool/Chudnovsky/SigmaZeta.lean 1 198 13.32 9.52 7.87 1.65 40 0
LeanPool/FormalLearningTheory/Complexity/Generalization/Core.lean 1 196 15.06 23.83 22.15 1.68 49 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/VectorCylinder.lean 12 194 5.86 3.07 1.92 1.15 10 0
LeanPool/ClassificationOfSurfaces/Moise/IntrinsicFaceModel.lean 2 192 4.97 4.24 2.90 1.34 46 0
LeanPool/Koethe/Pencil.lean 1 192 2.54 1.31 0.41 0.90 18 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/PolynomialRing.lean 1 192 5.15 3.66 2.39 1.27 30 0
LeanPool/NavierStokesAndEuler/Euler/NonnegativeLogConvex.lean 1 186 3.11 1.15 0.53 0.62 3 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/BlockLocalization.lean 1 180 25.09 21.52 19.94 1.58 45 0
LeanPool/RamanujanNagell/Helpers.lean 1 180 9.03 8.91 7.77 1.14 45 0
LeanPool/BrauerGroupNew/Subfield/Splitting.lean 3 179 14.29 7.92 6.23 1.69 4 4
LeanPool/Monlib4/LinearAlgebra/KroneckerToTensor.lean 2 178 5.08 4.50 3.08 1.42 17 0
LeanPool/Brouwer/Simplex.lean 42 176 3.97 1.81 0.74 1.07 6 0
LeanPool/LeanComplexAnalysis/Harmonic/Positive/HerglotzRieszRepresentations.lean 2 176 18.91 24.41 22.87 1.54 44 0
LeanPool/QuasiBorelSpaces/MeasureTheory/Quantile.lean 2 175 8.10 2.67 1.24 1.43 13 0
LeanPool/PFR/TauFunctional.lean 1 174 5.41 2.96 1.86 1.10 6 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/Basic.lean 5 173 4.84 4.11 2.89 1.22 25 0
LeanPool/MatchingLogic/EntryIII/Witnessed.lean 1 173 2.27 1.61 0.85 0.76 36 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/NoncompactTransport.lean 2 169 8.17 10.87 9.72 1.15 13 0
LeanPool/NavierStokesAndEuler/NavierStokes/R3/PressureFunctionals.lean 1 168 25.24 15.42 14.27 1.15 42 0
LeanPool/PFR/ImprovedPFR.lean 5 168 21.10 19.99 18.84 1.15 2 0
LeanPool/OrderPQ/MonoidHom.lean 1 166 4.51 1.63 0.57 1.06 10 0
LeanPool/FormalLearningTheory/Complexity/Rademacher.lean 3 164 28.42 37.59 35.87 1.72 41 0
LeanPool/FormalizationOfBoundedArithmetic/IOPEN.lean 1 161 4.77 6.08 4.69 1.39 22 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/Degree.lean 1 161 6.63 6.57 5.32 1.25 23 0
LeanPool/NavierStokesAndEuler/Euler/GevreyComposition.lean 1 161 3.64 1.61 0.66 0.96 4 0
LeanPool/NavierStokesAndEuler/Euler/MeanBoundaryOperator.lean 1 160 12.97 15.68 14.53 1.15 40 0
LeanPool/Zeta3Irrational/Integral.lean 4 160 19.30 25.10 23.64 1.46 40 0
LeanPool/ZetaZeros/Zeta/Kernel.lean 2 160 6.81 7.17 5.65 1.52 39 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/CylinderAlgebra.lean 2 157 4.88 3.34 2.23 1.11 12 0
LeanPool/PCFTheory/Background/Ordinal.lean 2 155 2.98 1.67 0.80 0.88 19 0
LeanPool/NavierStokesAndEuler/Euler/MetricHeatEnergy.lean 2 154 5.96 5.23 4.09 1.14 11 0
LeanPool/SelbergSieve4/SieveLemmas.lean 1 154 4.13 3.90 2.44 1.46 31 0
LeanPool/OSforGFF/Spacetime/TimeTranslation.lean 1 152 10.52 10.72 9.07 1.65 38 0
LeanPool/Odlyzko/ExplicitFormula/CompletedZetaCenterLogBound.lean 1 151 17.71 22.97 21.60 1.37 28 0
LeanPool/BannaiBannaiStanton/BoundOnDistanceSet.lean 14 148 7.13 9.63 8.28 1.35 30 0
LeanPool/ClassificationOfSurfaces/Moise/PlaneCycle.lean 2 148 5.17 3.36 1.98 1.38 24 0
LeanPool/ConnesRigidity/Paper/Section6/ModuleSemisimple.lean 1 148 18.62 11.94 10.22 1.72 37 4
LeanPool/OSforGFF/Covariance/RealForm.lean 4 148 10.21 9.44 7.88 1.56 37 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ImportedAnalyticInputs.lean 0 148 21.11 18.27 16.70 1.57 37 0
LeanPool/WhiteheadTheorem/Compressible/CWComplex.lean 3 148 7.49 3.94 2.52 1.42 10 0
LeanPool/NavierStokesAndEuler/Euler/PacketFieldPhysicalSobolev.lean 1 147 4.67 3.53 2.34 1.19 10 0
LeanPool/MRiscX/Util/BasicTheorems.lean 4 145 2.80 1.65 0.59 1.06 21 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/Residue/SectorCurve.lean 3 144 6.88 7.62 5.97 1.65 36 0
LeanPool/NavierStokesAndEuler/ForMathlib/SobolevThreeDimensional.lean 12 144 7.22 5.62 4.46 1.16 10 0
LeanPool/OSforGFF/General/L2TimeIntegral.lean 1 143 7.81 8.87 7.39 1.48 25 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/PressureJetIdentities.lean 2 142 6.80 3.93 2.84 1.09 9 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/RealCylinder.lean 7 142 4.07 2.14 1.04 1.10 10 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ProductBasisAndAnnuli.lean 0 140 12.10 9.45 7.90 1.55 35 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean 2 140 14.37 9.09 7.49 1.60 28 0
LeanPool/Wallace/FullTopology.lean 1 140 4.58 2.00 0.87 1.13 30 0
LeanPool/ConnesRigidity/Construction/PaperActionInstances.lean 4 137 7.94 7.23 5.49 1.74 34 0
LeanPool/OSforGFF/GaussianField/SchwartzNuclear/SchwartzSlicing.lean 4 136 19.70 18.70 17.16 1.54 34 0
LeanPool/Zeta3Irrational/Basic.lean 3 136 17.55 33.82 32.12 1.70 34 0
LeanPool/NavierStokesAndEuler/Euler/CylinderJetLp.lean 6 135 6.16 2.42 1.31 1.11 5 0
LeanPool/Vlasov/OT/Coupling.lean 7 134 13.70 10.34 8.81 1.53 29 0
LeanPool/OrderPQ/Basic.lean 1 133 7.14 4.31 2.99 1.32 16 0
LeanPool/ClassificationOfSurfaces/Moise/GraphRefinement.lean 4 132 6.61 6.76 5.39 1.37 22 0
LeanPool/LeanModularForms/Modularforms/SlashActionAuxil.lean 1 132 7.00 8.47 7.46 1.01 29 0
LeanPool/RiemannRochFunctionFields/SeparableRelNorm.lean 9 132 22.66 12.03 10.97 1.06 2 0
LeanPool/MatchingLogic/EntryIII/Renaming.lean 1 131 2.42 2.10 1.34 0.75 25 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Symm.lean 1 131 17.64 18.79 17.34 1.45 14 0
LeanPool/Computability/Encoding.lean 1 130 14.66 8.27 7.45 0.82 32 0
LeanPool/Lean4Itree/ITree/Basic.lean 4 130 5.65 2.16 1.34 0.82 31 0
LeanPool/LeanModularForms/Modularforms/Generators/Injectivity.lean 17 129 7.50 8.95 7.70 1.25 31 0
LeanPool/ConnesRigidity/Paper/Section5/ICCOrbits.lean 3 128 14.58 14.57 12.87 1.70 32 0
LeanPool/FormalLearningTheory/Theorem/Separation.lean 1 128 8.60 9.19 7.52 1.67 32 0
LeanPool/NavierStokesAndEuler/Euler/Foundations/SobolevProducts.lean 3 128 13.03 18.87 17.68 1.19 32 0
LeanPool/Erdos137/Base.lean 6 124 3.36 3.12 1.75 1.37 31 0
LeanPool/InfinitaryLogic/Descriptive/GSGraph.lean 1 124 2.57 1.82 0.73 1.09 31 0
LeanPool/LeanModularForms/HeckeRIngs/GL2/HeckeAction.lean 1 124 5.81 4.46 2.87 1.59 31 0
LeanPool/SelbergSieve4/Selberg.lean 1 124 5.82 5.35 3.91 1.44 25 0
LeanPool/Feige/SimplexExponentialIdentification.lean 1 123 3.97 3.37 1.81 1.56 24 0
LeanPool/Monlib4/LinearAlgebra/PiDirectSum.lean 3 123 5.77 4.47 3.50 0.96 22 0
LeanPool/NashWilliams/Combinatorics/Front/Ray.lean 7 122 3.50 1.53 0.71 0.82 18 0
LeanPool/ArchonFirstProofResults/FirstProof4/Problem4.lean 1 120 9.10 11.92 9.69 2.23 10 0
LeanPool/NavierStokesAndEuler/Euler/GevreyCompositionLp.lean 6 120 4.15 1.82 0.76 1.06 4 0
LeanPool/NavierStokesAndEuler/Euler/OrdinaryL2Integration.lean 2 120 5.11 3.25 2.08 1.17 7 0
LeanPool/OSforGFF/Covariance/Position.lean 1 120 7.02 4.99 3.43 1.56 30 0
LeanPool/ArchonFirstProofResults/FirstProof6/Problem6.lean 1 119 11.46 14.58 12.94 1.64 18 0
… +225 more files
Total 2,828 1,765,662 7755.22 7936.04 7152.69 783.35 31552 101

Aggregate phase totals

Phase Time
typeclass inference 2190126.4 ms (= 2190.13 s)
tactic execution 1282614.8 ms (= 1282.61 s)
interpretation 922475.2 ms (= 922.48 s)
simp 820782.7 ms (= 820.78 s)
import 783350.0 ms (= 783.35 s)
type checking 554262.7 ms (= 554.26 s)
blocked (unaccounted) 488691.6 ms (= 488.69 s)
elaboration 338575.6 ms (= 338.58 s)
tacticAnalysis 87461.4 ms (= 87.46 s)
norm_num 68235.5 ms (= 68.24 s)
linting 62687.7 ms (= 62.69 s)
process pre-definitions 54516.8 ms (= 54.52 s)

Slowest changed modules (from lake build)

Changed module Lake time
LeanPool.MetricCodes.Conclusion 137.00 s
LeanPool.BrauerGroupNew.IsoSecond 104.00 s
LeanPool.NavierStokesAndEuler.Euler.SourceCylinderPressureField 103.00 s
LeanPool.Monlib4.QuantumGraph.PiMatFinTwo 102.00 s
LeanPool.GrothendieckVanishing.PresheafFilteredColimit 99.00 s
LeanPool.InfiniteConnesRigidity.CarryAndCrossedProduct 96.00 s
LeanPool.MetricCodes.HarmonicAnalysis 92.00 s
LeanPool.Vlasov.OT.WeakToLagrangian 83.00 s
LeanPool.MetricCodes.Rigidity 82.00 s
LeanPool.NonSoficGroup.Spectral 80.00 s
LeanPool.PhaseRetrieval.DimdPoly.Internal.ImportedAnalyticInputs 78.00 s
LeanPool.InfiniteConnesRigidity.SpectralAndPropertyT 77.00 s

Comment truncated to fit GitHub's 64 KB limit. This PR profiles 621 files; the per-file table shows only the 396 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 merged commit 556bf98 into main Sep 18, 2026
23 of 25 checks passed
This was referenced Sep 18, 2026
Merged
Merged
Merged
JonCYeh pushed a commit to JonCYeh/lean-pool that referenced this pull request Sep 18, 2026
Jonathan Conrad @claude
Repair the build against Mathlib v4.34.0
14599b8 
main moved to Lean/Mathlib v4.34.0 (Mathlib 5ed29652, LeanPool#436) and this project no
longer built against it. Applies the repair from the maintainer review:

- Finset.prod_le_prod lost its nonnegativity hypothesis; it is now the
  ordered-monoid form with one hypothesis. The two call sites in JTPAnalytic.lean
  want the ordered-semiring form, Finset.prod_le_prod₀.
- Mathlib.Data.Complex.Basic is deprecated in favour of Mathlib.Basic.Complex.Basic.
- mul_le_one₀ is deprecated with no replacement; its proof is inlined as
  (mul_le_of_le_one_left hb₀ ha).trans hb, which is the lemma's own body.
- Four `convert … <;> …` sites produce a single goal, so the linter asks for
  `(convert …; …)`.

Verified against the pinned Mathlib at 5ed29652:
lake build LeanPool.PentagonalNumberTheoremAnalytic — 2885 jobs, 0 errors, 0 warnings.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@Vilin97 Vilin97 mentioned this pull request Sep 18, 2026
Merged
Vilin97 added a commit that referenced this pull request Sep 18, 2026
@Vilin97 @claude Vilin97 automation
Port HopfProblem to Mathlib v4.34.0 stable
fe3c100 
The v4.34.0 bump merged into this branch (#436) broke the project; CI's
Build pool failed in HomologyTheory/SingularMayerVietoris and stopped there.
Building the whole project locally surfaced the rest. Nothing mathematical
changes: every registered result still audits to propext, Classical.choice
and Quot.sound.

- Mathlib replaced the set-based `stdSimplex` by the bundled structure
  `Convexity.StdSimplex`, which `TopCat.toSSet` now uses. The singular
  chains here manipulate simplex coordinates as functions, so
  SingularMayerVietoris keeps a private copy of the retired set-based API
  (`SimplexSet`) and bridges to Mathlib's bundled simplices only at the
  `TopCat.toSSet` boundary (`toSimplex`/`ofSimplex`/`simplexIndexEquiv`);
  the face and chain-map compatibilities are now proved rather than `rfl`.
  The simplicial identity in TriangleRegularBaseFundamentalGroup is proved
  from `SimplexCategory.δ_comp_δ` instead of `SimplexCategory.toTop₀`.
- `Filter.EventuallyEq.mfderiv_eq` now inserts a `tangentSpaceCast`;
  Smale1 adds a private cast-free `mfderiv_eq'` (the cast is definitionally
  the identity) and the Recognition files use it.
- Renamed or reshaped Mathlib API: `logDeriv_mul`/`logDeriv_prod` (Pi
  forms), `IsOpenQuotientMap.secondCountableTopology`,
  `isClosed_of_discreteTopology`, `Finset.prod_le_prod₀`, removed
  `mul_le_one₀`, `JoinedIn.map` (ContinuousOn), `Set.equivOfEq`,
  `HasFDerivAt.isLittleO`, `ContinuousLinearMap.lipschitzWith`,
  `Sigma.ι_comp_desc`.
- Linter fixes: `<;>` where sequencing suffices, an unused `rfl`, and the
  `[FiniteDimensional ℝ _]` instances the `unusedArguments` linter now
  reports along the general-position chains (Mathlib's
  `dense_compl_of_dimH_lt_finrank` no longer needs them).

Validated: `lake build LeanPool.HopfProblem` warning-free (4546 jobs),
`lake exe runLinter LeanPool.HopfProblem` (15 linters, 22275
declarations), whole-library `lint-style`, `mk_all --check`, the
project card/declaration checks, the 216-declaration axiom audit and the
compiled option audit.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

needs-maintainer Actual human decision required: licensing, mathematical scope, policy, or reviewer disagreement.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Vilin97