diff --git a/gnu/packages/lean.scm b/gnu/packages/lean.scm
index d1e74adb83..ee64e23c8f 100644
--- a/gnu/packages/lean.scm
+++ b/gnu/packages/lean.scm
@@ -70,7 +70,7 @@
            python-wrapper
            tzdata-for-tests))
     (inputs
-     (list cadical gmp libuv llvm))
+     (list cadical-2.1 gmp libuv llvm))
     (arguments
      (list
       #:make-flags
diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 530be30778..2b4503c172 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -9944,6 +9944,21 @@ also included.")
 clause learning.")
     (license license:expat)))
 
+(define-public cadical-2.1
+  (package
+    (inherit cadical)
+    (name "cadical")
+    (version "2.1.3")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://github.com/arminbiere/cadical")
+                    (commit (string-append "rel-" version))))
+              (file-name (git-file-name name version))
+              (patches (search-patches "cadical-add-shared-library.patch"))
+              (sha256 (base32
+                       "1gl0xd6zyxb127w8k0mps9m2izaqb7im7j91by4lkknmm7xhwyav"))))))
+
 (define-public cadiback
   (let ((commit "789329d8fcda851085ed72f1b07d8c3f46243b8a")
         (revision "1"))