Repository navigation
Reduce Chudnovsky proof elaboration cost - #811
Conversation
Proof profile (new / modified Lean files)
This build covers the added modules and their dependency cones on top of the measurement environment; modified files are measured without rebuilding the pool. Statement changes✅ No statements changed — all 1,114 tracked declarations across 27 modified files kept their type; only proofs / definition bodies changed. Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 4,483,540 → 4,259,498 (-224,042, -5.0%). Commands: 2,388 → 2,388. Per-file wall sum: 572.6 s → 365.3 s (-36.2%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 25 compared — 21 cheaper, 0 costlier, 4 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%). Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from disjoint root command traces with
New files — absolute profileTotal heartbeats: 46,743 maxHeartbeats units across 1 valid file (175 added LOC). Sum of Count-heartbeats wall-clock total: 5.35 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.Chudnovsky.NumericalBounds |
3.60 s |
Per-file `lean --profile` output
LeanPool/Chudnovsky/NumericalBounds.lean
import took 944ms
share common exprs took 177ms
type checking took 141ms
linting took 113ms
cumulative profiling times:
attribute application 0.0319ms
congr simp thm 0.481ms
declTypeLinter 1.87ms
dsimp 1.52ms
elaboration 103ms
fix level params 4.45ms
import 944ms
initialization 25.2ms
instantiate metavars 18.3ms
interpretation 351ms
let-to-have transformation 0.0594ms
linting 134ms
module linting 0.00826ms
norm_num 248ms
parsing 5.59ms
process pre-definitions 82.6ms
ring 195ms
share common exprs 204ms
simp 4.15ms
tactic execution 365ms
tacticAnalysis 1.66ms
type checking 203ms
typeclass inference 254ms
real 2.94
user 2.69
sys 0.78
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
🤖 LLM review — refactor (
|
| Aspect | Value |
|---|---|
| Scope | proof optimization and certificate module split |
| Introduces tech debt | 🛑 yes |
| Maintainability | ✅ improved |
| Brittleness | ✅ more_robust |
| Risk | ✅ low |
The proofs are simpler and more explicit overall, with minor documentation debt that does not warrant blocking the refactor.
Findings (1)
- dead-leftover —
LeanPool/Chudnovsky/Kummer.lean:738
The section roadmap at lines 220–223 and the lemma description at lines 685–687 still describe the exponentially weighted modulus. This proof now establishes monotonicity and the zero limit directly for the squared modulus. Update both descriptions so readers can follow the roadmap without looking for the removed exponential-weight argument.
Tokens: 2,415,961 in / 9,606 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $9.8079 (Standard API equivalent; uncached input) (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
changed the title
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict. [Low impact] No blocking code issue was found in the proof refactor or the new certificate module. SummaryThe PR reduces repeated proof work in the Chudnovsky development without changing the existing source-level mathematical contracts.
Vilin97 explicitly retains the private wrappers to preserve the exact declaration contract. Removing them would conflict with that stated goal. Vilin97 also explicitly states that the whole-project 10% improvement target was not established and distinguishes the observed timings from a performance guarantee. Reviews (1) · Last reviewed commit: "Narrow numerical certificate imports wit..." · Reviewed by Greptile |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"summary": "This refactor isolates two real interval certificates and simplifies the hypergeometric-radius, Wronskian and final differential-identity arguments while retaining their intermediate mathematical reasoning. The remaining edits mainly make simplification and arithmetic inputs explicit. The existing written interfaces and computational definitions are preserved; the change improves maintainability without adding material technical debt.",
"assessment": {
"scope": "proof optimization and numerical-certificate module split",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The refactor keeps the mathematical contracts and readable proof structure while reducing repeated elaboration and separating elementary certificates from the analytic development."
},
"verdict": "approve",
"findings": [],
"reviewed_commit": "5127d9273c98e54df93f8bbd96586e039c5dc293",
"evidence": {
"source": "Compared complete current35/Main34 Lean modules and unchanged project card; all1184 retained written declaration headers and157 nonproof blocks are literal. The203 retained proof-body edits and two new certificate theorems were reconciled. Substantive analytic arguments, actual providers/callers and15 exact rational certificate margins were independently checked.",
"hosted_validation": "Exact-head Lean Action CI run43474513212 passed. All28 changed files compiled freshly;32 total fresh module compilations had maximum24 seconds. Lint checked35 modules/2367 declarations; style, quality and all applicable required contexts passed.",
"limits": "Written-source preservation is not a claim to reproduce the author's private compiled inventory or performance experiments. The reported timing-table arithmetic checks out, but shared-host measurements do not establish a universal speedup. The advisory profile's partial failures and voluntary10percent target do not block this source assessment.",
"integration": "The configured report currently visible covers fcba3dc, so a fresh configured assessment at5127d927 is still needed before protected queue admission."
}
}
|
/review |
Chudnovsky repeatedly normalizes large arithmetic expressions and carries real interval certificates in its final modular-form module. This separates the certificates and restructures the convergence, Wronskian and main-theorem proofs while preserving every existing elaborated declaration.
Six-hour daily optimization cycle completed. The whole-project 10% wall-time/RAM target was not established. The primary clean-commit experiment shows 7.01% lower mean wall time, 3.25% lower mean CPU time and essentially unchanged RSS; the source-declaration profile uses 4.71% fewer allocation-counter ticks. Shared-VM timing variation limits precision.
Changes
generalizedHypergeometricSeries_radius_eq_one. Reuse one linear-ratio limit argument and avoid redundant norm simplification and nonvanishing obligations.NumericalBounds, with smaller rounded factor enclosures for the scaled s₂ estimate. Keep both original private declarations as exact-type wrappers. Narrow the new module's imports withlake shake.Invariant audit
Base:
701389c04bdd56aabf8dbb9ad729165fdba772b5. Head:5127d9273c98e54df93f8bbd96586e039c5dc293.A Lean environment exporter was run on the base before editing and again on the complete compiled candidate. It imports all owned modules at private visibility with extensions disabled, records every owned constant including private/generated declarations, and compares exact structural expression DAGs. The comparison includes fully elaborated types, universe/binder parameters, declaration kind, safety, reducibility and inductive/recursor metadata, plus complete values for every non-theorem. Only theorem proof bodies and expression metadata are omitted.
All 2,316 original declarations are unchanged: zero missing, zero changed. This includes 2,121 theorems and 195 non-theorem declarations. The additions are two supporting theorems and 50 generated proof helpers, all theorems. Every difference found during development was investigated and the owning edits were restored where needed, including generated-helper type differences.
An independent source audit preserves all theorem signatures and non-proof commands in the 34 original files, including 157 immutable non-theorem source blocks. Existing public imports, names, definitions, instances, notation and namespaces are preserved. The generated project aggregate gains NumericalBounds; the pool discovery root stays fixed.
Manifest SHA-256: base
294d1dd1ea288b2252ba6161d26fae3950a2ce1e648c65bb85937bb901c191c5; head1b79118b9f6f6d47be9379b4b7241e6071b3ed97197a5e0872c5b69a0520537d.Controlled resource measurements
Each run deletes only Chudnovsky's compiled library/IR outputs and rebuilds its entire target: 34 modules at base, 35 at head. Pinned dependencies and the compiler-linter plugin remain warm. The primary experiment switches between clean exact-commit checkouts in the same isolated worktree, checking clean Git status and source/configuration fingerprints. The original branch is restored afterwards. The fixed command is:
No other Lean build/profile from this task overlaps either series. GNU time supplies wall/CPU time and largest-process RSS; a 0.1-second process-tree sampler supplies aggregate RSS, which includes shared mappings. The primary experiment uses all runs from two predeclared base/head/head/base blocks (four runs per revision).
Wall-time ranges: base: 144.70–210.73 s; head: 136.02–187.02 s. Wall-time medians: base: 183.360 s; head: 174.250 s. The balanced blocks give 10.14%, 3.17% wall-time reductions. These are observed measurements on a shared VM; they do not establish an exclusive-machine performance guarantee.
Earlier 12-run source-swap observations at 5127d92
These used identical source/configuration fingerprints but left the base tree dirty relative to the candidate commit. This possible bookkeeping confound is why the clean-commit series above is primary. All earlier observations are preserved.
Declaration profile
A separate synchronous command profile on the exact head totals 2,940,080,919 → 2,801,664,669 raw allocation-counter ticks (4.71% fewer). It covers 1,179 original source declarations and the two new certificate theorems, taking the maximum per declaration to avoid double-counting elaboration wrappers. This diagnostic is separate from whole-project wall time and RAM.
generalizedHypergeometricSeries_radius_eq_one: 33,540,478 → 17,128,879 ticks (48.93% fewer).Chudnovsky.WrC_eq_zero: 23,856,685 → 18,720,139 ticks (21.53% fewer).Chudnovsky.thm42: 23,407,679 → 15,019,787 ticks (35.83% fewer).The hosted advisory profile reports 5.0% fewer heartbeats across 25 compared files, but its merge-base environment cannot find the new
NumericalBounds.oleanwhen profiling Coefficients and Imports. Those two advisory measurements fail; the actual head build and the local profile of all 35 modules succeed. The hosted partial result is not used as the whole-project resource measurement.Validation
lake env lean --run scripts/ci/lint-project.lean <all 35 owned modules>: 2,367 declarations pass Mathlib linters.lake exe lint-style LeanPool.Chudnovsky.Importsandgit diff --check.lake exe mk_all --module --check --repo <selected-project fixture>plus exact aggregate and canonical-root checks.lake shake --force --keep-public --explain LeanPool.Chudnovsky.Imports: no remaining suggestions. Here--forceskips the whole-package stale-olean preflight for unrelated projects; the selected project is fully built before analysis.Applicable hosted validation on this exact head also passed: project build, index, Mathlib lint, style, repository quality, Python, workflow/separation/port/exposition checks, Documentation preflight and proof profiling. Lean validation run. Local validation covers all 35 owned modules; a cold full-pool build was not run locally. No repository gates, settings, waivers, unrelated projects or project statements/definitions are changed.