Skip to content

chore: bump Lean and Mathlib to v4.33.0-rc1 - #295

Merged
Vilin97 merged 70 commits into
mainfrom
bump/v4.33.0-rc1
Jul 30, 2026
Merged

chore: bump Lean and Mathlib to v4.33.0-rc1#295
Vilin97 merged 70 commits into
mainfrom
bump/v4.33.0-rc1

Conversation

@github-actions

@github-actions github-actions Bot commented Jul 28, 2026 •
edited by Vilin97
Loading

Copy link
Copy Markdown
Contributor

Bumps the pool from Lean v4.32.0-rc1 to v4.33.0-rc1 and updates Mathlib and the documentation/challenge-tool pins to matching revisions.

Pins

  • Lean: v4.33.0-rc1 (62eed1db)
  • Mathlib: 79d0395a1825a6264ad5d269e35e60537518955e
  • lean4export: af5aa64bb914c3c2c781f378088dbd38acf4f804 (v4.33.0-rc1)

Migration

  • Repairs API and elaboration changes throughout all affected pool projects.
  • Removes assumptions that Lean 4.33's declaration linter now proves redundant, including downstream fixed-point cleanups.
  • Keeps abstract quotient, bundled, phantom-indexed, and game-strategy APIs opaque; 4.33-specific unfolding is restricted to exact declaration-level consumers.
  • Restores the abstract IsWinning/extQuasi public theorem types and their named simp rules while keeping representation reasoning inside proofs.
  • Narrows the remaining Borel transparency exceptions from 11 file-wide settings to 63 single-declaration attribute … in scopes without changing theorem statements or proof bodies.
  • Replaces the Paco rewrite helpers' hard-coded theorem-argument positions with elaborated theorem applications checked by definitional equality, with focused pcofix/pfold/punfold regression examples.
  • Replaces review-identified broad automation with explicit constructor proofs or targeted simp only arguments.
  • Keeps the pool sorry-free, adds no linter waiver or option backdoor, and preserves the mathematical results.

Local validation on 43f929a6560f7cba5e1d040a6df7e355775d13a4

The final pre-commit patch hash was 7ae128e5ae47127faceb615d306badeafc54b75233157d87eacae5e41f1c6499; the worktree is clean.

  • lake exe mk_all --check: passed
  • lake build LeanPool: 8,303 jobs; zero CI warnings/errors
  • LeanPool, Challenge, and Solution declaration linters: passed
  • LeanPool, Challenge, and Solution style linters: passed
  • Challenge/Solution build: 4,033 jobs; only the three registered challenge sorry notices
  • Full repository quality check, including proof-size, Lean axiom, and option-backdoor audits: passed
  • Added-line forbidden/waiver scan and git diff --check: passed
  • Imported-client simp/API tests for the restored Borel theorems: passed

An earlier migration head also passed a local doc-gen4 build (17,095 incremental jobs) and exposition extraction/site generation (144 projects, 60,979 declarations, 420,785 dependency edges). Exact-head documentation CI is running.

Performance and proof size

Independent 4.32/4.33 worktrees with version-matched caches were used.

  • Clean six-project migration build: 425.64s → 396.66s (−6.8%)
  • DirectedTopology warm changed-module median: 23.13s → 24.38s (overlapping ranges, no material regression)
  • Representative cold module builds were generally faster, including DirectedVanKampen 33s → 26s, Brauer IsoSecond 73s → 55s, and ModularForms DimensionFormulas 21s → 12s.
  • The final transparency-scoping repair changed repeated direct DirectedVanKampen elaboration by about 2%, within run-to-run noise.
  • Proof-line deltas for the six heaviest repaired projects range from −0.35% to +0.87%.
  • Aggregate .olean deltas range from −2.23% to +0.42%; generated C stays within ±0.3%.
  • Proof-size p95/p99 remain 51/114 lines and the maximum remains 200 lines.

The exact-head GitHub CI, documentation build, automated review, and proof profile are running. The PR remains draft until every required result is green.

This was referenced Jul 28, 2026
Merged
Merged
Vilin97 added a commit that referenced this pull request Jul 28, 2026
@Vilin97
Approve the bump PR's gated CI run (#299)
bf78288 
* Make the bump PR actually get a CI run

PR #295 was opened with no checks whatsoever. GitHub suppresses workflow
triggers for anything pushed with GITHUB_TOKEN, so a bump branch pushed by
the workflow yields a pull request that never runs Lean Action CI. That is
worse than a failing PR: it reads as unverified rather than broken, and the
whole point of the draft PR is that CI has vetted it.

Two paths, preferring the good one:

  - BUMP_TOKEN (a PAT or GitHub App token), when set, is used for the branch
    push and the PR, so `pull_request` workflows fire natively and the checks
    appear on the PR.
  - Without it, `assemble` dispatches Lean Action CI explicitly on the bump
    branch. The code is still built and gated; the run just lives in the
    workflow's run list rather than as a PR check.

`assemble` already re-runs the whole-pool build and all four gates and
reports them in the PR body, so the information was never missing -- it was
only invisible where a reviewer would look for it.

* Correct the bump docs to match the workflow

* Approve the bump PR's gated CI run

Correcting the diagnosis in the previous commit. A `pull_request` run *is*
created for the bump PR and is attached to the right commit -- it sits in
`action_required`, because a pull request opened by a bot has its workflow
runs held until someone approves them. No check runs are created while it
waits, so the PR shows no checks at all.

`assemble` now finds its own gated run and approves it, so the draft PR
arrives with CI already going. This only ever approves a run on the `bump/*`
branch this workflow just created, whose contents are main plus patches from
this run; the approval gate for contributor pull requests is untouched.

BUMP_TOKEN remains supported and now genuinely optional: a PAT-authored PR is
not gated in the first place.
@Vilin97 Vilin97 mentioned this pull request Jul 29, 2026
Merged
@Vilin97 Vilin97 mentioned this pull request Jul 29, 2026
Merged
Vilin97 and others added 21 commits July 29, 2026 00:00
@Vilin97 @claude
Bump the lean4export pin with the toolchain
f4c2936 
lean4export reads the oleans this repository's build produced, so its
version has to track lean-toolchain. This branch moved to v4.33.0-rc1 but
left the pin at the v4.32.0-rc1 tag, so `Verify challenge solutions`
would fail inside an export — with a file-format error rather than
anything naming the pin — the moment a solved challenge is checked.
af5aa64 is refs/tags/v4.33.0-rc1.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@Vilin97
Merge remote-tracking branch 'origin/main' into bump-sync
082863c
@Vilin97
Merge remote-tracking branch 'origin/main' into bump-sync2
eb22eeb
@Vilin97
Merge remote-tracking branch 'origin/main' into bump-sync3
827c125 
# Conflicts:
#	.github/workflows/challenge-verify.yml
@github-actions
Repair 54 project(s) for v4.33.0-rc1
92d3fc5
@Vilin97
Zeta3Irrational: drop a tactic the preceding grw now discharges
6fd11a7 
The v4.33 grw closes the vonMangoldt_nonneg side goal itself, so the
trailing exact hit 'No goals to be solved'. Proof body only.
@Vilin97
Repair four projects for Lean 4.33
80699a0
@Vilin97
Fix Circuitlib simp lemma list
1ce1e12
@Vilin97
Merge remote-tracking branch 'origin/main' into bump/v4.33.0-rc1
c7cdd07
@Vilin97
Repair BrauerGroupNew for Lean 4.33
144d276
@Vilin97
Repair Turan3 for Lean 4.33
b282698
@Vilin97
Repair LowDimSolvClassification for Lean 4.33
ccd5791
@Vilin97
Repair tail projects for Lean 4.33-rc1
2a202bb
@Vilin97
Repair Shannon1948Formalization for Lean 4.33
9f3424c
@Vilin97
Repair RellichKondrachov for Lean 4.33
d9e1f24
@Vilin97
Repair PebblingLean for Lean 4.33
c3827eb
@Vilin97
Repair Monsky for Lean 4.33
9ccd7bf
@Vilin97
Repair DirectedTopologyLean4 for Lean 4.33
0e46d5d
@Vilin97
Repair TwoColoringOneRound for Lean 4.33
ad34902
@Vilin97
Repair Sensitivity for Lean 4.33
96265fe
@Vilin97
Repair ThreeGap for Lean 4.33
2570113
@Vilin97 ChatGPT Codex Connector

Vilin97 commented Jul 29, 2026

Copy link
Copy Markdown
Owner

/profile

@github-actions

github-actions Bot commented Jul 29, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

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

Reviewed head: 94b595462242865c55591f3220d6fcfe57d2c79f

Verdict: ✅ approve

This is a pool-wide Lean and Mathlib 4.33 migration: dependency pins move forward, changed APIs and elaboration behavior are accommodated, redundant assumptions are removed, abstraction boundaries are restored for the Borel development, and many proofs are moved from broad automation or incidental unfolding to explicit equalities, targeted simp only, and reusable bridge lemmas.

