Add Comparator in the CI

.github/workflows/comparator.yml

@@ -0,0 +1,66 @@
+name: Comparator
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  comparator:
+    runs-on: ubuntu-24.04
+    # The solution imports the complete Apery formalisation, whose first
+    # clean build on a GitHub runner takes longer than the default 45 minutes.
+    timeout-minutes: 300
+
+    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'

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

README.md

@@ -8,9 +8,16 @@ theorem irrational_five : ∃ x, Irrational x ∧ riemannZeta 5 = x
 
 following the preprint [ζ(5) is irrational](https://zenodo.org/records/22826419). (A. Fauzan, 17 September 2026).
 
-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`.
+Toolchain: Lean `v4.34.0-rc1`, Mathlib pinned to commit `f385f9fd`. The prime number theorem
+`θ ~ id` comes from [PrimeNumberTheoremAnd](https://github.com/mo271/PrimeNumberTheoremAnd)
+(pinned to commit `04d81b2a`), imported in `Apery/PNT.lean`.
+
+`Challenge.lean` holds 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),
+and `Solution.lean` discharges it from `Apery.irrational_five`. The CI workflow
+`.github/workflows/comparator.yml` runs [Comparator](https://github.com/leanprover/comparator)
+on `config.json`, checking that `Solution.lean` really proves the challenge statement and that
+the proof depends only on `propext`, `Classical.choice`, and `Quot.sound`.
 
 License: Apache 2.0 (see `LICENSE`), as for Mathlib and PrimeNumberTheoremAnd.
 

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

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
+}

formalization.yaml

@@ -0,0 +1,87 @@
+# 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.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.
+
+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.