diff --git a/gnu/packages/maths.scm b/gnu/packages/maths.scm
index 9b2b052..226db7c 100644
--- a/gnu/packages/maths.scm
+++ b/gnu/packages/maths.scm
@@ -29,6 +29,7 @@
   #:use-module ((gnu packages gettext)
                 #:renamer (symbol-prefix-proc 'gnu:))
   #:use-module (gnu packages gcc)
+  #:use-module (gnu packages gtk)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages perl)
   #:use-module (gnu packages pkg-config)
@@ -200,3 +201,30 @@ text, Postscript, PDF or HTML.")
 problems in numerical linear algebra.")
     (license (license:bsd-style "file://LICENSE"
                                 "See LICENSE in the distribution."))))
+
+(define-public aris
+  (package
+    (name "aris")
+    (version "2.1.1")
+    (source
+     (origin
+      (method url-fetch)
+      (uri (string-append "mirror://gnu/aris/aris-"
+                          version ".tar.bz2"))
+      (sha256
+       (base32
+        "08vw43qkmnsd2xjfwfkvp6njar8cdns0hbzav6sxgvbr08778cgp"))))
+    (build-system gnu-build-system)
+    (inputs `(("pkg-config" ,pkg-config)
+              ("gtk+" ,gtk+-2)
+              ("libxml2", libxml2)))
+    (home-page "https://gnu.org/software/aris")
+    (synopsis "Natural deduction first-order logic interface")
+    (description
+     "Aris is a program for performing logical proofs.  It supports
+propositional and predicate logic, as well as Boolean algebra and
+arithmetical logic.  In addition to its predefined inference and equivalence
+rules, Aris also supports references to older proofs. Its use of standard
+logical symbols and its natural deduction interface make it easy to use for
+beginners.")
+    (license license:gpl3+)))