Aspect Value
Scope toolchain and Mathlib migration
Introduces tech debt ✅ no
Maintainability ✅ improved
Brittleness ✅ more_robust
Risk 🟡 medium

Despite the migration's breadth, the diff reduces dependence on global simp sets and elaborator accidents, confines transparency exceptions to individual declarations, and introduces no actionable maintenance debt.

Tokens: 515,331 in / 2,616 out · Tier: flex · Effort: xhigh · Cost: $2.6355 (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 commented Jul 30, 2026

Copy link
Copy Markdown
Owner

/profile

@Vilin97 ChatGPT Codex Connector

Vilin97 commented Jul 30, 2026

Copy link
Copy Markdown
Owner

/profile

@Vilin97 ChatGPT Codex Connector

Vilin97 commented Jul 30, 2026

Copy link
Copy Markdown
Owner

/profile

@Vilin97
Vilin97 marked this pull request as ready for review July 30, 2026 05:39
@Vilin97 Vilin97 mentioned this pull request Jul 30, 2026
Merged
Vilin97 added a commit that referenced this pull request Jul 30, 2026
@Vilin97 @claude
ci: allow scripts/challenge/pins.env as version-bump metadata (#319)
234a451 
A Lean toolchain bump must move LEAN4EXPORT_COMMIT in
scripts/challenge/pins.env in the same PR — lean4export reads the oleans
our build produces, so the pin is tied to lean-toolchain. Add it to the
guard's bump-metadata allowlist so bump PRs (e.g. #295) can carry it
alongside content, exactly like the toolchain and manifest files.

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
@Vilin97

Vilin97 commented Jul 30, 2026

Copy link
Copy Markdown
Owner

Re-triggering CI to pick up the guard allowlist fix from #319 (close/reopen fires a fresh pull_request run against the updated guard).

@Vilin97 Vilin97 closed this Jul 30, 2026
@Vilin97 Vilin97 reopened this Jul 30, 2026
@Vilin97
Vilin97 merged commit cc54a3a into main Jul 30, 2026
19 of 20 checks passed
@github-actions

github-actions Bot commented Jul 30, 2026

Copy link
Copy Markdown
Contributor Author

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 5814.63 s (= 96.91 min) — user 21177.32 s, sys 1554.61 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

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

⚠️ Statements changed (488)
  • GaleStewartGame.PreStrategy.extQuasi — LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/BuildStrategies.lean
  • GaleStewartGame.PreStrategy.IsWinning — LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/Games.lean
  • GaleStewartGame.BorelDet.gameCov — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/BorelDeterminacy.lean
  • GaleStewartGame.Covering.covering_hpre_pl — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Covering.lean
  • GaleStewartGame.Covering.covering_winning — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Covering.lean
  • AgreeToDisagree.Partition.belief_eq_biUnion — LeanPool/AgreeToDisagree/AgreeToDisagreeBeliefs.lean
  • AgreeToDisagree.Partition.belief_mono — LeanPool/AgreeToDisagree/AgreeToDisagreeBeliefs.lean
  • AgreeToDisagree.Partition.measurableSet_belief — LeanPool/AgreeToDisagree/AgreeToDisagreeBeliefs.lean
  • adicCompletion_isLocalRing — LeanPool/AndersonConjecture/AdicLocal.lean
  • adjoin_transcendental_isNSubring — LeanPool/AndersonConjecture/Jensen/Adjoin/Transcendental.lean
  • countable_avoidance — LeanPool/AndersonConjecture/Jensen/Avoidance.lean
  • ideal_avoidance_of_card_lt_aux — LeanPool/AndersonConjecture/Jensen/Avoidance.lean
  • close_up_aux_factor_dvd_a — LeanPool/AndersonConjecture/Jensen/CloseUp/FactorDivisibility.lean
  • close_up_aux_factor_dvd_c — LeanPool/AndersonConjecture/Jensen/CloseUp/FactorDivisibility.lean
  • exists_prime_mem_of_ne_bot_closeup — LeanPool/AndersonConjecture/Jensen/CloseUp/TwoGen.lean
  • heitmann_prop1_noetherian — LeanPool/AndersonConjecture/Jensen/Jensen.lean
  • jensen_map_maxIdeal_le_of_closed — LeanPool/AndersonConjecture/Jensen/Jensen.lean
  • exists_prime_mem_of_ne_bot — LeanPool/AndersonConjecture/Jensen/KrullDomain/Prime.lean
  • initial_NSubring — LeanPool/AndersonConjecture/Jensen/NSubring.lean
  • transfinite_union_isUFD — LeanPool/AndersonConjecture/Jensen/TransfiniteUnion.lean
  • transfinite_union_primes_preserved — LeanPool/AndersonConjecture/Jensen/TransfiniteUnion.lean
  • a_isWeaklyQuasiComplete — LeanPool/AndersonConjecture/Main.lean
  • contraction_height_one — LeanPool/AndersonConjecture/Main.lean
  • evalₐ_zero_imp_map_mkQ_pow_zero — LeanPool/AndersonConjecture/Main.lean
  • isLocalHom_algebraMap_adicCompletion — LeanPool/AndersonConjecture/Main.lean
  • map_mkQ_eq_zero_iff_evalOneₐ — LeanPool/AndersonConjecture/Main.lean
  • map_mkQ_mk_eq_of_evalOneₐ — LeanPool/AndersonConjecture/Main.lean
  • quotient_not_analytically_irreducible — LeanPool/AndersonConjecture/Main.lean
  • ringKrullDim_le_of_adic_completion — LeanPool/AndersonConjecture/Main.lean
  • comap_map_algebraMap_adicCompletion — LeanPool/AndersonConjecture/QuasiCompleteRing/Complete.lean
  • dim1_ai_nonzero_prime_contracts — LeanPool/AndersonConjecture/QuasiCompleteRing/QuasiCompleteRing.lean
  • iInf_comap_add_pow_eq_comap — LeanPool/AndersonConjecture/QuasiCompleteRing/QuasiCompleteRing.lean
  • isQuasiComplete_iff_quotients_wqc — LeanPool/AndersonConjecture/QuasiCompleteRing/QuasiCompleteRing.lean
  • not_wqc_exists_maximal_zero_contraction — LeanPool/AndersonConjecture/QuasiCompleteRing/QuasiCompleteRing.lean
  • wqc_implies_ideals_meet — LeanPool/AndersonConjecture/QuasiCompleteRing/QuasiCompleteRing.lean
  • Azumaya.faithfulSMulTensor — LeanPool/BrauerGroupNew/Azumaya/Mul.lean
  • BrauerGroup.matrixEquivForward_tmul — LeanPool/BrauerGroupNew/BrauerGroup.lean
  • CSA_implies_CSA — LeanPool/BrauerGroupNew/CentralSimple.lean
  • IsCentralSimple.baseChange — LeanPool/BrauerGroupNew/CentralSimple.lean
  • MatrixRing.isCentral — LeanPool/BrauerGroupNew/CentralSimple.lean
  • BrauerGroupNew.not_real_subfield_of_finrank_two — LeanPool/BrauerGroupNew/FrobeniusTheorem.lean
  • BrauerGroupNew.smulCRassoc — LeanPool/BrauerGroupNew/FrobeniusTheorem.lean
  • IsMod — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • add_smul1 — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • mul_smul1 — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • one_smul1 — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • smul1 — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • smul1AddHom — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • smul1AddHom' — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • smul1_add — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • … +438 more

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

➕ Declarations added (92)
  • GaleStewartGame.Covering.Games.GameCovering — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Covering.lean
  • GaleStewartGame.BorelDet.pInvTreeHomMap_mem — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/CoveringClosedGame.lean
  • GaleStewartGame.BorelDet.One.PreLift.extension_winnable — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/One/Lift.lean
  • GaleStewartGame.BorelDet.One.PreLift.extension_won — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/One/Lift.lean
  • GaleStewartGame.BorelDet.Zero.Lift.extension_losable — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/Lift.lean
  • GaleStewartGame.BorelDet.Zero.Lift.extension_lost — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/Lift.lean
  • GaleStewartGame.BorelDet.Zero.TreeLift.losable_subtree_aux — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/TreeLift.lean
  • LeanPool.AharoniKorman.Hollom.embed_injective — LeanPool/AharoniKorman/Counterexample.lean
  • ShortComplex.moduleCatToCycles_coe — LeanPool/BrauerGroupNew/Examples/ShortComplex/LeftHomologyMapData.lean
  • smul1_one_tmul — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • smul1_tmul — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • smul1_zero_left — LeanPool/BrauerGroupNew/SkolemNoether.lean
  • ChannelCapacity.Counterexample.priorPushforward_diracProba — LeanPool/ChannelCapacity/Counterexample.lean
  • CircuitComplexity.ShannonUpper.andOr2_basis_eval — LeanPool/CircuitComplexity/Internal/ShannonUpper.lean
  • CircuitComplexity.CompileAON.mkChainGate_gate_congr — LeanPool/CircuitComplexity/Internal/Simulation.lean
  • Circuit.CombinationalCircuitCategory.tensorHom_drop — LeanPool/Circuitlib/Circuit/Category/Combinational.lean
  • Circuit.Wires.get_append — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_append_left — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_append_right — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_append_vector — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_append_vector_wires — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_append_wires_vector — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_cast_vector — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_drop — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_drop_vector — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_take — LeanPool/Circuitlib/Circuit/Wires.lean
  • Circuit.Wires.get_take_vector — LeanPool/Circuitlib/Circuit/Wires.lean
  • Computability.pfun_bind_coe — LeanPool/Computability/TuringDegree.lean
  • Computability.pfun_bind_none — LeanPool/Computability/TuringDegree.lean
  • Computability.pfun_bind_some — LeanPool/Computability/TuringDegree.lean
  • _root_.CK.lhom_ext — LeanPool/ConnesKreimer/Core.lean
  • Domain.Neighborhood.ApproximableMap.iterElem_monotone — LeanPool/DomainTheory/Neighborhood/Exercise408.lean
  • extendedFarkas.decidablePredI' — LeanPool/Duality/FarkasSpecial.lean
  • extendedFarkas.decidablePredJ' — LeanPool/Duality/FarkasSpecial.lean
  • FirstOrder.ZFC.instHasSubsetOfModelSets — LeanPool/FoZfc/Axioms.lean
  • FirstOrder.ZFC.subset_iff_extIsSubset — LeanPool/FoZfc/Axioms.lean
  • HypergraphLowerBound.shiftTwoEmbedding — LeanPool/FrontierMathOpenHypergraphs/Lubell.lean
  • HypergraphLowerBound.shiftTwoEmbedding_apply — LeanPool/FrontierMathOpenHypergraphs/Lubell.lean
  • GKPCarry.ternaryWordDigits_succ — LeanPool/GKPCarry/BadCarryCounting.lean
  • subtypeSheafHAddCommGroup — LeanPool/GrothendieckVanishing/ClosedImmersionCohomology.lean
  • sheafHAddCommGroup — LeanPool/GrothendieckVanishing/CohomologyAPI.lean
  • sheafPreadditive — LeanPool/GrothendieckVanishing/CohomologyAPI.lean
  • partialLiftCategory — LeanPool/GrothendieckVanishing/FlasqueVanishing.lean
  • TopCat.Presheaf.finsetGeneratorImageIotaMono — LeanPool/GrothendieckVanishing/GeneratedSubsheaf.lean
  • TopCat.Presheaf.finsetGeneratorMapHasImage — LeanPool/GrothendieckVanishing/GeneratedSubsheaf.lean
  • TopCat.Presheaf.hasImagesCategoryTheorySheaf — LeanPool/GrothendieckVanishing/GeneratedSubsheaf.lean
  • TopCat.Presheaf.hasImagesTopCatSheaf — LeanPool/GrothendieckVanishing/GeneratedSubsheaf.lean
  • TopCat.Presheaf.sectionHom — LeanPool/GrothendieckVanishing/GeneratedSubsheaf.lean
  • TopCat.Presheaf.sheafOfIsSheaf — LeanPool/GrothendieckVanishing/GeneratedSubsheaf.lean
  • TopCat.Presheaf.zeroOutside_map_of_le — LeanPool/GrothendieckVanishing/ZeroOutside.lean
  • … +42 more
➖ Declarations removed (11)
  • GaleStewartGame.Covering.Games.Covering — LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Covering.lean
  • LO.Arith.Fixpoint.Construction.Fixpoint — LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Fixpoint.lean
  • Nat.or_pos_iff — LeanPool/Incompleteness/Foundation/Vorspiel/Arith.lean
  • Complex.CanonicalDecomp.divisor_eq_divisor — LeanPool/Odlyzko/ECanonicalDecomposition.lean
  • Complex.ECanonicalDecomp — LeanPool/Odlyzko/ECanonicalDecomposition.lean
  • Complex._root_.MeromorphicOn.exists_ecanonicalDecomp — LeanPool/Odlyzko/ECanonicalDecomposition.lean
  • Complex._root_.Set.Subsingleton.mem_codiscreteWithin — LeanPool/Odlyzko/ECanonicalDecomposition.lean
  • Complex._root_.finprod_apply_ne_zero — LeanPool/Odlyzko/ECanonicalDecomposition.lean
  • FockSPR.filter_cast_eq_singleton — LeanPool/PhaseRetrieval/Constant/Internal/MainTheorem.lean
  • HermitekLEAN.filter_natCast_eq_singleton — LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean
  • Matrix.mulVec_apply — LeanPool/RlTheoryInLean/Data/Matrix/Mul.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,172,441 maxHeartbeats units across 576 files (7,021 added LOC).

Sum of lean --profile: 8429134.3 ms (= 8429.13 s). Import-excluded time: 7615970.3 ms (= 7615.97 s).

Count-heartbeats wall-clock total: 9131.70 s. Repeated import cost inside lean --profile: 813164.0 ms (= 813.16 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 3 273,655 131.73 89.57 87.20 2.37 62 18
LeanPool/Neukirch/HilbertRamificationTheory.lean 52 68,193 43.29 28.37 26.82 1.55 138 0
LeanPool/MRiscX/Examples/Examples.lean 3 50,401 16.34 7.62 6.36 1.26 10 0
LeanPool/BrauerGroupNew/FrobeniusTheorem.lean 2 36,507 36.11 45.24 43.39 1.85 51 0
LeanPool/BrauerGroupNew/DoubleCentralizer.lean 19 35,286 42.55 37.27 35.33 1.94 22 0
LeanPool/DirectedTopologyLean4/DirectedVanKampen.lean 55 28,678 20.90 18.84 17.46 1.38 68 0
LeanPool/Monlib4/QuantumGraph/PiMatFinTwo.lean 8 26,961 106.12 82.60 80.76 1.84 54 0
LeanPool/VirasoroProject/LieCohomologySmallDegree.lean 37 26,469 10.66 6.67 5.54 1.13 60 0
LeanPool/LowDimSolvClassification/InstancesLowDim.lean 43 26,172 30.76 16.12 14.75 1.37 97 0
LeanPool/BrauerGroupNew/Morita/TensorProduct.lean 42 22,922 21.01 12.76 11.23 1.53 45 0
LeanPool/BrauerGroupNew/Subfield/Separable.lean 14 17,746 20.08 14.96 13.01 1.95 23 0
LeanPool/WhiteheadTheorem/CWComplex/IProd/Def.lean 62 17,110 23.55 29.71 28.08 1.63 31 0
LeanPool/BrauerGroupNew/Azumaya/Mul.lean 1 16,678 30.38 26.68 24.87 1.81 71 0
LeanPool/Monlib4/LinearAlgebra/LmulRmul.lean 2 16,370 12.22 5.61 4.50 1.11 31 0
LeanPool/Monlib4/LinearAlgebra/PosMapIsReal.lean 8 15,034 35.42 34.18 32.44 1.74 78 0
LeanPool/BruhatTits/Lattice/Quotient.lean 52 14,775 22.25 19.09 17.56 1.53 37 0
LeanPool/RlTheoryInLean/Data/Matrix/Stochastic.lean 2 14,407 14.56 13.12 11.46 1.66 43 0
LeanPool/BrauerGroupNew/AlgClosedUnion.lean 7 13,577 31.68 26.92 25.56 1.36 29 0
LeanPool/BruhatTits/Lattice/Basic.lean 1 11,493 15.30 8.12 6.55 1.57 29 0
LeanPool/LowDimSolvClassification/Semidirect.lean 6 9,799 13.15 5.13 3.88 1.25 45 0
LeanPool/BrauerGroupNew/SkolemNoether.lean 120 9,255 16.29 10.34 8.35 1.99 22 0
LeanPool/Monlib4/QuantumGraph/PiMat.lean 36 8,852 107.31 150.29 148.51 1.78 96 0
LeanPool/BruhatTits/Cartan/Existence.lean 26 8,826 22.12 20.71 19.06 1.65 45 0
LeanPool/MisereGames/AugmentedForm.lean 63 8,777 13.20 16.31 15.58 0.73 76 0
LeanPool/BrauerGroupNew/ToSecond.lean 26 8,542 32.46 28.55 26.62 1.93 68 0
LeanPool/OSforGFF/GaussianField/Nuclear/NuclearTensorProduct.lean 14 8,482 20.93 20.20 18.70 1.50 78 0
LeanPool/GrothendieckVanishing/CohomologyAPI.lean 26 8,463 48.60 37.00 35.63 1.37 51 0
LeanPool/BruhatTits/Graph/Regular.lean 2 7,577 9.14 6.14 4.58 1.56 28 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/BorelDeterminacy.lean 83 7,504 7.33 6.85 5.21 1.64 23 0
LeanPool/Monlib4/LinearAlgebra/OfNorm.lean 1 7,494 13.36 13.40 11.80 1.60 56 0
LeanPool/BruhatTits/Lattice/Distance.lean 5 7,228 15.56 20.12 18.65 1.47 27 0
LeanPool/Monlib4/LinearAlgebra/Ips/Pos.lean 1 7,083 18.08 12.82 11.20 1.62 40 0
LeanPool/LowDimSolvClassification/GeneralResults.lean 2 6,947 16.87 13.15 11.89 1.26 81 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean 2 6,632 35.73 41.09 40.07 1.02 173 0
LeanPool/AharoniKorman/Counterexample.lean 6 6,580 15.40 24.47 23.51 0.96 101 0
LeanPool/SardMoreira/Chart.lean 5 6,184 27.98 27.87 26.05 1.82 26 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/ChartMeasureRiemannianVolume.lean 1 6,096 7.52 5.49 3.81 1.68 12 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/RellichKondrachovRiemannian/Chartwise.lean 1 6,091 39.46 35.26 33.05 2.21 11 0
LeanPool/GrothendieckVanishing/ZeroOutside.lean 30 5,826 11.00 14.27 12.87 1.40 25 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/RellichKondrachovRiemannian/Transport.lean 1 5,714 24.86 25.23 23.51 1.72 11 0
LeanPool/OSforGFF/Minlos/MeasurableModification.lean 5 5,520 18.43 19.08 17.33 1.75 24 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/BuildStrategies.lean 41 5,245 9.20 7.28 6.20 1.08 50 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Proof/Derivation.lean 1 4,990 29.90 23.88 22.83 1.05 162 0
LeanPool/Monlib4/LinearAlgebra/Ips/MatIps.lean 18 4,974 39.12 34.64 32.92 1.72 79 0
LeanPool/BrauerGroupNew/BrauerOverR.lean 43 4,973 13.76 10.27 8.31 1.96 16 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/Submodule.lean 5 4,834 17.08 16.04 14.40 1.64 29 0
LeanPool/BruhatTits/Graph/Orientation.lean 2 4,802 7.73 4.15 2.62 1.53 24 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Covering.lean 29 4,707 7.08 5.50 4.29 1.21 50 0
LeanPool/BruhatTits/Harmonic/Basic.lean 9 4,533 8.32 7.12 5.83 1.29 50 0
LeanPool/BrauerGroupNew/BrauerGroup.lean 12 4,503 28.71 21.07 19.31 1.76 70 0
LeanPool/BruhatTits/Utils/Matrix.lean 6 4,324 15.54 17.87 16.33 1.54 64 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Vec.lean 2 3,944 22.90 29.50 28.52 0.98 206 0
LeanPool/Incompleteness/Foundation/Logic/Calculus.lean 1 3,906 5.18 2.75 1.84 0.91 41 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean 2 3,416 19.48 21.17 20.18 0.98 157 0
LeanPool/Incompleteness/Foundation/FirstOrder/Basic/Semantics/Semantics.lean 1 3,368 9.08 9.61 8.71 0.90 133 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Coding.lean 33 3,346 8.96 11.18 10.14 1.04 141 0
LeanPool/BrauerGroupNew/ZeroSevenFourE.lean 3 3,280 18.42 17.70 15.93 1.77 19 0
LeanPool/Monlib4/LinearAlgebra/Ips/RankOne.lean 1 3,247 28.46 25.15 23.65 1.50 74 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/RellichKondrachovRiemannian/Global.lean 1 3,202 8.15 4.89 3.07 1.82 6 0
LeanPool/SetTheory/Basic.lean 9 3,129 17.04 21.50 18.27 3.23 189 0
LeanPool/BruhatTits/Graph/Edges.lean 3 3,082 16.10 15.24 13.58 1.66 31 0
LeanPool/OSforGFF/General/FunctionalAnalysis.lean 4 3,060 19.68 14.96 13.20 1.76 39 0
LeanPool/BruhatTits/Graph/GroupAction.lean 12 3,047 14.10 14.22 12.51 1.71 17 0
LeanPool/Monlib4/QuantumGraph/Matrix.lean 42 3,014 91.70 70.14 68.39 1.75 47 0
LeanPool/Monlib4/LinearAlgebra/Ips/Nontracial.lean 29 2,987 36.98 35.79 34.07 1.72 23 0
LeanPool/MisereGames/GameForm.lean 28 2,981 10.69 11.36 10.70 0.66 59 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/ChartDataRiemannian.lean 1 2,913 6.53 4.25 2.50 1.75 7 0
LeanPool/Monlib4/QuantumGraph/Example.lean 3 2,910 19.69 13.64 11.90 1.74 47 0
LeanPool/Duality/ExtendedFields.lean 1 2,891 5.12 2.96 1.96 1.00 17 0
LeanPool/Incompleteness/Foundation/FirstOrder/Basic/Syntax/Rew.lean 15 2,840 11.51 14.20 13.33 0.87 75 0
LeanPool/Incompleteness/Foundation/FirstOrder/Basic/Eq.lean 47 2,820 6.99 6.83 5.93 0.89 61 0
LeanPool/OSforGFF/Minlos/SazonovTightness.lean 18 2,812 25.67 31.83 30.13 1.70 28 0
LeanPool/VirasoroProject/CentralExtension.lean 13 2,790 12.06 3.19 2.05 1.14 28 0
LeanPool/SardMoreira/ContDiff.lean 7 2,717 8.02 7.38 5.89 1.49 23 0
LeanPool/VirasoroProject/LieAlgebraModuleUEA.lean 7 2,651 6.82 4.02 2.82 1.20 29 0
LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Model.lean 1 2,640 5.71 3.33 2.40 0.93 44 0
LeanPool/BrauerGroupNew/SplittingOfCSA.lean 2 2,622 9.97 7.26 5.64 1.62 19 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/ChartMeasureRiemannian.lean 1 2,413 6.21 4.59 2.93 1.66 7 0
LeanPool/BruhatTits/Graph/Tree.lean 3 2,278 6.60 3.68 2.14 1.54 12 0
LeanPool/ConnesKreimer/Core.lean 79 2,247 26.07 33.85 32.39 1.46 157 0
LeanPool/Monlib4/LinearAlgebra/Ips/MinimalProj.lean 5 2,095 16.85 16.94 15.35 1.59 73 0
LeanPool/OSforGFF/Minlos/MinlosConcentration.lean 2 2,074 36.88 49.34 47.57 1.77 11 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/One/Lift.lean 62 1,962 20.42 21.30 20.20 1.10 57 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/PreLift.lean 15 1,942 8.27 8.97 7.81 1.16 58 0
LeanPool/QuasiBorelSpaces/ProbabilityMeasure.lean 6 1,704 7.26 5.23 3.60 1.63 77 0
LeanPool/SetTheory/Ordinals.lean 3 1,666 6.29 4.80 3.52 1.28 39 0
LeanPool/Incompleteness/Foundation/FirstOrder/Basic/Calculus.lean 4 1,619 9.27 7.45 6.46 1.00 68 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/One/PreLift.lean 34 1,614 16.74 13.14 12.01 1.13 53 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/CoveringLim.lean 55 1,580 10.50 10.31 9.19 1.12 33 0
LeanPool/WhiteheadTheorem/HEP/Cofibration.lean 9 1,489 7.31 5.02 3.43 1.59 34 0
LeanPool/QuasiBorelSpaces/MeasureTheory/Randomization.lean 1 1,479 6.50 5.92 3.71 2.21 24 0
LeanPool/ZFLean/Naturals.lean 10 1,466 5.74 6.61 5.71 0.90 225 0
LeanPool/QuasiBorelSpaces/Sigma.lean 23 1,442 5.47 4.02 2.73 1.29 33 0
LeanPool/OSforGFF/General/SchwartzTranslationDecay.lean 1 1,441 14.39 21.33 19.56 1.77 11 0
LeanPool/Polylean/UnitConjecture/GardamGroup.lean 6 1,428 13.90 3.16 2.23 0.93 25 0
LeanPool/WhiteheadTheorem/HEP/CubeJar.lean 88 1,404 7.62 5.43 3.79 1.64 31 0
LeanPool/VirasoroProject/HeisenbergAlgebra.lean 22 1,377 5.82 4.04 2.92 1.12 50 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/ChartMeasure.lean 1 1,370 4.53 2.31 0.70 1.61 10 0
LeanPool/LeanBooleanfun/Basic.lean 2 1,328 10.90 10.56 9.05 1.51 79 0
LeanPool/Duality/FarkasSpecial.lean 11 1,319 20.01 19.26 18.10 1.16 29 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Subset.lean 20 1,293 18.53 13.18 11.51 1.67 54 0
LeanPool/QuasiBorelSpaces/OmegaHom.lean 27 1,293 5.00 3.21 1.92 1.29 37 0
LeanPool/LeanModelChecking/NNFABW.lean 3 1,285 52.51 52.36 51.41 0.95 83 0
LeanPool/DirectedTopologyLean4/PathCover.lean 2 1,284 9.72 8.68 7.40 1.28 23 0
LeanPool/Incompleteness/Foundation/Logic/HilbertStyle/Basic.lean 2 1,253 7.95 5.45 4.56 0.90 139 0
LeanPool/RellichKondrachov/Geometry/Manifold/Riemannian/VolumeMeasure.lean 2 1,253 4.24 2.26 0.59 1.67 3 0
LeanPool/LeanModularForms/Modularforms/Eisenstein.lean 7 1,210 17.42 21.15 19.76 1.39 73 0
LeanPool/Monlib4/QuantumGraph/Basic.lean 10 1,204 58.39 58.43 56.67 1.76 88 0
LeanPool/Circuitlib/Circuit/Category/Combinational.lean 157 1,197 21.39 17.70 16.88 0.82 72 0
LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Theory.lean 3 1,171 16.39 10.08 9.10 0.99 42 0
LeanPool/Monlib4/QuantumGraph/ToProjections.lean 8 1,132 40.07 35.23 33.55 1.68 50 0
LeanPool/Incompleteness/Foundation/Logic/Entailment.lean 4 1,099 6.29 4.97 4.08 0.89 105 0
LeanPool/LeanModularForms/ValenceFormula/TextbookForm.lean 6 1,064 20.50 21.11 19.16 1.95 38 0
LeanPool/Incompleteness/DC/Basic.lean 3 1,053 6.79 5.41 4.42 0.98 31 0
LeanPool/LatticeTriangle/Solution.lean 70 1,034 82.34 121.34 119.56 1.78 517 0
LeanPool/CircuitComplexity/Internal/Simulation.lean 52 1,027 10.82 7.33 6.46 0.86 77 0
LeanPool/Incompleteness/Foundation/FirstOrder/Basic/Model.lean 12 1,015 4.18 2.25 1.34 0.91 42 0
LeanPool/DomainTheory/Neighborhood/Exercise623.lean 1 982 6.17 5.02 4.01 1.01 93 0
LeanPool/Incompleteness/Arith/Theory.lean 4 978 14.55 9.74 8.68 1.06 37 0
LeanPool/OSforGFF/Covariance/Momentum.lean 1 941 25.87 33.90 32.20 1.70 85 0
LeanPool/QuasiBorelSpaces/SeparatesPoints.lean 1 927 4.52 1.74 0.44 1.30 9 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean 2 924 39.11 42.03 40.35 1.68 77 0
LeanPool/Incompleteness/Arith/D1.lean 1 899 8.69 9.05 7.80 1.25 33 0
LeanPool/Circuitlib/Circuit/Category/Sequential.lean 197 870 19.71 16.84 16.01 0.82 65 0
LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Fixpoint.lean 17 863 5.00 4.93 3.86 1.07 39 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/Lift.lean 44 855 15.12 12.55 11.41 1.14 49 0
LeanPool/RellichKondrachov/Geometry/Manifold/Riemannian/ChartLocalLipschitz.lean 1 832 6.61 3.58 1.67 1.91 2 0
LeanPool/RellichKondrachov/Geometry/Manifold/Riemannian/ChartLocalLipschitzForward.lean 1 832 8.21 4.64 3.01 1.63 2 0
LeanPool/VirasoroProject/IsCentralExtension.lean 50 818 5.26 2.50 1.34 1.16 16 0
LeanPool/Incompleteness/Foundation/Vorspiel/Vorspiel.lean 2 775 7.58 6.92 6.03 0.89 140 0
LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean 66 772 9.21 5.82 4.90 0.92 29 0
LeanPool/Monlib4/QuantumGraph/Iso.lean 18 749 22.84 19.19 17.43 1.76 22 0
LeanPool/Monlib4/QuantumGraph/QamA.lean 4 743 41.12 57.05 55.21 1.84 39 4
LeanPool/WhiteheadTheorem/Shapes/DiskHomeoCube.lean 64 738 8.22 6.34 4.71 1.63 43 0
LeanPool/Monlib4/LinearAlgebra/QuantumSet/Instances.lean 1 730 16.13 13.34 11.54 1.80 30 0
LeanPool/QuasiBorelSpaces/Functor.lean 26 716 5.47 3.21 1.92 1.29 60 0
LeanPool/Desargues/Basic.lean 1 715 7.62 6.66 6.66 0.00 42 0
LeanPool/DomainTheory/Neighborhood/Exercise617.lean 3 713 5.51 5.34 4.34 0.99 58 0
LeanPool/Brouwer/Primitive.lean 1 699 12.84 17.66 16.10 1.56 87 0
LeanPool/LeanModularForms/Modularforms/Derivative.lean 1 692 12.42 14.88 13.50 1.38 58 0
LeanPool/AndersonConjecture/Jensen/NSubring.lean 0 677 5.35 3.36 1.86 1.50 9 0
LeanPool/Chudnovsky/Ramanujan.lean 1 672 25.14 39.11 36.92 2.19 53 0
LeanPool/Burkholder/Majorants/MajorantPG2.lean 16 664 92.76 140.26 138.71 1.55 332 0
LeanPool/Burkholder/Majorants/MajorantPL2.lean 8 662 96.09 155.47 153.73 1.74 331 0
LeanPool/DemazureProduct/AspPerm.lean 4 655 12.87 17.65 16.62 1.03 171 0
LeanPool/QuasiBorelSpaces/PreProbabilityMeasure.lean 28 649 6.97 5.06 3.40 1.66 63 0
LeanPool/FormalizationOfBoundedArithmetic/LanguageZambella.lean 2 642 4.46 2.44 1.08 1.36 37 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Tree/RestrictTree.lean 1 639 10.03 6.43 5.31 1.12 48 0
LeanPool/FactorizationSystems/Orthogonality.lean 4 632 4.92 3.48 2.60 0.89 47 0
LeanPool/QuasiBorelSpaces/Cont.lean 11 626 5.52 2.54 1.11 1.43 20 0
LeanPool/Brouwer/Brouwer.lean 19 618 9.83 10.14 8.49 1.65 28 0
LeanPool/Monlib4/LinearAlgebra/Ips/Functional.lean 13 604 12.69 13.33 11.48 1.85 48 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/CoveringClosedGame.lean 234 596 10.23 12.51 11.36 1.15 59 0
LeanPool/BrauerGroupNew/Azumaya/Basic.lean 11 594 12.72 10.32 8.32 2.00 19 0
LeanPool/GrothendieckVanishing/PresheafFilteredColimit.lean 81 594 22.37 14.97 13.51 1.46 17 0
LeanPool/Incompleteness/Foundation/Modal/LogicSymbol.lean 2 594 6.89 6.27 5.40 0.86 120 0
LeanPool/DomainTheory/Neighborhood/Exercise617Gen.lean 3 588 6.87 7.92 6.94 0.98 71 0
LeanPool/BrauerGroupNew/Subfield/Subfield.lean 3 585 7.70 7.24 5.28 1.96 6 0
LeanPool/Monlib4/LinearAlgebra/TensorProduct/FiniteDimensional.lean 4 580 14.47 8.28 6.80 1.48 8 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/Strategies.lean 3 576 6.05 4.73 3.57 1.16 36 0
LeanPool/DirectedTopologyLean4/DirectedPathHomotopy.lean 3 545 9.51 8.37 7.03 1.34 46 0
LeanPool/QuasiBorelSpaces/Prod.lean 1 529 4.71 2.20 0.90 1.30 13 0
LeanPool/LeanModularForms/ValenceFormula/OrbitSum.lean 2 528 7.03 5.36 3.61 1.75 24 0
LeanPool/VirasoroProject/VirasoroAlgebra.lean 20 528 6.82 3.80 2.42 1.38 33 0
LeanPool/MisereGames/Misere/PFreeDeadEnding.lean 2 524 6.49 4.99 4.27 0.72 37 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/GaleStewart.lean 14 521 4.78 2.34 1.20 1.14 9 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Applications/Meager.lean 1 519 7.98 9.10 7.80 1.30 57 0
LeanPool/ZhangYeungInequality/PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean 12 518 6.30 4.88 3.61 1.27 26 0
LeanPool/SardMoreira/MainTheorem.lean 28 509 20.93 31.23 29.57 1.66 20 0
LeanPool/Polylean/UnitConjecture/GardamTheorem.lean 2 506 390.50 230.25 229.27 0.98 29 0
LeanPool/RellichKondrachov/Geometry/Manifold/Sobolev/ChartMeasureLp.lean 1 501 4.67 2.34 0.70 1.64 9 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/One/Strat.lean 226 497 27.18 45.98 44.84 1.14 30 0
LeanPool/QuasiBorelSpaces/FlatReal.lean 4 495 4.87 2.14 0.53 1.61 17 0
LeanPool/SetTheory/KunenInconsistency.lean 9 494 8.83 7.01 5.70 1.31 55 0
LeanPool/SetTheory/Realize.lean 4 493 12.01 9.46 8.14 1.32 108 0
LeanPool/Polytopes/Halfspace.lean 4 491 8.31 7.60 4.05 3.55 19 0
LeanPool/Computability/Oracle.lean 3 482 3.84 1.87 0.96 0.91 34 0
LeanPool/Monlib4/LinearAlgebra/PiStarOrderedRing.lean 9 477 3.26 1.65 0.70 0.95 10 0
LeanPool/DemazureOperatorsLean/StrongExchange.lean 1 474 10.39 6.30 5.14 1.16 40 0
LeanPool/Monsky/SegmentCounting.lean 73 473 22.09 30.47 28.93 1.54 94 0
LeanPool/BrauerGroupNew/TwoSidedIdeal.lean 1 467 6.43 2.04 0.99 1.05 8 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseCircleEstimate.lean 4 462 81.53 106.05 104.29 1.76 231 0
LeanPool/BruhatTits/Utils/RingHom.lean 8 459 7.73 2.94 1.72 1.22 18 0
LeanPool/LowDimSolvClassification/Tactics.lean 2 449 24.46 13.50 12.50 1.00 58 0
LeanPool/LeanModularForms/ValenceFormula/OrbitPairing.lean 4 438 6.80 5.79 4.05 1.74 39 0
LeanPool/ArtinWedderburn/Idempotents.lean 1 436 8.92 7.37 6.11 1.26 35 0
LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SearchTree.lean 2 414 7.95 5.27 4.33 0.94 19 0
LeanPool/PentagonalNumberTheorem/Old.lean 5 412 19.96 24.08 22.93 1.15 137 0
LeanPool/OSforGFF/KolmogorovExtension4/KolmogorovExtension.lean 3 408 5.53 2.84 1.64 1.20 11 0
LeanPool/Turan3/Turans3rdProof.lean 5 404 26.12 23.78 22.41 1.37 55 0
LeanPool/Polylean/UnitConjecture/TorsionFree.lean 21 403 8.54 7.08 2.53 4.55 13 0
LeanPool/ComputableReal/AuxLemmas.lean 1 401 4.56 2.52 1.62 0.90 8 0
LeanPool/SemicircleLaw/SemicircleDistribution.lean 8 400 14.03 13.85 12.20 1.65 78 0
LeanPool/CriticalPortraits/Forward.lean 1 390 9.23 6.18 5.16 1.02 75 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Auxiliary.lean 7 388 15.13 15.66 13.74 1.92 44 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/BuildLevelwise.lean 19 387 6.27 5.50 4.25 1.25 48 0
LeanPool/WhiteheadTheorem/Shapes/CubeBoundaryMap.lean 11 384 6.86 4.12 2.87 1.25 11 0
LeanPool/DirectedTopologyLean4/FundamentalCategory.lean 2 383 6.73 4.78 3.50 1.28 26 0
LeanPool/Monsky/RainbowTriangles.lean 6 382 8.79 9.09 7.55 1.54 30 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean 7 382 88.29 144.47 142.65 1.82 191 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/TreeLift.lean 230 374 17.93 27.50 26.40 1.10 32 0
LeanPool/OSforGFF/Spacetime/Basic.lean 1 373 5.57 3.90 2.08 1.82 35 0
LeanPool/GrothendieckVanishing/PresheafFilteredColimitCore.lean 51 372 20.47 12.77 11.38 1.39 26 0
LeanPool/Incompleteness/Arithmetization/Definability/Absoluteness.lean 2 368 3.47 2.19 1.22 0.97 16 0
LeanPool/PumpingCfg/ChomskyNormalForm/EmptyElimination.lean 2 367 5.20 6.19 5.30 0.89 70 0
LeanPool/Monlib4/Preq/StarAlgEquiv.lean 0 365 5.76 2.85 1.88 0.97 29 0
LeanPool/RiemannMappingTheorem/Hurwitz.lean 1 365 7.72 6.29 4.63 1.66 29 0
LeanPool/Incompleteness/Arith/D3.lean 10 362 6.67 3.81 2.80 1.01 12 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean 27 362 96.54 98.11 96.43 1.68 181 0
LeanPool/Incompleteness/Foundation/Logic/Semantics.lean 2 360 4.57 3.02 2.15 0.87 56 0
LeanPool/BrauerGroupNew/MatrixEquivTensor.lean 6 357 10.70 6.04 4.93 1.11 15 0
LeanPool/FundamentalInequality.lean 2 357 6.57 5.91 4.63 1.28 8 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Tree/BodyFunctor.lean 4 351 7.77 3.22 2.13 1.09 23 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/Zero/Strat.lean 118 350 10.81 9.71 8.62 1.09 10 0
LeanPool/ArtinWedderburn/MatrixUnits.lean 8 348 7.27 4.82 3.63 1.19 32 0
LeanPool/OSforGFF/Covariance/Parseval.lean 1 346 19.40 15.52 13.77 1.75 44 0
LeanPool/RiemannMappingTheorem/Uniform.lean 1 337 3.26 2.39 1.45 0.94 25 0
LeanPool/CompactSpectral/Topology/WeakHilbertCompact.lean 11 336 6.53 4.68 3.20 1.48 11 0
LeanPool/BrauerGroupNew/MoritaEquivalence.lean 17 333 20.70 11.56 10.23 1.33 17 0
LeanPool/SetTheory/Omega.lean 1 330 6.06 3.36 2.10 1.26 29 0
LeanPool/WhiteheadTheorem/Compressible/Disk.lean 165 329 9.72 6.70 5.10 1.60 21 0
LeanPool/Chudnovsky/Liouville.lean 7 320 19.13 41.15 38.62 2.53 53 0
LeanPool/WhiteheadTheorem/HomotopyGroup/ChangeBasePt.lean 25 317 7.89 5.39 3.76 1.63 31 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Tree/TreeExtensions.lean 4 312 6.54 4.77 3.67 1.10 22 0
LeanPool/WhiteheadTheorem/CWComplex/IProd/Iso.lean 18 312 6.79 4.50 2.93 1.57 20 0
LeanPool/Lean4Itree/ITree/Monad.lean 8 309 5.01 3.81 2.64 1.17 23 0
LeanPool/Monlib4/RepTheory/AutMat.lean 5 309 20.22 17.53 15.97 1.56 65 0
LeanPool/Biswal/Theorem1.lean 2 308 34.46 55.03 53.29 1.74 154 0
LeanPool/DemazureProduct/Avoiding321.lean 1 296 13.06 14.15 13.11 1.04 45 0
LeanPool/ComputableReal/ComputableRSeq.lean 40 293 41.08 47.96 46.93 1.03 133 0
LeanPool/PCFTheory/Background/Club.lean 13 289 4.27 3.57 2.51 1.06 32 0
LeanPool/SardMoreira/MeasureComap.lean 1 288 5.74 1.87 0.70 1.17 7 0
LeanPool/WhiteheadTheorem/Shapes/MappingCylinder.lean 0 279 5.16 3.09 1.76 1.33 28 0
LeanPool/CutAndProject/Basic.lean 36 278 21.25 32.91 31.57 1.34 139 0
LeanPool/OSforGFF/OS/OS3MixedRep.lean 1 276 16.35 19.43 17.56 1.87 23 0
LeanPool/OSforGFF/OS/OS3ReflectionPositivity.lean 5 276 11.79 13.18 11.26 1.92 30 0
LeanPool/FrontierMathOpenHypergraphs/Uniform.lean 2 274 30.59 38.63 37.71 0.92 128 0
LeanPool/OrderPQ/MulZMod.lean 5 272 3.57 2.27 0.84 1.43 20 0
LeanPool/ZhangYeungInequality/PFR/ForMathlib/Entropy/Kernel/Basic.lean 1 268 6.93 4.71 3.39 1.32 38 0
LeanPool/KaltonRoberts/Collections.lean 7 265 8.93 9.52 7.88 1.64 40 0
LeanPool/Monlib4/LinearAlgebra/ToMatrixOfEquiv.lean 9 265 11.95 9.06 7.36 1.70 34 0
LeanPool/AndersonConjecture/Jensen/Adjoin/Transcendental.lean 0 259 18.38 24.06 22.54 1.52 10 0
LeanPool/Incompleteness/Foundation/FirstOrder/Ultraproduct.lean 2 258 3.59 2.08 1.12 0.97 17 0
LeanPool/MisereGames/Form/Classes.lean 2 254 3.24 1.22 0.61 0.61 26 0
LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean 2 251 6.40 4.99 1.83 3.16 49 0
LeanPool/WhiteheadTheorem/HomotopyGroup/InducedMaps.lean 18 250 5.09 3.46 2.17 1.29 50 0
LeanPool/BrauerGroupNew/CentralSimple.lean 3 249 12.68 13.22 11.79 1.43 18 0
LeanPool/OSforGFF/Spacetime/DiscreteSymmetry.lean 1 248 5.23 3.33 1.51 1.82 15 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Proof/WinAsap.lean 21 244 12.01 9.66 8.62 1.04 41 0
LeanPool/SardMoreira/OuterMeasureDeriv.lean 1 236 13.41 8.90 7.39 1.51 12 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Basic/InfLists.lean 2 233 3.19 2.27 1.18 1.09 27 0
LeanPool/ABCExceptions/Section2.lean 5 232 25.86 39.16 37.75 1.41 99 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/DiagonalCosets.lean 13 231 30.49 27.72 26.39 1.33 57 0
LeanPool/DemazureProduct/Tableaux.lean 1 230 8.01 5.78 4.71 1.07 74 0
LeanPool/FoZfc/Axioms.lean 7 230 7.66 7.67 6.77 0.90 115 0
LeanPool/DomainTheory/Neighborhood/Theorem56Full.lean 5 225 4.13 4.11 3.12 0.98 76 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Tree/TreeLim.lean 20 222 6.23 4.20 3.10 1.10 23 0
LeanPool/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimate.lean 1 221 5.63 3.67 1.99 1.68 11 0
LeanPool/RellichKondrachov/Analysis/FunctionalSpaces/Sobolev/Euclidean/TranslationEstimateH1.lean 1 220 6.29 3.55 1.92 1.63 5 0
LeanPool/BrauerGroupNew/Examples/ShortComplex/LeftHomologyMapData.lean 9 219 5.81 2.93 1.57 1.36 7 0
LeanPool/OSforGFF/GaussianField/Nuclear/DyninMityagin.lean 1 218 5.57 1.96 0.61 1.35 3 0
LeanPool/Monlib4/QuantumGraph/QamAExample.lean 4 215 7.92 6.18 4.44 1.74 34 0
LeanPool/FrontierMathOpenHypergraphs/Uniform/FrameDefs.lean 2 213 21.60 10.41 9.49 0.92 80 0
LeanPool/Monlib4/LinearAlgebra/Matrix/IncludeBlock.lean 8 212 13.16 10.56 8.93 1.63 72 0
LeanPool/FrontierMathOpenHypergraphs/Lubell.lean 25 210 28.52 34.21 32.63 1.58 102 0
LeanPool/PumpingCfg/ChomskyNormalForm/UnitElimination.lean 1 210 11.81 8.39 7.52 0.87 40 0
LeanPool/AndersonConjecture/Jensen/TransfiniteUnion.lean 0 207 8.61 6.01 4.48 1.53 8 0
LeanPool/Redhill/Common/SubsumCondition.lean 15 205 5.42 4.20 3.29 0.92 22 0
LeanPool/LeanModularForms/GeneralizedResidueTheory/HomologicalCauchy/DixonProof.lean 2 204 13.49 14.39 12.46 1.93 34 0
LeanPool/OSforGFF/GaussianField/SchwartzNuclear/HermiteTensorProduct.lean 8 202 28.97 37.08 35.34 1.74 101 0
LeanPool/Chudnovsky/SingularModuli/ModularPolynomialQ.lean 1 199 11.90 16.66 14.50 2.16 70 0
LeanPool/TwoColoringOneRound/LowerBound/N1000000IntersectionCounting.lean 17 198 16.10 12.04 10.98 1.06 42 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Basic/MiscCat.lean 1 197 4.61 2.35 1.24 1.11 20 0
LeanPool/Chudnovsky/SingularModuli/MasserA1.lean 2 196 11.18 14.98 13.03 1.95 77 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseAnnulusEstimate.lean 25 196 29.62 53.23 51.48 1.75 98 0
LeanPool/TwoColoringOneRound/LowerBound/N9.lean 4 196 18.28 14.19 13.18 1.01 45 0
LeanPool/WhiteheadTheorem/RelHomotopyGroup/Defs.lean 2 190 4.72 2.72 1.43 1.29 28 0
LeanPool/Chudnovsky/SingularModuli/ModularPolynomialZ.lean 1 189 9.94 11.59 9.32 2.27 56 0
LeanPool/Incompleteness/Foundation/Vorspiel/Arith.lean 156 188 6.14 5.42 4.55 0.87 90 0
LeanPool/MisereGames/Misere/IntegerInvertible.lean 1 187 3.58 2.26 1.55 0.71 21 0
LeanPool/ZhangYeungInequality/PFR/ForMathlib/Uniform.lean 3 187 8.81 8.03 6.78 1.25 23 0
LeanPool/LeanModularForms/Modularforms/SummableLems.lean 20 186 38.52 42.29 41.00 1.29 90 0
LeanPool/Lean4GlCoalgebras/Split/Completeness.lean 31 184 47.24 71.72 70.71 1.01 87 0
LeanPool/AndersonConjecture/Jensen/Avoidance.lean 10 182 14.09 12.77 11.20 1.57 17 0
LeanPool/ChannelCapacity/Counterexample.lean 16 177 28.15 32.48 30.32 2.16 36 0
LeanPool/Computability/TuringDegree.lean 24 177 6.00 4.40 3.50 0.91 46 0
LeanPool/Monlib4/QuantumGraph/Degree.lean 16 176 17.36 21.64 19.88 1.76 35 0
LeanPool/PCFTheory/ClubGuessing.lean 1 175 3.67 1.89 0.86 1.03 21 0
LeanPool/CircuitComplexity/Internal/ShannonUpper.lean 16 174 62.63 69.15 68.14 1.01 87 0
LeanPool/LeanModularForms/HeckeRIngs/GL2/MultiplicationTable.lean 8 174 28.08 43.39 41.98 1.41 50 0
LeanPool/AndersonConjecture/CompleteDomain/LocalRing.lean 4 173 18.23 17.05 15.36 1.69 26 0
LeanPool/DirectedTopologyLean4/SplitPath/SplitProperties.lean 20 172 8.83 10.18 8.98 1.20 43 0
LeanPool/Sabidussi/OddBalance.lean 1 170 6.40 5.61 4.58 1.03 37 0
LeanPool/BrauerGroupNew/Subfield/Splitting.lean 2 168 32.28 20.93 18.97 1.96 4 4
LeanPool/ErdosTuzaValtr/Etv/AlphaBeta.lean 4 165 5.43 2.70 1.78 0.92 22 0
LeanPool/MisereGames/Misere/OutcomeStable.lean 5 164 10.67 11.97 11.28 0.69 42 0
LeanPool/CompactSpectral/Analysis/InnerProductSpace/RayleighCompact.lean 4 160 9.59 9.80 8.23 1.57 5 0
LeanPool/Incompleteness/Foundation/Vorspiel/Collection.lean 2 159 5.10 1.68 0.80 0.88 35 0
LeanPool/Neukirch/ExtensionOfDedekindDomains.lean 7 158 8.95 2.14 0.38 1.76 3 0
LeanPool/Incompleteness/Foundation/Modal/MaximalConsistentSet.lean 1 157 10.45 15.38 14.49 0.90 12 0
LeanPool/MisereGames/Player.lean 10 155 3.76 1.06 0.45 0.61 25 0
LeanPool/Brouwer/Nash.lean 3 154 11.53 8.53 7.00 1.53 29 0
LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean 3 152 5.54 4.48 3.13 1.35 28 0
LeanPool/KaltonRoberts/Recombination.lean 1 152 17.58 16.11 14.55 1.56 18 0
LeanPool/ChannelCapacity/Finite.lean 1 151 8.85 9.81 7.80 2.01 12 0
LeanPool/AndersonConjecture/Jensen/CloseUp/GcdComplexity.lean 11 150 6.17 4.31 2.74 1.57 6 0
LeanPool/ComputableReal/ComputableReal.lean 2 150 4.96 2.72 1.80 0.93 53 0
LeanPool/Redhill/Common/VWPair.lean 6 144 4.90 4.85 3.92 0.93 16 0
LeanPool/RiemannMappingTheorem/Spaces.lean 7 144 5.75 2.79 1.06 1.73 16 0
LeanPool/Monlib4/LinearAlgebra/KroneckerToTensor.lean 12 141 8.12 6.95 5.34 1.61 17 0
LeanPool/AgreeToDisagree/AgreeToDisagreeBeliefs.lean 5 138 5.45 4.99 3.74 1.25 17 0
LeanPool/Lean4GlCoalgebras/General/Completeness.lean 29 138 53.72 47.13 46.18 0.95 65 0
LeanPool/Flean/Rounding.lean 1 135 6.51 6.98 5.66 1.32 48 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/BasisLocalization.lean 3 134 97.85 100.63 98.86 1.77 67 0
LeanPool/BooleanIsoperimetry/Cube.lean 9 130 14.76 16.67 15.65 1.02 65 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/CoprimeMul.lean 22 130 26.20 16.75 15.35 1.40 18 0
LeanPool/OSforGFF/OS/OS3CovarianceRP.lean 1 130 13.63 7.15 5.27 1.88 21 0
LeanPool/AndersonConjecture/Jensen/KrullDomain/Prime.lean 1 129 7.27 6.15 4.58 1.57 5 0
LeanPool/WhiteheadTheorem/Compressible/CWComplex.lean 3 128 10.14 5.21 3.61 1.60 10 0
LeanPool/LeanModularForms/HeckeRIngs/AbstractHeckeRing/Module.lean 21 126 5.73 3.95 2.71 1.24 21 0
LeanPool/AndersonConjecture/Jensen/CloseUp/TwoGen.lean 1 125 24.96 15.95 14.34 1.61 5 0
LeanPool/CompactSpectral/Analysis/InnerProductSpace/CompactOperatorOrthonormal.lean 5 124 5.50 4.07 2.45 1.62 4 0
LeanPool/CompactSpectral/Analysis/InnerProductSpace/CompactSelfAdjoint/Approximation.lean 3 124 7.42 5.42 3.83 1.59 4 0
LeanPool/Redhill/General/Subsum.lean 10 124 11.89 12.39 11.10 1.29 16 0
LeanPool/TwoColoringOneRound/LowerBound/N1000000OrbitCounting.lean 8 124 5.24 3.53 2.49 1.04 31 0
LeanPool/LeanModularForms/HeckeRIngs/GLn/Basic.lean 7 123 9.73 5.63 4.34 1.29 25 0
LeanPool/Chudnovsky/SingularModuli/CosetOrbit.lean 6 120 12.38 7.92 6.11 1.81 40 0
LeanPool/Lean4GlCoalgebras/Interpolation/PartialInterpolation.lean 24 120 95.72 66.79 65.76 1.03 60 0
LeanPool/Sundogcert/Degradation.lean 27 120 8.28 2.48 1.21 1.27 20 0
LeanPool/Lean4GlCoalgebras/Pdl/Game.lean 2 118 4.03 2.33 1.51 0.83 42 0
LeanPool/PhaseRetrieval/Constant/Internal/LocalCore.lean 1 118 61.92 57.97 56.29 1.68 59 0
LeanPool/PCFTheory/Background/Ordinal.lean 34 115 3.39 2.08 1.09 0.98 19 0
LeanPool/SemicircleCheck/CatalanRecurrence.lean 7 114 20.35 25.47 24.43 1.04 55 0
LeanPool/ZhangYeungInequality/Theorem4.lean 22 114 7.80 9.59 7.71 1.88 57 0
LeanPool/DomainTheory/Neighborhood/Theorem614.lean 1 112 4.59 3.46 2.47 1.00 56 0
LeanPool/BooleanIsoperimetry/ConwayGuyCoherentGap.lean 4 111 10.63 7.52 6.49 1.03 51 0
LeanPool/LeanModularForms/Modularforms/Delta.lean 5 111 9.36 11.38 10.02 1.36 40 0
LeanPool/AFormalizationOfBorelDeterminacyInLean/Game/Games.lean 17 108 7.54 3.99 2.82 1.17 28 0
LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Representation.lean 23 106 5.41 4.80 3.84 0.96 26 0
LeanPool/MRiscX/Semantics/MsTheory.lean 4 106 5.49 3.68 2.46 1.22 53 0
LeanPool/Zeta3Irrational/Chebyshev.lean 0 106 29.10 33.78 32.12 1.66 35 0
LeanPool/OSforGFF/GaussianField/SchwartzNuclear/SchwartzHermiteExpansion.lean 3 104 20.33 21.92 20.11 1.81 52 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/ModulusRigidity.lean 9 104 47.32 52.38 50.67 1.71 52 0
LeanPool/WhiteheadTheorem/RelHomotopyGroup/Algebra.lean 1 103 2.99 1.41 0.46 0.96 10 0
LeanPool/BooleanIsoperimetry/Cascade.lean 13 102 14.57 14.22 13.14 1.08 51 0
LeanPool/OrderPQ/Basic.lean 4 101 6.39 5.59 4.15 1.44 16 0
LeanPool/DomainTheory/Neighborhood/Exercise508.lean 1 100 3.48 1.92 0.94 0.98 18 0
LeanPool/WhiteheadTheorem/Shapes/Cube.lean 5 100 6.37 5.01 3.76 1.25 50 0
LeanPool/FormalLearningTheory/Complexity/Generalization/Core.lean 5 98 21.19 32.65 30.96 1.69 49 0
LeanPool/FrontierMathOpenHypergraphs/Substitution.lean 3 98 5.30 4.29 3.36 0.94 49 0
LeanPool/CencovPetz/PermutationInvariantBilinForm.lean 3 97 13.81 7.27 5.86 1.41 23 0
LeanPool/EventStructures/Path.lean 1 97 3.64 2.88 2.09 0.79 47 0
LeanPool/FormalizationOfBoundedArithmetic/Syntax.lean 15 97 3.75 2.45 1.56 0.89 27 0
LeanPool/GrothendieckVanishing/FinitelyGeneratedVanishing.lean 16 96 19.59 12.80 11.43 1.37 6 0
LeanPool/LowDimSolvClassification/Classification3.lean 3 96 14.95 22.09 20.72 1.37 12 0
LeanPool/WhiteheadTheorem/RelHomotopyGroup/LongExactSeq.lean 22 95 8.46 5.68 4.02 1.66 13 0
LeanPool/LeanStationaryHarmonicMaps/StationaryHarmonicMap/RadiusAnalysis.lean 2 94 8.83 6.78 5.09 1.69 47 0
LeanPool/CriticalPortraits/Denominator.lean 1 93 7.78 7.94 6.85 1.09 44 0
LeanPool/OSforGFF/General/L2TimeIntegral.lean 2 93 13.53 12.67 10.96 1.71 25 0
LeanPool/Incompleteness/Foundation/Modal/Kripke/Tree.lean 7 90 4.67 3.13 2.23 0.90 26 0
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/BlockLocalization.lean 41 90 41.73 33.96 32.23 1.73 45 0
LeanPool/ZFLean/Sum.lean 46 89 5.00 3.03 2.08 0.95 32 0
LeanPool/BannaiBannaiStanton/BoundOnDistanceSet.lean 11 88 13.53 14.23 12.75 1.48 30 0
LeanPool/ErdosTuzaValtr/Etv/Label.lean 1 88 3.21 1.71 0.81 0.90 10 0
LeanPool/LeanComplexAnalysis/Harmonic/Positive/HerglotzRieszRepresentations.lean 10 88 28.25 35.47 33.81 1.66 44 0
LeanPool/LowDimSolvClassification/LemmasDim3.lean 4 88 24.06 38.68 37.33 1.35 11 0
LeanPool/FormalLearningTheory/Complexity/Measurability.lean 4 87 5.93 2.70 0.94 1.76 32 0
LeanPool/RiemannMappingTheorem/Montel.lean 8 87 5.66 2.76 0.94 1.82 7 0
… +208 more files
Total 7,021 1,172,441 9131.70 8429.13 7615.97 813.16 20781 40

Aggregate phase totals

Phase Time
typeclass inference 2169262.1 ms (= 2169.26 s)
simp 1301267.6 ms (= 1301.27 s)
interpretation 1111970.5 ms (= 1111.97 s)
tactic execution 1061901.2 ms (= 1061.90 s)
import 813164.0 ms (= 813.16 s)
type checking 577261.3 ms (= 577.26 s)
blocked (unaccounted) 422779.0 ms (= 422.78 s)
elaboration 283823.3 ms (= 283.82 s)
norm_num 92460.4 ms (= 92.46 s)
tacticAnalysis 86769.6 ms (= 86.77 s)
grind 54423.9 ms (= 54.42 s)
linting 53535.8 ms (= 53.54 s)

Slowest changed modules (from lake build)

Changed module Lake time
LeanPool.Polylean.UnitConjecture.GardamTheorem 1007.00 s
LeanPool.BrauerGroupNew.IsoSecond 194.00 s
LeanPool.Monlib4.QuantumGraph.PiMat 164.00 s
LeanPool.Lean4GlCoalgebras.Interpolation.PartialInterpolation 149.00 s
LeanPool.Burkholder.Majorants.MajorantPG2 135.00 s
LeanPool.Burkholder.Majorants.MajorantPL2 130.00 s
LeanPool.LatticeTriangle.Solution 129.00 s
LeanPool.RootSystem.An 125.00 s
LeanPool.Monlib4.QuantumGraph.PiMatFinTwo 121.00 s
LeanPool.PhaseRetrieval.DimdPoly.Internal.FiniteBaseCircleEstimate 113.00 s
LeanPool.PhaseRetrieval.DimdPoly.Internal.ImportedAnalyticInputs 111.00 s
LeanPool.PhaseRetrieval.Constant.Internal.LocalCore 108.00 s

Comment truncated to fit GitHub's 64 KB limit. This PR profiles 576 files; the per-file table shows only the 368 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.

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

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Vilin97