From d5fdd63972c0ea15b39c73fc2958ef64f8964c7f Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 23 Sep 2026 13:37:19 +0000 Subject: [PATCH 1/4] Add Comparator challenge and formalization metadata --- .github/workflows/comparator.yml | 64 +++++++++++++ Challenge.lean | 36 ++++++++ README.md | 153 ++++--------------------------- Solution.lean | 8 ++ config.json | 7 ++ formalization.yaml | 86 +++++++++++++++++ lakefile.toml | 8 +- 7 files changed, 228 insertions(+), 134 deletions(-) create mode 100644 .github/workflows/comparator.yml create mode 100644 Challenge.lean create mode 100644 Solution.lean create mode 100644 config.json create mode 100644 formalization.yaml diff --git a/.github/workflows/comparator.yml b/.github/workflows/comparator.yml new file mode 100644 index 0000000..aaf13ca --- /dev/null +++ b/.github/workflows/comparator.yml @@ -0,0 +1,64 @@ +name: Comparator + +on: + push: + pull_request: + workflow_dispatch: + +permissions: + contents: read + +jobs: + comparator: + runs-on: ubuntu-24.04 + timeout-minutes: 45 + + steps: + - uses: actions/checkout@v4 + + - uses: actions/checkout@v4 + with: + repository: leanprover/comparator + ref: 777e7f56119efc0fac34003db4efe831e0b53723 + path: .ci/comparator + + - uses: actions/checkout@v4 + with: + repository: Zouuup/landrun + ref: 811cfff51ceaf3d9843708aa6d22e9b84ccac8b4 + path: .ci/landrun + + - uses: actions/setup-go@v5 + with: + go-version: stable + + - name: Build Landrun + working-directory: .ci/landrun + run: go build -o landrun cmd/landrun/main.go + + - name: Set up Lean and fetch the Mathlib cache + uses: leanprover/lean-action@v1 + with: + auto-config: false + use-mathlib-cache: true + + - name: Build Comparator + uses: leanprover/lean-action@v1 + with: + lake-package-directory: .ci/comparator + auto-config: false + build: true + build-args: lean4export comparator + use-mathlib-cache: false + + - name: Run Comparator + env: + COMPARATOR_LANDRUN: ${{ github.workspace }}/.ci/landrun/landrun + COMPARATOR_LEAN4EXPORT: ${{ github.workspace }}/.ci/comparator/.lake/packages/lean4export/.lake/build/bin/lean4export + run: >- + systemd-run --property=RestrictAddressFamilies=~AF_UNIX --user --pty --pipe + -E PATH="$PATH" + -E COMPARATOR_LANDRUN="$COMPARATOR_LANDRUN" + -E COMPARATOR_LEAN4EXPORT="$COMPARATOR_LEAN4EXPORT" + --working-directory "$PWD" -- + bash -c 'lake env .ci/comparator/.lake/build/bin/comparator config.json' diff --git a/Challenge.lean b/Challenge.lean new file mode 100644 index 0000000..9d445c8 --- /dev/null +++ b/Challenge.lean @@ -0,0 +1,36 @@ +/- +Copyright 2025 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import Mathlib + +/-! +# Irrationality of ζ(5) + +This challenge statement is copied verbatim from the Formal Conjectures +repository, `FormalConjectures/Wikipedia/RiemannZetaValues.lean`, theorem +`RiemannZetaValues.irrational_five`, at commit +[`2db01438fda960163f58ff2c2385b52e53f56dd2`](https://github.com/google-deepmind/formal-conjectures/blob/2db01438fda960163f58ff2c2385b52e53f56dd2/FormalConjectures/Wikipedia/RiemannZetaValues.lean). +-/ + +namespace RiemannZetaValues + +/-- +$\zeta(5)$ is irrational. +-/ +theorem irrational_five : ∃ x, Irrational x ∧ riemannZeta 5 = x := by + sorry + +end RiemannZetaValues diff --git a/README.md b/README.md index efed27c..b6a0db7 100644 --- a/README.md +++ b/README.md @@ -1,145 +1,32 @@ # Zeta5 -Lean 4 / Mathlib project around the statement +Lean 4 / Mathlib formalization of ```lean theorem irrational_five : ∃ x, Irrational x ∧ riemannZeta 5 = x ``` -following the preprint *ζ(5) is irrational* (A. Fauzan, 17 September 2026). +The proof follows A. Fauzan’s preprint, *ζ(5) is irrational* (17 September +2026). The project is licensed under Apache 2.0. -Toolchain: Lean `v4.33.1`, Mathlib `v4.33.1` (commit `0df444a3`). The prime number theorem -`θ ~ id` comes from [PrimeNumberTheoremAnd](https://github.com/mo271/PrimeNumberTheoremAnd/tree/v4.33.1) -(the `v4.33.1` branch, pinned to commit `04d81b2a`), imported in `Apery/PNT.lean`. +## Project map -License: Apache 2.0 (see `LICENSE`), as for Mathlib and PrimeNumberTheoremAnd. +- `Challenge.lean` contains the benchmark statement, copied from the Formal + Conjectures declaration + [`RiemannZetaValues.irrational_five`](https://github.com/google-deepmind/formal-conjectures/blob/2db01438fda960163f58ff2c2385b52e53f56dd2/FormalConjectures/Wikipedia/RiemannZetaValues.lean). +- `Solution.lean` proves the same statement using `Apery.irrational_five`. +- `Apery/` contains the proof development. +- `config.json` and `.github/workflows/comparator.yml` configure Comparator + verification. -## Status +## Dependencies -**The formalisation is complete.** `irrational_five` is proved without `sorry`: +- [Mathlib](https://github.com/leanprover-community/mathlib4), pinned to + `v4.33.1`. +- [PrimeNumberTheoremAnd](https://github.com/mo271/PrimeNumberTheoremAnd), + imported by `Apery/PNT.lean` for the prime number theorem. +- [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) + supplies the challenge statement; it is cited above rather than imported + as a project dependency. -``` -#print axioms Apery.irrational_five --- [propext, Classical.choice, Quot.sound] -``` - -The two `sorry`s inside the `PrimeNumberTheoremAnd` dependency (`Wiener.lean`) are not reached. - -**Deviation from the paper.** The normaliser is `mN n = ∏_{p ≤ 2h} p^{-L_p}` (`Apery/Norm.lean`), -where each `L_p` is one of the local bounds *proved here*: - -* the small-prime bound (3.12), for `p · 400 ≤ K`; -* the inner-range bound with a water-filling allocation, for `K/400 < p ≤ K/3`; -* the outer-range bound with a full rank loss, for `p > K/3`. - -This differs from the paper in three places: - -* the rank loss is `r` rather than `min(r, z)` (Lemma 4.2), costing `9/640` in the constant; -* the cutoff is `M = 400` rather than 200; -* the valuation bounds are proved by direct class-wise partial fractions instead of the - Tate-algebra functional. - -Irrationality needs only `A_eff + U < 0`, not the paper's rate `139/5`. So `main_estimate` gives -`0 < Q_n(ζ(5)) < exp(-c n²)` with `c = -800(A_eff + U) > 0`, which suffices for the criterion. -Numerically, the constant these bounds achieve is `≈ 1.345`, below `A_eff = 1.36`, which is -below `-U = 1.36700`. - -Proved parts of the paper: the degree formula (2.9); **Proposition 2.2 in full** (polynomial -moments from Euler's formula, pole moments via Hermite's formula at `s = 5`, partial fractions, -positivity of `Δ_K(ζ(5))`); **Section 6 in full** (Lemma 6.1 via Table 2, Lemma 6.2, the -configuration inequality (6.9), Andréief, (6.11)–(6.15), Proposition 6.3); Appendix A; Section 7; -**Sections 3–4 in the form above** (the bound (3.12) at every prime, the inner and outer local -bounds, unimodular class bases, Proposition 5.1 for `mN`). - -| File | Content | Status | -|---|---|---| -| `Apery/Criterion.lean` | Irrationality criterion (paper §1.1): if for large `n` there is an integer polynomial `Q` of degree `≤ d n` with `0 < Q(ξ) ≤ ε n`, and `b^(d n) ε n → 0` for every positive integer `b`, then `ξ` is irrational. Also `b^(37n) exp(-139n²/5) → 0`. | proved | -| `Apery/Construction.lean` | Definitions of §2.1: `D_m`, the functional `μ_X` (2.2)–(2.3) via polynomial division and partial fractions, the Hankel matrix `G_K(X)` (2.4), `Δ_K = det G_K`, `S_K` (2.5), `F_K = S_K Δ_K`. | definitions | -| `Apery/Degree.lean` | (2.9): `deg Δ_K = deg F_K = h = 37 n`, via the affine entries and a weighted Vandermonde determinant. | proved | -| `Apery/Zeta5.lean` | `zeta5 : ℝ` and `riemannZeta 5 = ↑zeta5`. | proved | -| `Apery/Constants.lean` | `U`, `A*`, `A_M`, `A₂₀₀`; identity (5.20) and margin (7.2) by `norm_num`. | proved | -| `Apery/Stirling.lean` | `log m! ≤ m log m - m + (log m)/2 + 1`, `m log m - m ≤ log m!`, and `∑_{i 0` (Gram matrix of a positive weight, `Matrix.PosDef.det_pos`). | proved | -| `Apery/Andreief.lean` | Andréief's identity `det(∫ fᵢ gⱼ dμ) = (1/n!) ∫ det(fᵢ(xⱼ)) det(gᵢ(xⱼ)) dμⁿ`. | proved | -| `Apery/DetIntegral.lean` | (6.10): `Δ_K(ζ(5)) = (1/h!) ∫_{(0,∞)^h} det V(y)² ∏ν(yᵢ) dy` with `V` the Vandermonde matrix of the `yᵢ²`. | proved | -| `Apery/Energy.lean` | The external field `V` (6.1); the bound `w(y) ≤ (1/π)(1+2πy)⁵e^{-2πy}`; both directions of the sum–integral comparison (6.12); `∫₀^∞(1+2πy)⁵e^{-y/K}dy ≤ C K⁶`; a.e. configurations have positive, pairwise distinct coordinates. | proved | -| `Apery/PotentialV.lean` | The closed form (A.5) of `V`: `∫₀^c log(t+u²)du = c log(t+c²) - 2c + 2√t arctan(c/√t)`. | proved | -| `Apery/EnergyBound.lean` | The configuration inequality (6.9) as `energy_ineq` (from `EnergyFinal`); the pointwise bound for the integrand of (6.10) and its integration, giving (6.14) as `log_Δ_le'`. | proved | -| `Apery/Potential.lean`, `Apery/TableCheck.lean`, `Apery/Table/*.lean` | Lemma 6.1: the potential `Uρ` of the arcsine measure (closed form (A.1)), monotonicity of `Uρ` and `V`, the reduction of (6.2) to endpoint checks, the certified endpoint bounds on all 684 intervals of Table 2 (generated, ~110k lines), the tail `t ≥ 2` via (6.8), and `potential_ineq : 2Uρ(t) - V(t) ≤ M₀` for all `t > 0`. | proved | -| `Apery/Gaussian.lean`, `Apery/ZeroMass.lean`, `Apery/Kernel.lean`, `Apery/EnergyLimit.lean` | Lemma 6.2 (zero-mass logarithmic energy) for finite families of parametrised curves with real weights: Gaussian positivity for the truncated kernel `L_{a,b}`, the limit `L_{a,b} → log` by dominated convergence, `energy_log_nonpos`. | proved | -| `Apery/CircleAtoms.lean`, `Apery/ArcsineAtoms.lean`, `Apery/ArcsinePotential.lean`, `Apery/EnergyAtoms.lean` | The circle and arcsine atoms: circle integrals of `log‖·-a‖` (from Mathlib's circle-average identity), the factorisation `z - (m + r cos θ) = -(r/2w)(w-q₁)(w-q₂)`, the potential formula (A.1) as `arc_potential_real`, the Hölder-1/2 estimate for the potential, integrability on the torus, and Lemma 6.2 applied to a configuration (`atom_energy_nonpos`). | proved | -| `Apery/EnergyBlocks.lean`, `Apery/EnergyRaw.lean`, `Apery/EnergyFinal.lean` | The four blocks of the atom energy (circle self-energy `(2π)² log ε`, circle–circle `≥ (2π)² log|tᵢ-tⱼ|`, circle–arcsine `≤ (2π)²(Uω(tᵢ) + error)`, arcsine–arcsine `≥ (2π)² I(ρ)` via `∑ c_j c_k f(max j k) = ∑ (S_j² - S_{j-1}²) f_j`), the raw inequality `energy_raw`, the error bound with `ε = K⁻⁶`, the pointwise bound (6.7), and **(6.9)** as `energy_ineq_final` with constants `(λM₀ - I(ρ))K² + 5h + 6h log K`. | proved | -| `Apery/RealBound.lean` | (6.14) as `log_Δ_le` (from `EnergyBound`), (6.15) as `log_S_le` (proved), and Proposition 6.3 (`real_bound'`) from `Δ_pos`, `log_Δ_le`, `energy_const`, `log_S_le` (proved). | proved | -| `Apery/Arith/Val.lean`, `IntPoly.lean`, `BinomBasis.lean`, `TauBound.lean`, `PoleFun.lean` | Valuations `VG` on `ℚ` and Gauss valuations `GV` on `ℚ[X]`, the weighted determinant bound `det_GV`; the Bernoulli functional, the binomial basis, the bound (3.9) (`tau_bound`); the functional `τ_X` on rational functions with integer poles. | proved | -| `Apery/Arith/DirectPoly.lean`, `DirectBound.lean` | The **direct entry bound** `tauX_direct`: `v_p^G(τ_X(g)) ≥ min_c(e_c − ℓ_c) − 4`, replacing the paper's Tate-algebra functional and distribution formula (Lemmas 3.1–3.2) by class-wise partial fractions. | proved | -| `Apery/Arith/Pullback.lean`, `BasisChange.lean`, `Unimodular.lean` | The pullback identity (3.1) `μX_eq_tauX`; linearity of `μ_X` and `det_basis_change` (`det[μ_X(D_N⁶E_aE_b)] = det(C)²Δ_K`); unimodularity of the class bases by CRT over `𝔽_p` (`coeffMat_det_unit`). | proved | -| `Apery/Arith/TEntry.lean`, `ClassFrame.lean`, `ClassCount.lean`, `InnerWeights.lean` | **Inner range** (Prop. 4.1 analogue): the class framework `class_frame` (valid weights `w` give `v_p^G(Δ_K) ≥ 2∑w`), the class counts, and `inner_bound_cap`: for any allocation `L` of the `37n` rows to the classes with `∑L = 37n` satisfying the zero-class condition, `v_p^G(Δ_K) ≥ 2∑ wcap`. | proved | -| `Apery/Arith/MomentVal.lean`, `LowRank.lean`, `OuterFrame.lean` | **Outer range framework**: `p`-integrality of the moments below `2p − 3` (von Staudt–Clausen), the low-rank correction of the high moments, and the Schur-complement bound `outer_frame`: `v_p^G(Δ_K) ≥ 2∑w − r` with `r = 37n − ((2p+22n−3) − (37n−1))`. | proved | -| `Apery/Arith/PoleVal.lean`, `OuterEntry.lean`, `OuterBasis.lean`, `OuterEntries.lean`, `OuterEntryMain.lean` | **Outer range entries** (Prop. 4.3 analogue): valuations of the pole values `μ_X(1/(t+j²))` (including the pairing `j, p−j` via `H^{(5)}` congruences, `pair_GV`); the class basis `rootsO` and its reduction mod `p`; the residue bounds per class; the three cases (both rows below the big-pole count, one row above it, the zero class); `outer_entry` and **`outer_bound`**: for `7 ≤ p`, `3n < p`, `40n < 3p`, `v_p^G(Δ_K) ≥ 2∑_c ∑_{i 0`) from `degree_F`, `real_bound`, `normalization`. | proved (modulo `growth_mN`) | -| `Apery/Main.lean` | `irrational_zeta5` and `irrational_five`. | proved | -| `Apery/PNT.lean` | The prime number theorem `θ ~ id` (`theta_asymptotic`), from the `PrimeNumberTheoremAnd` dependency. | imported | - -How `growth_mN` is assembled. `log m_K = ∑_{p ≤ 2h} (-L_p) log p` is split into four prime -ranges: - -| Range, with `x = K/p` | Per-prime bound | Contribution to `K⁻² log m_K` | -|---|---|---| -| `p ≤ K/400` | `-L_p = 6h⌊log_p 200n⌋ + h v_p(24)` | `6λ/400 = 0.013875` (PNT) | -| `3 ≤ x ≤ 20` | `table_Lp_le` | `(5.18) = 0.042788…` | -| `20 ≤ x ≤ 400` | `tail_Lp_le` | `≤ -0.053462…` | -| `20/37 ≤ x < 3` | `outer_Lp_le` | `129101/96000 = 1.344802…` | - -The total is `1.348003… < A_eff = 1.36 < -U = 1.36700`. - -## Numerical checks of the paper (not part of the Lean development) - -Exact computations of `Δ_K(X) ∈ ℚ[X]` for `K = 40, 80, ..., 240` (python-flint), with -`P_K := Δ_K / content(Δ_K)` the primitive integer polynomial: - -| n | K | log F_K(ζ5) / K² | −log content(F_K) / K² | log P_K(ζ5) | log P_K(ζ5) / n² | -|---|---|---|---|---|---| -| 1 | 40 | −1.276 | 1.110 | −265 | −265 | -| 2 | 80 | −1.329 | 1.199 | −833 | −208 | -| 3 | 120 | −1.348 | 1.223 | −1804 | −200 | -| 4 | 160 | −1.357 | 1.230 | −3247 | −203 | -| 5 | 200 | −1.363 | 1.251 | −4479 | −179 | -| 6 | 240 | −1.367 | 1.251 | −6669 | −185 | - -The paper's asymptotic constants are `U = −1.36700` (real side) and `A_200 = 1.34960` -(normalisation), giving the claimed `−139/5 = −27.8` per `n²`. The exact rational data of -Appendix B (the integrals (5.18) and (5.10), Tables 3 and 4, and `A*`) were recomputed from the -paper's definitions and agree exactly (`scripts/appendixB.py`); the constants of Appendix A.4 -(`I(ρ)`, `C*`, and the margin `6.45·10⁻⁸` in (6.4)) were recomputed to 40 digits and agree; the -potential inequality (6.2) of Lemma 6.1 was recomputed over the 684 intervals of Table 2 -(`scripts/lemma61.py`) and holds with the stated margin. Also verified exactly: the -leading-coefficient formula (2.9), the moment formulas (2.2)/(2.3) by numerical integration, -the valuation bound (3.12) at every prime, integrality at primes `p > K`, and the outer-range -bound `γ_p^out` of (4.14)/Proposition 4.3 at every admissible prime (it is attained exactly at -most of them). +The checked proof uses only `propext`, `Classical.choice`, and `Quot.sound`. diff --git a/Solution.lean b/Solution.lean new file mode 100644 index 0000000..31e00a0 --- /dev/null +++ b/Solution.lean @@ -0,0 +1,8 @@ +import Apery.Main + +namespace RiemannZetaValues + +theorem irrational_five : ∃ x, Irrational x ∧ riemannZeta 5 = x := by + exact Apery.irrational_five + +end RiemannZetaValues diff --git a/config.json b/config.json new file mode 100644 index 0000000..ae91b7c --- /dev/null +++ b/config.json @@ -0,0 +1,7 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": ["RiemannZetaValues.irrational_five"], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"], + "enable_nanoda": false +} diff --git a/formalization.yaml b/formalization.yaml new file mode 100644 index 0000000..d7cde59 --- /dev/null +++ b/formalization.yaml @@ -0,0 +1,86 @@ +# yaml-language-server: $schema=https://raw.githubusercontent.com/mathlib-initiative/formalization.yaml/main/schema/formalization.schema.json +version: "v0.4" + +project: + name: "Irrationality of ζ(5)" + description: >- + A Lean formalization of the irrationality of the Riemann zeta value ζ(5), + following A. Fauzan's preprint and the corresponding Formal Conjectures + statement. The proof supplies the Comparator challenge theorem + RiemannZetaValues.irrational_five. + authors: ["Moritz Firsching"] + responsible_maintainers: ["Moritz Firsching"] + license: "Apache-2.0" + +repository: + role: "substantive-development" + +sources: + - title: "Formal Conjectures: Particular values of the Riemann zeta function" + authors: ["The Formal Conjectures Authors"] + id: "https://github.com/google-deepmind/formal-conjectures/blob/2db01438fda960163f58ff2c2385b52e53f56dd2/FormalConjectures/Wikipedia/RiemannZetaValues.lean" + type: "formalization repository" + location: "RiemannZetaValues.irrational_five" + relationship: "formalizes" + note: >- + Challenge.lean copies this theorem statement verbatim from the pinned + Formal Conjectures revision. + - title: "ζ(5) is irrational" + authors: ["A. Fauzan"] + type: "preprint" + location: "Theorem 1.1" + relationship: "formalizes" + note: "The proof development follows the preprint dated 17 September 2026." + - title: "Particular values of the Riemann zeta function" + authors: ["Wikipedia contributors"] + id: "https://en.wikipedia.org/wiki/Particular_values_of_the_Riemann_zeta_function" + type: "encyclopedia article" + relationship: "background" + +classification: + arxiv: ["math.NT"] + msc2020: ["11M06", "11J72"] + +status: + scope: >- + Proves the Formal Conjectures statement that ζ(5) is irrational and + verifies the proof independently through Lean's kernel and Comparator. + sorry_count: 0 + sorry_in_definitions: 0 + axioms: ["propext", "Quot.sound", "Classical.choice"] + main_results: + - declaration: "RiemannZetaValues.irrational_five" + file: "Solution.lean" + sorry_count: 0 + axioms: ["propext", "Quot.sound", "Classical.choice"] + comparator_config: "config.json" + literature_dependencies: [] + +automation: + methods: + - method: "manual" + framework: "Lean 4 and Mathlib" + tool_setup: >- + The proof development uses the pinned Lean v4.33.1 toolchain, + Mathlib, and the pinned PrimeNumberTheoremAnd dependency. Comparator + and Landrun are pinned in .github/workflows/comparator.yml. + notes: >- + The Comparator wrapper and metadata are maintained alongside the proof + development; the challenge deliberately contains one sorry placeholder. + +fidelity: + divergences: >- + The challenge theorem is the same proposition as the Formal Conjectures + declaration, but omits Formal Conjectures-only category and answer + attributes because the standalone challenge imports Mathlib directly. + +review: + status: "self-assessed" + reviewers: ["Moritz Firsching"] + notes: >- + The proof is checked by the existing Lean build and the Comparator CI + workflow against the standard permitted axiom whitelist. + +acknowledgements: >- + This project uses Lean, Mathlib, PrimeNumberTheoremAnd, Formal Conjectures, + and leanprover/comparator. diff --git a/lakefile.toml b/lakefile.toml index a58edb9..8133827 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -1,7 +1,7 @@ name = "Apery" version = "0.1.0" keywords = ["math"] -defaultTargets = ["Apery"] +defaultTargets = ["Apery", "Challenge", "Solution"] [leanOptions] pp.unicode.fun = true # pretty-prints `fun a ↦ b` @@ -17,6 +17,12 @@ rev = "v4.33.1" [[lean_lib]] name = "Apery" +[[lean_lib]] +name = "Challenge" + +[[lean_lib]] +name = "Solution" + [[require]] name = "PrimeNumberTheoremAnd" git = "https://github.com/mo271/PrimeNumberTheoremAnd" From d8822f0bf277710df22782dc612b2da8a8550324 Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 23 Sep 2026 14:43:28 +0000 Subject: [PATCH 2/4] Align Lean toolchain with Comparator --- README.md | 2 +- formalization.yaml | 7 ++++--- lake-manifest.json | 4 ++-- lakefile.toml | 2 +- lean-toolchain | 2 +- 5 files changed, 9 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index b6a0db7..7292176 100644 --- a/README.md +++ b/README.md @@ -22,7 +22,7 @@ The proof follows A. Fauzan’s preprint, *ζ(5) is irrational* (17 September ## Dependencies - [Mathlib](https://github.com/leanprover-community/mathlib4), pinned to - `v4.33.1`. + `f385f9fd18abed332ebcd3df239cb357e264aceb` for Lean `v4.34.0-rc1`. - [PrimeNumberTheoremAnd](https://github.com/mo271/PrimeNumberTheoremAnd), imported by `Apery/PNT.lean` for the prime number theorem. - [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) diff --git a/formalization.yaml b/formalization.yaml index d7cde59..f9badec 100644 --- a/formalization.yaml +++ b/formalization.yaml @@ -61,9 +61,10 @@ automation: - method: "manual" framework: "Lean 4 and Mathlib" tool_setup: >- - The proof development uses the pinned Lean v4.33.1 toolchain, - Mathlib, and the pinned PrimeNumberTheoremAnd dependency. Comparator - and Landrun are pinned in .github/workflows/comparator.yml. + The proof development uses the pinned Lean v4.34.0-rc1 toolchain, + the pinned Mathlib revision, and the pinned PrimeNumberTheoremAnd + dependency. Comparator and Landrun are pinned in + .github/workflows/comparator.yml. notes: >- The Comparator wrapper and metadata are maintained alongside the proof development; the challenge deliberately contains one sorry placeholder. diff --git a/lake-manifest.json b/lake-manifest.json index 02f659c..f587812 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,10 +15,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0df444a360eaa60ab8c11dca51a86af692955474", + "rev": "f385f9fd18abed332ebcd3df239cb357e264aceb", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.1", + "inputRev": "f385f9fd18abed332ebcd3df239cb357e264aceb", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/b-mehta/PrimeCert", diff --git a/lakefile.toml b/lakefile.toml index 8133827..734787d 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -12,7 +12,7 @@ maxSynthPendingDepth = 3 [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.33.1" +rev = "f385f9fd18abed332ebcd3df239cb357e264aceb" [[lean_lib]] name = "Apery" diff --git a/lean-toolchain b/lean-toolchain index a8afa7d..75def60 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.1 +leanprover/lean4:v4.34.0-rc1 From 89e9ff833a6dffe8620028c70182386de65603b5 Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 23 Sep 2026 14:48:21 +0000 Subject: [PATCH 3/4] Use Mathlib-compatible dependency order --- lake-manifest.json | 110 ++++++++++++++++++++++----------------------- lakefile.toml | 10 ++--- 2 files changed, 60 insertions(+), 60 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index f587812..7c5c6f6 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,17 +1,7 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/mo271/PrimeNumberTheoremAnd", - "type": "git", - "subDir": null, - "scope": "", - "rev": "04d81b2a68ea3548b9990813fdc463c78511f412", - "name": "PrimeNumberTheoremAnd", - "manifestFile": "lake-manifest.json", - "inputRev": "04d81b2a68ea3548b9990813fdc463c78511f412", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4", + [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", @@ -21,51 +11,21 @@ "inputRev": "f385f9fd18abed332ebcd3df239cb357e264aceb", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/b-mehta/PrimeCert", + {"url": "https://github.com/mo271/PrimeNumberTheoremAnd", "type": "git", "subDir": null, "scope": "", - "rev": "916ee9c35a57af128d5089a69172415051e700ca", - "name": "PrimeCert", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/alerad/leancert.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "621a43d7cf21f87872392a01e874f2f1dbddc926", - "name": "leancert", + "rev": "04d81b2a68ea3548b9990813fdc463c78511f412", + "name": "PrimeNumberTheoremAnd", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.1", - "inherited": true, + "inputRev": "04d81b2a68ea3548b9990813fdc463c78511f412", + "inherited": false, "configFile": "lakefile.toml"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", - "name": "checkdecls", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hanwenzhu/LeanArchitect.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0f5bc0209ae02a7fb0cfe7d113d4094542cee221", - "name": "LeanArchitect", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "rev": "99e8adeea3c3cd86b6b79ba01a1383bf2d31d055", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -115,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,20 +85,60 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "rev": "9a86b38593ce6411eb26cc53e512392e12cd8939", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/b-mehta/PrimeCert", + "type": "git", + "subDir": null, + "scope": "", + "rev": "916ee9c35a57af128d5089a69172415051e700ca", + "name": "PrimeCert", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/alerad/leancert.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "621a43d7cf21f87872392a01e874f2f1dbddc926", + "name": "leancert", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.1", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/PatrickMassot/checkdecls.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", + "name": "checkdecls", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/hanwenzhu/LeanArchitect.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0f5bc0209ae02a7fb0cfe7d113d4094542cee221", + "name": "LeanArchitect", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "Apery", diff --git a/lakefile.toml b/lakefile.toml index 734787d..2f3b7c9 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -9,11 +9,6 @@ relaxedAutoImplicit = false weak.linter.mathlibStandardSet = true maxSynthPendingDepth = 3 -[[require]] -name = "mathlib" -scope = "leanprover-community" -rev = "f385f9fd18abed332ebcd3df239cb357e264aceb" - [[lean_lib]] name = "Apery" @@ -27,3 +22,8 @@ name = "Solution" name = "PrimeNumberTheoremAnd" git = "https://github.com/mo271/PrimeNumberTheoremAnd" rev = "04d81b2a68ea3548b9990813fdc463c78511f412" + +[[require]] +name = "mathlib" +scope = "leanprover-community" +rev = "f385f9fd18abed332ebcd3df239cb357e264aceb" From d38a2888708e86eb80e16a6cf9170f8a824c7d78 Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 23 Sep 2026 16:05:56 +0000 Subject: [PATCH 4/4] Allow time for the Comparator clean build --- .github/workflows/comparator.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/comparator.yml b/.github/workflows/comparator.yml index aaf13ca..d053b98 100644 --- a/.github/workflows/comparator.yml +++ b/.github/workflows/comparator.yml @@ -11,7 +11,9 @@ permissions: jobs: comparator: runs-on: ubuntu-24.04 - timeout-minutes: 45 + # The solution imports the complete Apery formalisation, whose first + # clean build on a GitHub runner takes longer than the default 45 minutes. + timeout-minutes: 120 steps: - uses: actions/checkout@v4