diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheory.scala b/lisa-utils/src/test/scala/lisa/test/TestTheory.scala
new file mode 100644
index 0000000000000000000000000000000000000000..caf62e802b55f0385512ed54b40ae9245cd4c813
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/test/TestTheory.scala
@@ -0,0 +1,3 @@
+package lisa.test
+
+object TestTheory extends TestTheoryAxioms {}
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala b/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala
new file mode 100644
index 0000000000000000000000000000000000000000..151fdbb13bad568639c7cc65dd9d32dae8d45bb8
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/test/TestTheoryAxioms.scala
@@ -0,0 +1,31 @@
+package lisa.test
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.utils.Helpers.{_, given}
+
+trait TestTheoryAxioms {
+  final val p1 = ConstantPredicateLabel("p1", 1)
+  final val p2 = ConstantPredicateLabel("p2", 1)
+  final val f1 = ConstantFunctionLabel("f1", 1)
+  final val fixedElement = ConstantFunctionLabel("fixed_element", 0)
+  final val anotherFixed = ConstantFunctionLabel("another_element", 0)
+
+  val runningTestTheory = new RunningTheory()
+  runningTestTheory.addSymbol(p1)
+  runningTestTheory.addSymbol(p2)
+  runningTestTheory.addSymbol(f1)
+  runningTestTheory.addSymbol(fixedElement)
+  runningTestTheory.addSymbol(anotherFixed)
+
+  private final val x = VariableLabel("x")
+  final val p1_implies_p2: Formula = forall(x, p1(x) ==> p2(x))
+  final val ax2 = p1(fixedElement())
+  final val same_fixed = fixedElement() === anotherFixed()
+  final val fixed_point = forall(x, (f1(x) === fixedElement()) <=> (x === fixedElement()))
+
+  assert(runningTestTheory.addAxiom("p1_implies_p2", p1_implies_p2), "p1_implies_p2")
+  assert(runningTestTheory.addAxiom("A2", ax2), "ax2")
+  assert(runningTestTheory.addAxiom("same_fixed", same_fixed), "same fixed")
+  assert(runningTestTheory.addAxiom("fixed_point", fixed_point), "fixed point")
+}
diff --git a/lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala b/lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2431591566d8735ef056e47994f4f3115a6e0378
--- /dev/null
+++ b/lisa-utils/src/test/scala/lisa/test/TestTheoryLibrary.scala
@@ -0,0 +1,5 @@
+package lisa.test
+
+object TestTheoryLibrary extends lisa.utils.Library(TestTheory.runningTestTheory) {
+  export TestTheory.*
+}