diff --git a/.github/workflows/comparator.yml b/.github/workflows/comparator.yml
new file mode 100644
index 0000000..52f9cd9
--- /dev/null
+++ b/.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'
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 cfc8764..ebbbe2c 100644
--- a/README.md
+++ b/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.
 
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..f9badec
--- /dev/null
+++ b/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.
diff --git a/lake-manifest.json b/lake-manifest.json
index 02f659c..7c5c6f6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,71 +1,31 @@
 {"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",
-   "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",
+  {"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 8e91da7..3db060d 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,15 +17,21 @@ weak.linter.unreachableTactic = false
 weak.linter.unnecessarySeqFocus = false
 maxSynthPendingDepth = 3
 
-[[require]]
-name = "mathlib"
-scope = "leanprover-community"
-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"
 rev = "04d81b2a68ea3548b9990813fdc463c78511f412"
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "f385f9fd18abed332ebcd3df239cb357e264aceb"
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