diff --git a/pkgs/development/coq-modules/mathcomp-apery/default.nix b/pkgs/development/coq-modules/mathcomp-apery/default.nix
new file mode 100644
index 00000000000..69511693876
--- /dev/null
+++ b/pkgs/development/coq-modules/mathcomp-apery/default.nix
@@ -0,0 +1,23 @@
+{ coq, mkCoqDerivation, mathcomp, coqeal, mathcomp-real-closed,
+  mathcomp-bigenough, mathcomp-zify, mathcomp-algebra-tactics,
+  lib, version ? null }:
+
+mkCoqDerivation {
+
+  pname = "apery";
+
+  inherit version;
+  defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ]  [
+      { cases = [ (range "8.13" "8.16") (isGe "1.12.0") ]; out = "1.0.2"; }
+    ] null;
+
+  release."1.0.2".sha256 = "sha256-llxyMKYvWUA7fyroG1S/jtpioAoArmarR1edi3cikcY=";
+
+  propagatedBuildInputs = [ mathcomp.field coqeal mathcomp-real-closed
+    mathcomp-bigenough mathcomp-zify mathcomp-algebra-tactics ];
+
+  meta = {
+    description = "A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational";
+    license = lib.licenses.cecill-c;
+  };
+}
diff --git a/pkgs/top-level/coq-packages.nix b/pkgs/top-level/coq-packages.nix
index 87291ca8f3d..3aa08807f79 100644
--- a/pkgs/top-level/coq-packages.nix
+++ b/pkgs/top-level/coq-packages.nix
@@ -77,6 +77,7 @@ let
       mathcomp-character = self.mathcomp.character;
       mathcomp-abel = callPackage ../development/coq-modules/mathcomp-abel {};
       mathcomp-analysis = callPackage ../development/coq-modules/mathcomp-analysis {};
+      mathcomp-apery = callPackage ../development/coq-modules/mathcomp-apery {};
       mathcomp-classical = self.mathcomp-analysis.classical;
       mathcomp-finmap = callPackage ../development/coq-modules/mathcomp-finmap {};
       mathcomp-bigenough = callPackage ../development/coq-modules/mathcomp-bigenough {};