From aef926bde615b0b4725e024476f85ee9f54693da Mon Sep 17 00:00:00 2001
From: SimonGuilloud <simon.guilloud@bluewin.ch>
Date: Mon, 20 Nov 2023 11:38:23 +0100
Subject: [PATCH] Save proofs (#187)

    -Add ids to terms like for formulas
    -Add serialization of proofs. Theorems can be serialized to binary files and loaded back on later run.
    -On my machine, running everything up to Recursion.scala takes 19s instead of 24s.
    -Does no hash consing, but simple optimizations to proof size (remove consecutive rewrites, flatten subproofs)
    -Cleans up the distinction between fullName (with the whole path, should be unique) and name (just the last part, possibly duplicate across different files/domains).
    -Good completion of documentation in WithTheorems
    -checkProofs does not print proofs of more thant 100 steps now.
    -fixed an indexing bug in ShrinkProof.flattenProof
    -Suite of tests for serialization, export then load a collection of theorems.
    -Push suite of tests for Tableaux tactic that were missing.
---
 .../lisa/kernel/fol/CommonDefinitions.scala   |   2 +-
 .../lisa/kernel/fol/TermDefinitions.scala     |   8 +
 .../main/scala/lisa/prooflib/BasicMain.scala  |   4 +
 .../main/scala/lisa/prooflib/Library.scala    |   2 +
 .../scala/lisa/prooflib/ProofsHelpers.scala   |  42 +-
 .../scala/lisa/prooflib/WithTheorems.scala    | 284 ++++++-
 .../main/scala/lisa/utils/KernelHelpers.scala |   6 +-
 .../main/scala/lisa/utils/LisaException.scala |   3 +
 .../main/scala/lisa/utils/ProofsShrink.scala  |  11 +-
 .../main/scala/lisa/utils/Serialization.scala | 721 ++++++++++++++++++
 .../lisa/test/utils/ProofTacticTestLib.scala  |   2 +-
 .../lisa/settheory/SetTheoryTGAxioms.scala    |   1 -
 .../lisa/settheory/SetTheoryZAxioms.scala     |  18 +-
 .../lisa/settheory/SetTheoryZFAxioms.scala    |   1 -
 .../scala/lisa/automation/TableauTest.scala   | 130 ++++
 .../lisa/utilities/SerializationTest.scala    | 187 +++++
 16 files changed, 1355 insertions(+), 67 deletions(-)
 create mode 100644 lisa-utils/src/main/scala/lisa/utils/Serialization.scala
 create mode 100644 src/test/scala/lisa/automation/TableauTest.scala
 create mode 100644 src/test/scala/lisa/utilities/SerializationTest.scala

diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
index 8a9d040f..6f65ffdf 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -26,7 +26,7 @@ private[fol] trait CommonDefinitions {
 
     val counterSeparator: Char = '_'
     val delimiter: Char = '`'
-    val forbiddenChars: Set[Char] = ("()[]{}?" + delimiter + counterSeparator).toSet
+    val forbiddenChars: Set[Char] = ("()[]{}?,;" + delimiter + counterSeparator).toSet
     def isValidIdentifier(s: String): Boolean = s.forall(c => !forbiddenChars.contains(c) && !c.isWhitespace)
   }
 
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
index 58d7ad10..6e1b9b5c 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -38,6 +38,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
    */
   sealed case class Term(label: TermLabel, args: Seq[Term]) extends TreeWithLabel[TermLabel] {
     require(label.arity == args.size)
+    val uniqueNumber: Long = TermCounters.getNewId
     val arity: Int = label.arity
 
     override def freeVariables: Set[VariableLabel] = label match {
@@ -55,6 +56,13 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
     }
     override def freeSchematicTermLabels: Set[SchematicTermLabel] = schematicTermLabels
   }
+  private object TermCounters {
+    var totalNumberOfTerms: Long = 0
+    def getNewId: Long = {
+      totalNumberOfTerms += 1
+      totalNumberOfTerms
+    }
+  }
 
   /**
    * A VariableTerm is exactly an arity-0 term whose label is a variable label, but we provide specific constructors and destructors.
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala
index e22a1113..f7bcd5f8 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala
@@ -1,6 +1,10 @@
 package lisa.prooflib
 
+import lisa.utils.Serialization.*
+
 trait BasicMain {
+  val library: Library
+
   private val realOutput: String => Unit = println
 
   given om: OutputManager = new OutputManager {
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
index 1b57fa94..73cc6096 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
@@ -30,6 +30,8 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro
 
   var last: Option[JUSTIFICATION] = None
 
+  var _withCache: Boolean = false
+
   val knownDefs: scala.collection.mutable.Map[F.ConstantLabel[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
 
   def addSymbol(s: F.ConstantFunctionLabel[?] | F.ConstantPredicateLabel[?] | F.Constant): Unit = {
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
index 5fe1901e..23ba931d 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
@@ -148,17 +148,17 @@ trait ProofsHelpers {
   )
   class definitionWithVars[N <: Arity](val args: Variable *** N) {
 
-    // inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(t: Term) = simpleDefinition(lambda(args, t, args.length))
-    // inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(f: Formula) = predicateDefinition(lambda(args, f, args.length))
+    // inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(t: Term) = simpleDefinition(lambda(args, t, args.length))
+    // inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(f: Formula) = predicateDefinition(lambda(args, f, args.length))
 
-    inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(t: The): ConstantFunctionLabelOfArity[N] =
-      FunctionDefinition[N](name.value, name.value, line.value, file.value)(args.toSeq, t.out, t.f, t.just).label
+    inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(t: The): ConstantFunctionLabelOfArity[N] =
+      FunctionDefinition[N](name.value, line.value, file.value)(args.toSeq, t.out, t.f, t.just).label
 
-    inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(term: Term): ConstantFunctionLabelOfArity[N] =
-      SimpleFunctionDefinition[N](name.value, name.value, line.value, file.value)(lambda(args.toSeq, term).asInstanceOf).label
+    inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(term: Term): ConstantFunctionLabelOfArity[N] =
+      SimpleFunctionDefinition[N](name.value, line.value, file.value)(lambda(args.toSeq, term).asInstanceOf).label
 
-    inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(formula: Formula): ConstantPredicateLabelOfArity[N] =
-      PredicateDefinition[N](name.value, name.value, line.value, file.value)(lambda(args.toSeq, formula).asInstanceOf).label
+    inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(formula: Formula): ConstantPredicateLabelOfArity[N] =
+      PredicateDefinition[N](name.value, line.value, file.value)(lambda(args.toSeq, formula).asInstanceOf).label
 
   }
 
@@ -172,13 +172,13 @@ trait ProofsHelpers {
   /**
    * Allows to make definitions "by unique existance" of a function symbol
    */
-  class FunctionDefinition[N <: F.Arity](using om: OutputManager)(val name: String, val fullName: String, line: Int, file: String)(
+  class FunctionDefinition[N <: F.Arity](using om: OutputManager)(val fullName: String, line: Int, file: String)(
       val vars: Seq[F.Variable],
       val out: F.Variable,
       val f: F.Formula,
       j: JUSTIFICATION
   ) extends DEFINITION(line, file) {
-    def repr: String =
+    override def repr: String =
       s" ${if (withSorry) " Sorry" else ""} Definition of function symbol ${label(vars)} := the ${out} such that ${(out === label(vars)) <=> f})\n"
 
     // val expr = LambdaExpression[Term, Formula, N](vars, f, valueOf[N])
@@ -284,33 +284,25 @@ trait ProofsHelpers {
   /**
    * Allows to make definitions "by equality" of a function symbol
    */
-  class SimpleFunctionDefinition[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(
+  class SimpleFunctionDefinition[N <: F.Arity](using om: OutputManager)(fullName: String, line: Int, file: String)(
       val lambda: LambdaExpression[Term, Term, N],
       out: F.Variable,
       j: JUSTIFICATION
-  ) extends FunctionDefinition[N](name, fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {
-    override def repr: String =
-      s" Definition of function symbol ${label(lambda.bounds.asInstanceOf)} := ${lambda.body}${if (j.withSorry) " (!! Relies on Sorry)" else ""}\n"
-
-  }
+  ) extends FunctionDefinition[N](fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {}
 
   object SimpleFunctionDefinition {
-    def apply[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(lambda: LambdaExpression[Term, Term, N]): SimpleFunctionDefinition[N] = {
-
-      // THM(using om: OutputManager)(val statement: F.Sequent, val fullName: String, line: Int, file: String, val kind: TheoremKind)(computeProof: Proof ?=> Unit)
+    def apply[N <: F.Arity](using om: OutputManager)(fullName: String, line: Int, file: String)(lambda: LambdaExpression[Term, Term, N]): SimpleFunctionDefinition[N] = {
       val intName = "definition_" + fullName
       val out = Variable(freshId(lambda.allSchematicLabels.map(_.id), "y"))
-      val defThm = new THM(F.ExistsOne(out, out === lambda.body), intName, line, file, InternalStatement)({
+      val defThm = THM(F.ExistsOne(out, out === lambda.body), intName, line, file, InternalStatement)({
         have(SimpleDeducedSteps.simpleFunctionDefinition(lambda, out))
       })
-      new SimpleFunctionDefinition[N](name, fullName, line, file)(lambda, out, defThm)
+      new SimpleFunctionDefinition[N](fullName, line, file)(lambda, out, defThm)
     }
   }
 
-  class PredicateDefinition[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(val lambda: LambdaExpression[Term, Formula, N])
-      extends DEFINITION(line, file) {
-    override def repr: String =
-      s" Definition of predicate symbol ${label(lambda.bounds.asInstanceOf)} := ${lambda.body}"
+  class PredicateDefinition[N <: F.Arity](using om: OutputManager)(val fullName: String, line: Int, file: String)(val lambda: LambdaExpression[Term, Formula, N]) extends DEFINITION(line, file) {
+
     lazy val vars: Seq[F.Variable] = lambda.bounds.asInstanceOf
     val arity = lambda.arity
 
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index 27a9aa68..2fa698e2 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -18,12 +18,25 @@ import scala.collection.mutable.Stack as stack
 trait WithTheorems {
   library: Library =>
 
+  /**
+   * The main builder for proofs. It is a mutable object that can be used to build a proof step by step.
+   * It is used either to construct a theorem/lemma ([[BaseProof]]) or to construct a subproof ([[InnerProof]]).
+   * We can add proof tactics to it producing intermediate results. In the end, obtain a [[K.SCProof]] from it.
+   *
+   * @param assump list of starting assumptions, usually propagated from outer proofs.
+   */
   sealed abstract class Proof(assump: List[F.Formula]) {
     val possibleGoal: Option[F.Sequent]
     type SelfType = this.type
     type OutsideFact >: JUSTIFICATION
     type Fact = ProofStep | InstantiatedFact | OutsideFact | Int
 
+    /**
+     * A proven fact (from a previously proven step, a theorem or a definition) with specific instantiations of free variables.
+     *
+     * @param fact The base fact
+     * @param insts The instantiation of free variables
+     */
     case class InstantiatedFact(
         fact: Fact,
         insts: Seq[F.SubstPair] /*,
@@ -44,8 +57,21 @@ trait WithTheorems {
     private var assumptions: List[F.Formula] = assump
     private var discharges: List[Fact] = Nil
 
+    /**
+     * the theorem that is being proved (paritally, if subproof) by this proof.
+     *
+     * @return The theorem
+     */
     def owningTheorem: THM
 
+    /**
+     * A proof step, containing a high level ProofTactic and the corresponding K.SCProofStep. If the tactic produce more than one
+     * step, they must be encapsulated in a subproof. Usually constructed with [[ValidProofTactic.validate]]
+     *
+     * @param judgement The result of the tactic
+     * @param scps The corresponding [[K.SCProofStep]]
+     * @param position The position of the step in the proof
+     */
     case class ProofStep private (judgement: ValidProofTactic, scps: K.SCProofStep, position: Int) {
       val bot: F.Sequent = judgement.bot
       def innerBot: K.Sequent = scps.bot
@@ -69,6 +95,10 @@ trait WithTheorems {
 
       }
     }
+
+    /**
+     * A proof step can be constructed from a succesfully executed tactic
+     */
     def newProofStep(judgement: ValidProofTactic): ProofStep =
       ProofStep.newProofStep(judgement)
 
@@ -91,6 +121,11 @@ trait WithTheorems {
       instantiatedFacts = (instFact, steps.length - 1) :: instantiatedFacts
     }
 
+    /**
+     * Add an assumption the the proof, i.e. a formula that is automatically on the left side of the sequent.
+     *
+     * @param f
+     */
     def addAssumption(f: F.Formula): Unit = {
       if (!assumptions.contains(f)) assumptions = f :: assumptions
     }
@@ -123,6 +158,11 @@ trait WithTheorems {
      */
     def getDischarges: List[Fact] = discharges
 
+    /**
+     * Produce the low level [[K.SCProof]] corresponding to the proof. Automatically eliminates any formula in the discharges that is still left of the sequent.
+     *
+     * @return
+     */
     def toSCProof: K.SCProof = {
       import lisa.utils.KernelHelpers.{-<<, ->>}
       val finalSteps = discharges.foldLeft(steps.map(_.scps))((cumul, next) => {
@@ -136,6 +176,12 @@ trait WithTheorems {
       K.SCProof(finalSteps.reverse.toIndexedSeq, getImports.map(of => of._2.underlying).toIndexedSeq)
     }
 
+    /**
+     * For a fact, returns the sequent that the fact proove and the position of the fact in the proof.
+     *
+     * @param fact Any fact, possibly instantiated, belonging to the proof
+     * @return its proven sequent and position
+     */
     def sequentAndIntOfFact(fact: Fact): (F.Sequent, Int) = fact match {
       case i: Int =>
         (
@@ -195,10 +241,22 @@ trait WithTheorems {
     def getSequent(f: Fact): F.Sequent = sequentOfFact(f)
     def mostRecentStep: ProofStep = steps.head
 
+    /**
+     * The number of steps in the proof. This is not the same as the number of steps in the corresponding [[K.SCProof]].
+     * This also does not count the number of steps in the subproof.
+     *
+     * @return
+     */
     def length: Int = steps.length
 
+    /**
+     * The set of symbols that can't be instantiated because they are free in an assumption.
+     */
     def lockedSymbols: Set[F.SchematicLabel[?]] = assumptions.toSet.flatMap(f => f.freeSchematicLabels.toSet)
 
+    /**
+     * Used to "lift" the type of a justification when the compiler can't infer it.
+     */
     def asOutsideFact(j: JUSTIFICATION): OutsideFact
 
     @nowarn("msg=.*It would fail on pattern case: _: InnerProof.*")
@@ -207,6 +265,10 @@ trait WithTheorems {
       case _: BaseProof => 0
     }
 
+    /**
+     * Create a subproof inside the current proof. The subproof will have the same assumptions as the current proof.
+     * Can have a goal known in advance (usually for a user-written subproof) or not (usually for a tactic-generated subproof).
+     */
     def newInnerProof(possibleGoal: Option[F.Sequent]) = new InnerProof(possibleGoal)
     final class InnerProof(val possibleGoal: Option[F.Sequent]) extends Proof(this.getAssumptions) {
       val parent: Proof.this.type = Proof.this
@@ -262,19 +324,58 @@ trait WithTheorems {
     }
   }
 
-  sealed class BaseProof(val owningTheorem: THM) extends Proof(Nil) {
+  /**
+   * Top-level instance of [[Proof]] directly proving a theorem
+   */
+  sealed class BaseProof(val owningTheorem: THMFromProof) extends Proof(Nil) {
     val goal: F.Sequent = owningTheorem.goal
     val possibleGoal: Option[F.Sequent] = Some(goal)
     type OutsideFact = JUSTIFICATION
     override inline def asOutsideFact(j: JUSTIFICATION): OutsideFact = j
 
     override def sequentOfOutsideFact(j: JUSTIFICATION): F.Sequent = j.statement
+
+    def justifications: List[JUSTIFICATION] = getImports.map(_._1)
   }
 
+  /**
+   * Abstract class representing theorems, axioms and different kinds of definitions. Corresponds to a [[theory.Justification]].
+   */
   sealed abstract class JUSTIFICATION {
+
+    /**
+     * A pretty representation of the justification
+     */
     def repr: String
+
+    /**
+     * The inner kernel justification
+     */
     def innerJustification: theory.Justification
+
+    /**
+     * The sequent that the justification proves
+     */
     def statement: F.Sequent
+
+    /**
+     * The complete name of the justification. Two justifications should never have the same full name. Typically, path is used to disambiguate.
+     */
+    def fullName: String
+
+    /**
+     * The short name of the justification (without the path).
+     */
+    val name: String = fullName.split("\\.").last
+
+    /**
+     * The "owning" object of the justification. Typically, the package/object in which it is defined.
+     */
+    val owner = fullName.split("\\.").dropRight(1).mkString(".")
+
+    /**
+     * Returns if the statement is unconditionaly proven or if it depends on some sorry step (including in the other justifications it relies on)
+     */
     def withSorry: Boolean = innerJustification match {
       case thm: theory.Theorem => thm.withSorry
       case fd: theory.FunctionDefinition => fd.withSorry
@@ -283,7 +384,10 @@ trait WithTheorems {
     }
   }
 
-  class AXIOM(innerAxiom: theory.Axiom, val axiom: F.Formula, val name: String) extends JUSTIFICATION {
+  /**
+   * A Justification, corresponding to [[K.Axiom]]
+   */
+  class AXIOM(innerAxiom: theory.Axiom, val axiom: F.Formula, val fullName: String) extends JUSTIFICATION {
     def innerJustification: theory.Axiom = innerAxiom
     val statement: F.Sequent = F.Sequent(Set(), Set(axiom))
     if (statement.underlying != theory.sequentFromJustification(innerAxiom)) {
@@ -292,40 +396,160 @@ trait WithTheorems {
     def repr: String = s" Axiom $name := $axiom"
   }
 
-  def Axiom(name: String, axiom: F.Formula): AXIOM = {
-    val ax: Option[theory.Axiom] = theory.addAxiom(name, axiom.underlying)
+  /**
+   * Introduces a new axiom in the theory.
+   *
+   * @param fullName The name of the axiom, including the path. Usually fetched automatically by the compiler.
+   * @param axiom The axiomatized formula.
+   * @return
+   */
+  def Axiom(using fullName: sourcecode.FullName)(axiom: F.Formula): AXIOM = {
+    val ax: Option[theory.Axiom] = theory.addAxiom(fullName.value, axiom.underlying)
     ax match {
-      case None => throw new InvalidAxiomException("Not all symbols belong to the theory", name, axiom, library)
-      case Some(value) => AXIOM(value, axiom, name)
+      case None => throw new InvalidAxiomException("Not all symbols belong to the theory", fullName.value, axiom, library)
+      case Some(value) => AXIOM(value, axiom, fullName.value)
     }
   }
 
-  // def Axiom(using om: OutputManager, line: Int, file: String)(ax: theory.Axiom): AXIOM = AXIOM(line, file, ax.)
+  /**
+   * A Justification, corresponding to [[K.FunctionDefinition]] or [[K.PredicateDefinition]]
+   */
   abstract class DEFINITION(line: Int, file: String) extends JUSTIFICATION {
+    val fullName: String
+    def repr: String = innerJustification.repr
 
     def label: F.ConstantLabel[?]
     knownDefs.update(label, Some(this))
 
   }
 
-  class THM(using om: OutputManager)(val statement: F.Sequent, val fullName: String, line: Int, file: String, val kind: TheoremKind)(computeProof: Proof ?=> Unit) extends JUSTIFICATION {
+  /**
+   * A proven, reusable statement. A justification corresponding to [[K.Theorem]].
+   */
+  sealed abstract class THM extends JUSTIFICATION {
+
+    /**
+     * The underlying Kernel proof [[K.SCProof]], if it is still available. Proofs are not kept in memory for efficiency.
+     */
+    def kernelProof: Option[K.SCProof]
+
+    /**
+     * The high level [[Proof]], if one was used to obtain the theorem. If the theorem was not produced by such high level proof but directly by a low level one, this is None.
+     */
+    def highProof: Option[BaseProof]
+    val innerJustification: theory.Theorem
+
+    /**
+     * A pretty representation of the goal of the theorem
+     */
+    def prettyGoal: String = lisa.utils.FOLPrinter.prettySequent(statement.underlying)
+  }
+  object THM {
+
+    /**
+     * Standard way to construct a theorem using a high level proof.
+     *
+     * @param om The output manager, available in any file extending [[lisa.utils.BasicMain]]
+     * @param statement The statement of the theorem
+     * @param fullName The full name of the theorem, including the path. Usually fetched automatically by the compiler.
+     * @param line The line at which the theorem is defined. Usually fetched automatically by the compiler. Used for error reporting
+     * @param file The file in which the theorem is defined. Usually fetched automatically by the compiler. Used for error reporting
+     * @param kind The kind of theorem (Theorem, Lemma, Corollary)
+     * @param computeProof The proof computation. The proof is built by adding proof steps to the proof object. The proof object is an impicit argument of computeProof,
+     * @see <a href="https://docs.scala-lang.org/scala3/reference/contextual/context-functions.html">Context Functions in Scala</a>
+     * @return
+     */
+    def apply(using om: OutputManager)(statement: F.Sequent, fullName: String, line: Int, file: String, kind: TheoremKind)(computeProof: Proof ?=> Unit) =
+      THMFromProof(statement, fullName, line, file, kind)(computeProof)
+
+    /**
+     * Constructs a "high level" theorem from an existing theorem in the
+     *
+     * @param om The output manager, available in any file extending [[lisa.utils.BasicMain]]
+     * @param statement The statement of the theorem
+     * @param fullName The full name of the theorem, including the path/package.
+     * @param kind The kind of theorem (Theorem, Lemma, Corollary)
+     * @param innerThm The inner theorem, coming from the kernel
+     * @param getProof If available, a way to compute the Kernel proof again.
+     */
+    def fromKernel(using om: OutputManager)(statement: F.Sequent, fullName: String, kind: TheoremKind, innerThm: theory.Theorem, getProof: () => Option[K.SCProof]) =
+      THMFromKernel(statement, fullName, kind, innerThm, getProof)
+
+    /**
+     * Construct a theorem (both in the kernel and high level) from a proof.
+     *
+     * @param om The output manager, available in any file extending [[lisa.utils.BasicMain]]
+     * @param statement The statement of the theorem
+     * @param fullName The full name of the theorem, including the path/package.
+     * @param kind The kind of theorem (Theorem, Lemma, Corollary)
+     * @param getProof The kernel proof.
+     * @param justifs low level justifications used to justify the proof's imports
+     * @return
+     */
+    def fromSCProof(using om: OutputManager)(statement: F.Sequent, fullName: String, kind: TheoremKind, getProof: () => K.SCProof, justifs: Seq[theory.Justification]): THM =
+      val proof = getProof()
+      theory.theorem(fullName, statement.underlying, proof, justifs) match {
+        case K.Judgement.ValidJustification(just) =>
+          fromKernel(statement, fullName, kind, just.asInstanceOf, () => Some(getProof()))
+        case wrongJudgement: K.Judgement.InvalidJustification[?] =>
+          om.lisaThrow(
+            LisaException.InvalidKernelJustificationComputation(
+              "The proof was rejected by LISA's logical kernel. ",
+              wrongJudgement,
+              None
+            )
+          )
+      }
+
+  }
+
+  /**
+   * A theorem that was produced from a kernel theorem and not from a high level proof. See [[THM.fromKernel]].
+   * Those are typically theorems imported from another tool, or from serialization.
+   */
+  class THMFromKernel(using om: OutputManager)(val statement: F.Sequent, val fullName: String, val kind: TheoremKind, innerThm: theory.Theorem, getProof: () => Option[K.SCProof]) extends THM {
+
+    def repr: String = innerJustification.repr
+    val innerJustification: theory.Theorem = innerThm
+    assert(innerThm.name == fullName)
+    def kernelProof: Option[K.SCProof] = getProof()
+    def highProof: Option[BaseProof] = None
+
+    val goal: F.Sequent = statement
+
+  }
+
+  /**
+   * A theorem that was produced from a high level proof. See [[THM.apply]].
+   * Typical way to construct a theorem in the library, but serialization for example will produce a [[THMFromKernel]].
+   */
+  class THMFromProof(using om: OutputManager)(val statement: F.Sequent, val fullName: String, line: Int, file: String, val kind: TheoremKind)(computeProof: Proof ?=> Unit) extends THM {
 
     val goal: F.Sequent = statement
-    val name: String = fullName
 
     val proof: BaseProof = new BaseProof(this)
+    def kernelProof: Option[K.SCProof] = Some(proof.toSCProof)
+    def highProof: Option[BaseProof] = Some(proof)
 
-    val innerJustification: theory.Theorem = prove(computeProof)
+    import lisa.utils.Serialization.*
+    val innerJustification: theory.Theorem =
+      if library._withCache then
+        oneThmFromFile("cache/" + name, library.theory) match {
+          case Some(thm) => thm // try to get the theorem from file
 
-    def prettyGoal: String = lisa.utils.FOLPrinter.prettySequent(goal.underlying)
-    def repr: String = s" ${if (withSorry) " Sorry" else ""} Theorem $name := $statement\n"
+          case None =>
+            val (thm, scp, justifs) = prove(computeProof) // if fail, prove it
+            thmsToFile("cache/" + name, theory, List((name, scp, justifs))) // and save it to the file
+            thm
+        }
+      else prove(computeProof)._1
+    def repr: String = innerJustification.repr
 
-    private def prove(computeProof: Proof ?=> Unit): theory.Theorem = {
+    library.last = Some(this)
+    private def prove(computeProof: Proof ?=> Unit): (theory.Theorem, SCProof, List[(String, theory.Justification)]) = {
       try {
         computeProof(using proof)
       } catch {
-        /*case e: NotImplementedError =>
-          om.lisaThrow(new UnimplementedProof(this))*/
         case e: UserLisaException =>
           om.lisaThrow(e)
       }
@@ -334,10 +558,10 @@ trait WithTheorems {
         om.lisaThrow(new UnimplementedProof(this))
 
       val scp = proof.toSCProof
-      theory.theorem(name, goal.underlying, scp, proof.getImports.map(_._1.innerJustification)) match {
+      val justifs = proof.getImports.map(e => (e._1.owner, e._1.innerJustification))
+      theory.theorem(name, goal.underlying, scp, justifs.map(_._2)) match {
         case K.Judgement.ValidJustification(just) =>
-          library.last = Some(this)
-          just
+          (just, scp, justifs)
         case wrongJudgement: K.Judgement.InvalidJustification[?] =>
           om.lisaThrow(
             LisaException.InvalidKernelJustificationComputation(
@@ -355,19 +579,33 @@ trait WithTheorems {
 
   trait TheoremKind {
     val kind2: String
-    def apply(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(statement: F.Sequent)(computeProof: Proof ?=> Unit): THM = {
-      val thm = new THM(statement, name.value, line.value, file.value, this)(computeProof) {}
-      if (this == Theorem) {
-        show(thm)
-      }
+
+    def apply(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(statement: F.Sequent)(computeProof: Proof ?=> Unit): THM = {
+      val thm = THM(statement, name.value, line.value, file.value, this)(computeProof)
+      if this == Theorem then show(thm)
       thm
     }
 
   }
+
+  /**
+   * A "Theorem" kind of theorem, by opposition with a lemma or corollary. The difference is that theorem are always printed when a file defining one is run.
+   */
   object Theorem extends TheoremKind { val kind2: String = "Theorem" }
+
+  /**
+   * Lemmas are like theorems, but are conceptually less importants and are not printed when a file defining one is run.
+   */
   object Lemma extends TheoremKind { val kind2: String = "Lemma" }
+
+  /**
+   * Corollaries are like theorems, but are conceptually less importants and are not printed when a file defining one is run.
+   */
   object Corollary extends TheoremKind { val kind2: String = "Corollary" }
 
+  /**
+   * Internal statements are internally produced theorems, for example as intermediate step in definitions.
+   */
   object InternalStatement extends TheoremKind { val kind2: String = "Internal, automatically produced" }
 
 }
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index fa327fe3..62381a49 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -463,6 +463,10 @@ object KernelHelpers {
    */
   def checkProof(proof: SCProof, output: String => Unit = println): Unit = {
     val judgement = SCProofChecker.checkSCProof(proof)
-    output(FOLPrinter.prettySCProof(judgement))
+    val pl = proof.totalLength
+    if pl > 100 then
+      output("...")
+      output(s"Proof is too long to be displayed [$pl steps]")
+    else output(FOLPrinter.prettySCProof(judgement))
   }
 }
diff --git a/lisa-utils/src/main/scala/lisa/utils/LisaException.scala b/lisa-utils/src/main/scala/lisa/utils/LisaException.scala
index 7b945d40..dcef0ce6 100644
--- a/lisa-utils/src/main/scala/lisa/utils/LisaException.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/LisaException.scala
@@ -44,6 +44,9 @@ abstract class UserLisaException(var errorMessage: String)(using line: sourcecod
   def fixTrace(): Unit = ()
 }
 object UserLisaException {
+  class InvalidProofFromFileException(errorMessage: String, file: String)(using sourcecode.Line, sourcecode.File) extends UserLisaException(errorMessage) {
+    def showError: String = errorMessage
+  }
   class InvalidAxiomException(errorMessage: String, name: String, formula: lisa.fol.FOL.Formula, library: lisa.prooflib.Library)(using sourcecode.Line, sourcecode.File)
       extends UserLisaException(errorMessage) {
     def showError: String = s"The desired axiom \"$name\" contains symbol that are not part of the theory.\n" +
diff --git a/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala b/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
index e005fa3f..cc898057 100644
--- a/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
@@ -94,14 +94,14 @@ object ProofsShrink {
               val (k, sequent) = resolve(i)
               val imported = subProof.imports(j)
               if (sequent != imported) {
-                Some((Restate(imported, k), -(j - 1) -> imported))
+                Some((Restate(imported, k), j -> imported))
               } else {
-                None
+                Some((Restate(imported, k), j -> imported))
               }
             }.unzip
-            val rewrittenMap = rewrittenSeq.zipWithIndex.map { case ((i, sequent), j) => i -> (offset + acc.size + j, sequent) }.toMap
-            val childTopPremises = subPremises.map(i => rewrittenMap.getOrElse(i, resolve(i))).toIndexedSeq
-            acc ++ rewrittenPremises ++ flattenProofRecursive(subProof.steps, childTopPremises, offset + acc.size + rewrittenPremises.size)
+            val rewrittenMap = rewrittenSeq.map { case (j, sequent) => j -> (offset + acc.size - j - 1 + rewrittenSeq.size, sequent) }.toMap
+            val childTopPremises = subPremises.zipWithIndex.map((i, j) => rewrittenMap(j)).toIndexedSeq
+            acc ++ rewrittenPremises.reverse ++ flattenProofRecursive(subProof.steps, childTopPremises, offset + acc.size + rewrittenPremises.size)
           case _ =>
             acc :+ mapPremises(step, i => resolve(i)._1)
         }
@@ -299,4 +299,5 @@ object ProofsShrink {
     optimizeFixedPoint(flattenProof(proof))
   }
 
+  def minimizeProofOnce(proof: SCProof): SCProof = deadStepsElimination(factorProof(simplifyProof(flattenProof(proof))))
 }
diff --git a/lisa-utils/src/main/scala/lisa/utils/Serialization.scala b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
new file mode 100644
index 00000000..d89d473f
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
@@ -0,0 +1,721 @@
+package lisa.utils
+
+import lisa.utils.K.*
+import lisa.utils.ProofsShrink.*
+
+import java.io._
+import scala.collection.mutable.{Map => MutMap}
+
+object Serialization {
+
+  // Define codes for the various proof steps
+  inline def restate: Byte = 0
+  inline def restateTrue: Byte = 1
+  inline def hypothesis: Byte = 2
+  inline def cut: Byte = 3
+  inline def leftAnd: Byte = 4
+  inline def leftOr: Byte = 5
+  inline def leftImplies: Byte = 6
+  inline def leftIff: Byte = 7
+  inline def leftNot: Byte = 8
+  inline def leftForall: Byte = 9
+  inline def leftExists: Byte = 10
+  inline def leftExistsOne: Byte = 11
+  inline def rightAnd: Byte = 12
+  inline def rightOr: Byte = 13
+  inline def rightImplies: Byte = 14
+  inline def rightIff: Byte = 15
+  inline def rightNot: Byte = 16
+  inline def rightForall: Byte = 17
+  inline def rightExists: Byte = 18
+  inline def rightExistsOne: Byte = 19
+  inline def weakening: Byte = 20
+  inline def leftRefl: Byte = 21
+  inline def rightRefl: Byte = 22
+  inline def leftSubstEq: Byte = 23
+  inline def rightSubstEq: Byte = 24
+  inline def leftSubstIff: Byte = 25
+  inline def rightSubstIff: Byte = 26
+  inline def instSchema: Byte = 27
+  inline def scSubproof: Byte = 28
+  inline def sorry: Byte = 29
+
+  type Line = Int
+
+  // Injectively represent a TermLabel as a string
+  def termLabelToString(label: TermLabel): String =
+    label match
+      case l: ConstantFunctionLabel => "cfl_" + l.id.name + "_" + l.id.no + "_" + l.arity
+      case l: SchematicFunctionLabel => "sfl_" + l.id.name + "_" + l.id.no + "_" + l.arity
+      case l: VariableLabel => "vl_" + l.id.name + "_" + l.id.no
+
+  // Injectively represent a FormulaLabel as a string.
+  def formulaLabelToString(label: FormulaLabel): String =
+    label match
+      case l: ConstantPredicateLabel => "cpl_" + l.id.name + "_" + l.id.no + "_" + l.arity
+      case l: SchematicPredicateLabel => "spl_" + l.id.name + "_" + l.id.no + "_" + l.arity
+      case l: ConstantConnectorLabel => "ccl_" + l.id.name + "_" + l.id.no + "_" + l.arity
+      case l: SchematicConnectorLabel => "scl_" + l.id.name + "_" + l.id.no + "_" + l.arity
+      case l: VariableFormulaLabel => "vfl_" + l.id.name + "_" + l.id.no
+      case l: BinderLabel => "bl_" + l.id.name + "_" + l.id.no
+
+  // write a term label to an OutputStream
+  def termLabelToDOS(label: TermLabel, dos: DataOutputStream): Unit =
+    label match
+      case l: ConstantFunctionLabel =>
+        dos.writeByte(0)
+        dos.writeUTF(l.id.name)
+        dos.writeInt(l.id.no)
+        dos.writeInt(l.arity)
+      case l: SchematicFunctionLabel =>
+        dos.writeByte(1)
+        dos.writeUTF(l.id.name)
+        dos.writeInt(l.id.no)
+        dos.writeInt(l.arity)
+      case l: VariableLabel =>
+        dos.writeByte(2)
+        dos.writeUTF(l.id.name)
+        dos.writeInt(l.id.no)
+  // write a formula label to an OutputStream
+  def formulaLabelToDOS(label: FormulaLabel, dos: DataOutputStream): Unit =
+    label match
+      case l: ConstantPredicateLabel =>
+        dos.writeByte(3)
+        dos.writeUTF(l.id.name)
+        dos.writeInt(l.id.no)
+        dos.writeInt(l.arity)
+      case l: SchematicPredicateLabel =>
+        dos.writeByte(4)
+        dos.writeUTF(l.id.name)
+        dos.writeInt(l.id.no)
+        dos.writeInt(l.arity)
+      case l: ConstantConnectorLabel =>
+        dos.writeByte(5)
+        dos.writeUTF(l.id.name)
+      case l: SchematicConnectorLabel =>
+        dos.writeByte(6)
+        dos.writeUTF(l.id.name)
+        dos.writeInt(l.id.no)
+        dos.writeInt(l.arity)
+      case l: VariableFormulaLabel =>
+        dos.writeByte(7)
+        dos.writeUTF(l.id.name)
+        dos.writeInt(l.id.no)
+      case l: BinderLabel =>
+        dos.writeByte(8)
+        dos.writeUTF(l.id.name)
+
+  /**
+   * Main function that, when given a proof, will serialize it to a file. It will also serialize all the formulas appearing in it to another file.
+   */
+  def proofsToDataStream(treesDOS: DataOutputStream, proofDOS: DataOutputStream, theorems: Seq[(String, SCProof, List[String])]): Unit = {
+
+    val termMap = MutMap[Long, Line]()
+    val formulaMap = MutMap[Long, Line]()
+
+    var line = -1
+
+    // Compute the line of a term. If it is not in the map, add it to the map and write it to the tree file
+    def lineOfTerm(term: Term): Line =
+      termMap.get(term.uniqueNumber) match
+        case Some(line) => line
+        case None =>
+          val na = term.args.map(t => lineOfTerm(t))
+          termLabelToDOS(term.label, treesDOS)
+          na.foreach(t => treesDOS.writeInt(t))
+          line = line + 1
+          termMap(term.uniqueNumber) = line
+          line
+
+    // Compute the line of a formula. If it is not in the map, add it to the map and write it to the tree file
+    def lineOfFormula(formula: Formula): Line =
+      formulaMap.get(formula.uniqueNumber) match
+        case Some(line) => line
+        case None =>
+          val nextLine = formula match
+            case PredicateFormula(label, args) =>
+              val na = args.map(t => lineOfTerm(t))
+              formulaLabelToDOS(label, treesDOS)
+              na.foreach(t => treesDOS.writeInt(t))
+            case ConnectorFormula(label, args) =>
+              val na = args.map(t => lineOfFormula(t))
+              formulaLabelToDOS(label, treesDOS)
+              treesDOS.writeShort(na.size)
+              na.foreach(t => treesDOS.writeInt(t))
+            case BinderFormula(label, bound, inner) =>
+              val ni = lineOfFormula(inner)
+              formulaLabelToDOS(label, treesDOS)
+              termLabelToDOS(bound, treesDOS)
+              treesDOS.writeInt(ni)
+          line = line + 1
+          formulaMap(formula.uniqueNumber) = line
+          line
+
+    // Write a sequent to the proof file.
+    def sequentToProofDOS(sequent: Sequent): Unit =
+      proofDOS.writeShort(sequent.left.size)
+      sequent.left.foreach(f => proofDOS.writeInt(lineOfFormula(f)))
+      proofDOS.writeShort(sequent.right.size)
+      sequent.right.foreach(f => proofDOS.writeInt(lineOfFormula(f)))
+
+    def lttToProofDOS(ltt: LambdaTermTerm): Unit =
+      val body = lineOfTerm(ltt.body)
+      proofDOS.writeShort(ltt.vars.size)
+      ltt.vars.foreach(v => termLabelToDOS(v, proofDOS))
+      proofDOS.writeInt(body)
+
+    def ltfToProofDOS(ltf: LambdaTermFormula): Unit =
+      val body = lineOfFormula(ltf.body)
+      proofDOS.writeShort(ltf.vars.size)
+      ltf.vars.foreach(v => termLabelToDOS(v, proofDOS))
+      proofDOS.writeInt(body)
+
+    def lffToProofDOS(lff: LambdaFormulaFormula): Unit =
+      val body = lineOfFormula(lff.body)
+      proofDOS.writeShort(lff.vars.size)
+      lff.vars.foreach(v => formulaLabelToDOS(v, proofDOS))
+      proofDOS.writeInt(body)
+
+    /**
+     * Write a proof step to the proof file.
+     * First write the code describing the proof step, then the "bot" sequent, then the various parameters in order.
+     * List are described by first writing (as a short) the number of elements in the list.
+     *
+     * @param ps
+     */
+    def proofStepToProofDOS(ps: SCProofStep): Unit = {
+      ps match {
+        case Restate(bot, t1) =>
+          proofDOS.writeByte(restate)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+        case RestateTrue(bot) =>
+          proofDOS.writeByte(restateTrue)
+          sequentToProofDOS(bot)
+        case Hypothesis(bot, phi) =>
+          proofDOS.writeByte(hypothesis)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(lineOfFormula(phi))
+        case Cut(bot, t1, t2, phi) =>
+          proofDOS.writeByte(cut)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(t2)
+          proofDOS.writeInt(lineOfFormula(phi))
+        case LeftAnd(bot, t1, phi, psi) =>
+          proofDOS.writeByte(leftAnd)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          proofDOS.writeInt(lineOfFormula(psi))
+        case LeftOr(bot, t, disjuncts) =>
+          proofDOS.writeByte(leftOr)
+          sequentToProofDOS(bot)
+          proofDOS.writeShort(t.size)
+          t.foreach(proofDOS.writeInt)
+          proofDOS.writeShort(disjuncts.size)
+          disjuncts.foreach(f => proofDOS.writeInt(lineOfFormula(f)))
+        case LeftImplies(bot, t1, t2, phi, psi) =>
+          proofDOS.writeByte(leftImplies)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(t2)
+          proofDOS.writeInt(lineOfFormula(phi))
+          proofDOS.writeInt(lineOfFormula(psi))
+        case LeftIff(bot, t1, phi, psi) =>
+          proofDOS.writeByte(leftIff)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          proofDOS.writeInt(lineOfFormula(psi))
+        case LeftNot(bot, t1, phi) =>
+          proofDOS.writeByte(leftNot)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+        case LeftForall(bot, t1, phi, x, t) =>
+          proofDOS.writeByte(leftForall)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          termLabelToDOS(x, proofDOS)
+          proofDOS.writeInt(lineOfTerm(t))
+        case LeftExists(bot, t1, phi, x) =>
+          proofDOS.writeByte(leftExists)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          termLabelToDOS(x, proofDOS)
+        case LeftExistsOne(bot, t1, phi, x) =>
+          proofDOS.writeByte(leftExistsOne)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          termLabelToDOS(x, proofDOS)
+        case RightAnd(bot, t, conjuncts) =>
+          proofDOS.writeByte(rightAnd)
+          sequentToProofDOS(bot)
+          proofDOS.writeShort(t.size)
+          t.foreach(proofDOS.writeInt)
+          proofDOS.writeShort(conjuncts.size)
+          conjuncts.foreach(f => proofDOS.writeInt(lineOfFormula(f)))
+        case RightOr(bot, t1, phi, psi) =>
+          proofDOS.writeByte(rightOr)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          proofDOS.writeInt(lineOfFormula(psi))
+        case RightImplies(bot, t1, phi, psi) =>
+          proofDOS.writeByte(rightImplies)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          proofDOS.writeInt(lineOfFormula(psi))
+        case RightIff(bot, t1, t2, phi, psi) =>
+          proofDOS.writeByte(rightIff)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(t2)
+          proofDOS.writeInt(lineOfFormula(phi))
+          proofDOS.writeInt(lineOfFormula(psi))
+        case RightNot(bot, t1, phi) =>
+          proofDOS.writeByte(rightNot)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+        case RightForall(bot, t1, phi, x) =>
+          proofDOS.writeByte(rightForall)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          termLabelToDOS(x, proofDOS)
+        case RightExists(bot, t1, phi, x, t) =>
+          proofDOS.writeByte(rightExists)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          termLabelToDOS(x, proofDOS)
+          proofDOS.writeInt(lineOfTerm(t))
+        case RightExistsOne(bot, t1, phi, x) =>
+          proofDOS.writeByte(rightExistsOne)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(phi))
+          termLabelToDOS(x, proofDOS)
+        case Weakening(bot, t1) =>
+          proofDOS.writeByte(weakening)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+        case LeftRefl(bot, t1, fa) =>
+          proofDOS.writeByte(leftRefl)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeInt(lineOfFormula(fa))
+        case RightRefl(bot, fa) =>
+          proofDOS.writeByte(rightRefl)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(lineOfFormula(fa))
+        case LeftSubstEq(bot, t1, equals, lambdaPhi) =>
+          proofDOS.writeByte(leftSubstEq)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeShort(equals.size)
+          equals.foreach(t =>
+            proofDOS.writeInt(lineOfTerm(t._1))
+            proofDOS.writeInt(lineOfTerm(t._2))
+          )
+          ltfToProofDOS(lambdaPhi)
+        case RightSubstEq(bot, t1, equals, lambdaPhi) =>
+          proofDOS.writeByte(rightSubstEq)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeShort(equals.size)
+          equals.foreach(t =>
+            proofDOS.writeInt(lineOfTerm(t._1))
+            proofDOS.writeInt(lineOfTerm(t._2))
+          )
+          ltfToProofDOS(lambdaPhi)
+        case LeftSubstIff(bot, t1, equals, lambdaPhi) =>
+          proofDOS.writeByte(leftSubstIff)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeShort(equals.size)
+          equals.foreach(t =>
+            proofDOS.writeInt(lineOfFormula(t._1))
+            proofDOS.writeInt(lineOfFormula(t._2))
+          )
+          lffToProofDOS(lambdaPhi)
+        case RightSubstIff(bot, t1, equals, lambdaPhi) =>
+          proofDOS.writeByte(rightSubstIff)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeShort(equals.size)
+          equals.foreach(t =>
+            proofDOS.writeInt(lineOfFormula(t._1))
+            proofDOS.writeInt(lineOfFormula(t._2))
+          )
+          lffToProofDOS(lambdaPhi)
+        case InstSchema(bot, t1, mCon, mPred, mTerm) =>
+          proofDOS.writeByte(instSchema)
+          sequentToProofDOS(bot)
+          proofDOS.writeInt(t1)
+          proofDOS.writeShort(mCon.size)
+          mCon.foreach(t =>
+            formulaLabelToDOS(t._1, proofDOS)
+            lffToProofDOS(t._2)
+          )
+          proofDOS.writeShort(mPred.size)
+          mPred.foreach(t =>
+            formulaLabelToDOS(t._1, proofDOS)
+            ltfToProofDOS(t._2)
+          )
+          proofDOS.writeShort(mTerm.size)
+          mTerm.foreach(t =>
+            termLabelToDOS(t._1, proofDOS)
+            lttToProofDOS(t._2)
+          )
+        case SCSubproof(sp, premises) => throw new Exception("Cannot support subproofs, flatten the proof first.")
+        case Sorry(bot) =>
+          proofDOS.writeByte(sorry)
+          sequentToProofDOS(bot)
+      }
+    }
+
+    proofDOS.writeShort(theorems.size)
+    theorems.foreach((thmName, proof, justifications) =>
+      proofDOS.writeUTF(thmName)
+      proofDOS.writeShort(justifications.size)
+      justifications.foreach(j => proofDOS.writeUTF(j))
+      proofDOS.writeInt(proof.imports.size)
+      proof.imports.foreach(sequent => sequentToProofDOS(sequent))
+      proofDOS.writeInt(proof.steps.size)
+      proof.steps.foreach(ps => proofStepToProofDOS(ps))
+    )
+
+  }
+
+  /**
+   * This functions reverses the effect of proofToDataStream
+   *
+   * @param lines The lines of the "file" where the proof is stored
+   */
+  def proofsFromDataStream(treesDIS: DataInputStream, proofDIS: DataInputStream): Seq[(String, SCProof, List[String])] = {
+
+    val termMap = MutMap[Line, Term]()
+    val formulaMap = MutMap[Line, Formula]()
+
+    // Read a label from the tree file, reversing the effect of termLabelToDOS and formulaLabelToDOS.
+    def labelFromInputStream(dis: DataInputStream): Label = {
+      val labelType = dis.readByte()
+      labelType match
+        case 0 =>
+          val name = dis.readUTF()
+          val no = dis.readInt()
+          val arity = dis.readInt()
+          ConstantFunctionLabel(Identifier(name, no), arity)
+        case 1 =>
+          val name = dis.readUTF()
+          val no = dis.readInt()
+          val arity = dis.readInt()
+          SchematicFunctionLabel(Identifier(name, no), arity)
+        case 2 =>
+          val name = dis.readUTF()
+          val no = dis.readInt()
+          VariableLabel(Identifier(name, no))
+        case 3 =>
+          val name = dis.readUTF()
+          val no = dis.readInt()
+          val arity = dis.readInt()
+          ConstantPredicateLabel(Identifier(name, no), arity)
+        case 4 =>
+          val name = dis.readUTF()
+          val no = dis.readInt()
+          val arity = dis.readInt()
+          SchematicPredicateLabel(Identifier(name, no), arity)
+        case 5 =>
+          val name = dis.readUTF()
+          name match
+            case And.id.name => And
+            case Or.id.name => Or
+            case Implies.id.name => Implies
+            case Iff.id.name => Iff
+            case Neg.id.name => Neg
+        case 6 =>
+          val name = dis.readUTF()
+          val no = dis.readInt()
+          val arity = dis.readInt()
+          SchematicConnectorLabel(Identifier(name, no), arity)
+        case 7 =>
+          val name = dis.readUTF()
+          val no = dis.readInt()
+          VariableFormulaLabel(Identifier(name, no))
+        case 8 =>
+          dis.readUTF() match
+            case Forall.id.name => Forall
+            case Exists.id.name => Exists
+            case ExistsOne.id.name => ExistsOne
+
+    }
+
+    // Read and reconstruct all the terms and formulas in the tree file. Fill the table with it.
+    var lineNo = -1
+    try {
+      while true do
+        lineNo = lineNo + 1
+        val label = labelFromInputStream(treesDIS)
+        label match
+          case l: TermLabel =>
+            val args = (1 to l.arity).map(_ => termMap(treesDIS.readInt())).toSeq
+            termMap(lineNo) = Term(l, args)
+          case l: FormulaLabel =>
+            val formula = label match
+              case l: PredicateLabel =>
+                val args = (1 to l.arity).map(_ => termMap(treesDIS.readInt())).toSeq
+                PredicateFormula(l, args)
+              case l: ConnectorLabel =>
+                val ar = treesDIS.readShort()
+                val args = (1 to ar).map(_ => formulaMap(treesDIS.readInt())).toSeq
+                ConnectorFormula(l, args)
+              case l: BinderLabel =>
+                BinderFormula(l, labelFromInputStream(treesDIS).asInstanceOf[VariableLabel], formulaMap(treesDIS.readInt()))
+            formulaMap(lineNo) = formula
+    } catch
+      case _: EOFException =>
+        ()
+
+    // Terms and Formulas finished, deal with the proof now.
+
+    def lttFromProofDIS(): LambdaTermTerm =
+      val vars = (1 to proofDIS.readShort()).map(_ => labelFromInputStream(proofDIS).asInstanceOf[VariableLabel]).toSeq
+      val body = termMap(proofDIS.readInt())
+      LambdaTermTerm(vars, body)
+
+    def ltfFromProofDIS(): LambdaTermFormula =
+      val vars = (1 to proofDIS.readShort()).map(_ => labelFromInputStream(proofDIS).asInstanceOf[VariableLabel]).toSeq
+      val body = formulaMap(proofDIS.readInt())
+      LambdaTermFormula(vars, body)
+
+    def lffFromProofDIS(): LambdaFormulaFormula =
+      val vars = (1 to proofDIS.readShort()).map(_ => labelFromInputStream(proofDIS).asInstanceOf[VariableFormulaLabel]).toSeq
+      val body = formulaMap(proofDIS.readInt())
+      LambdaFormulaFormula(vars, body)
+
+    def sequentFromProofDIS(): Sequent =
+      val leftSize = proofDIS.readShort()
+      val left = (1 to leftSize).map(_ => formulaMap(proofDIS.readInt())).toSet
+      val rightSize = proofDIS.readShort()
+      val right = (1 to rightSize).map(_ => formulaMap(proofDIS.readInt())).toSet
+      Sequent(left, right)
+
+    // Read a proof step from the proof file. Inverse of proofStepToProofDOS
+    def proofStepFromProofDIS(): SCProofStep = {
+      val psType = proofDIS.readByte()
+      if (psType == restate) Restate(sequentFromProofDIS(), proofDIS.readInt())
+      else if (psType == restateTrue) RestateTrue(sequentFromProofDIS())
+      else if (psType == hypothesis) Hypothesis(sequentFromProofDIS(), formulaMap(proofDIS.readInt()))
+      else if (psType == cut) Cut(sequentFromProofDIS(), proofDIS.readInt(), proofDIS.readInt(), formulaMap(proofDIS.readInt()))
+      else if (psType == leftAnd) LeftAnd(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))
+      else if (psType == leftOr)
+        LeftOr(
+          sequentFromProofDIS(),
+          (1 to proofDIS.readShort()).map(_ => proofDIS.readInt()).toSeq,
+          (1 to proofDIS.readShort()).map(_ => formulaMap(proofDIS.readInt())).toSeq
+        )
+      else if (psType == leftImplies) LeftImplies(sequentFromProofDIS(), proofDIS.readInt(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))
+      else if (psType == leftIff) LeftIff(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))
+      else if (psType == leftNot) LeftNot(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()))
+      else if (psType == leftForall)
+        LeftForall(
+          sequentFromProofDIS(),
+          proofDIS.readInt(),
+          formulaMap(proofDIS.readInt()),
+          labelFromInputStream(proofDIS).asInstanceOf[VariableLabel],
+          termMap(proofDIS.readInt())
+        )
+      else if (psType == leftExists) LeftExists(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), labelFromInputStream(proofDIS).asInstanceOf[VariableLabel])
+      else if (psType == leftExistsOne) LeftExistsOne(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), labelFromInputStream(proofDIS).asInstanceOf[VariableLabel])
+      else if (psType == rightAnd)
+        RightAnd(
+          sequentFromProofDIS(),
+          (1 to proofDIS.readShort()).map(_ => proofDIS.readInt()).toSeq,
+          (1 to proofDIS.readShort()).map(_ => formulaMap(proofDIS.readInt())).toSeq
+        )
+      else if (psType == rightOr) RightOr(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))
+      else if (psType == rightImplies) RightImplies(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))
+      else if (psType == rightIff) RightIff(sequentFromProofDIS(), proofDIS.readInt(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))
+      else if (psType == rightNot) RightNot(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()))
+      else if (psType == rightForall) RightForall(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), labelFromInputStream(proofDIS).asInstanceOf[VariableLabel])
+      else if (psType == rightExists)
+        RightExists(
+          sequentFromProofDIS(),
+          proofDIS.readInt(),
+          formulaMap(proofDIS.readInt()),
+          labelFromInputStream(proofDIS).asInstanceOf[VariableLabel],
+          termMap(proofDIS.readInt())
+        )
+      else if (psType == rightExistsOne) RightExistsOne(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()), labelFromInputStream(proofDIS).asInstanceOf[VariableLabel])
+      else if (psType == weakening) Weakening(sequentFromProofDIS(), proofDIS.readInt())
+      else if (psType == leftRefl) LeftRefl(sequentFromProofDIS(), proofDIS.readInt(), formulaMap(proofDIS.readInt()))
+      else if (psType == rightRefl) RightRefl(sequentFromProofDIS(), formulaMap(proofDIS.readInt()))
+      else if (psType == leftSubstEq)
+        LeftSubstEq(
+          sequentFromProofDIS(),
+          proofDIS.readInt(),
+          (1 to proofDIS.readShort()).map(_ => (termMap(proofDIS.readInt()), termMap(proofDIS.readInt()))).toList,
+          ltfFromProofDIS()
+        )
+      else if (psType == rightSubstEq)
+        RightSubstEq(
+          sequentFromProofDIS(),
+          proofDIS.readInt(),
+          (1 to proofDIS.readShort()).map(_ => (termMap(proofDIS.readInt()), termMap(proofDIS.readInt()))).toList,
+          ltfFromProofDIS()
+        )
+      else if (psType == leftSubstIff)
+        LeftSubstIff(
+          sequentFromProofDIS(),
+          proofDIS.readInt(),
+          (1 to proofDIS.readShort()).map(_ => (formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))).toList,
+          lffFromProofDIS()
+        )
+      else if (psType == rightSubstIff)
+        RightSubstIff(
+          sequentFromProofDIS(),
+          proofDIS.readInt(),
+          (1 to proofDIS.readShort()).map(_ => (formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))).toList,
+          lffFromProofDIS()
+        )
+      else if (psType == instSchema)
+        InstSchema(
+          sequentFromProofDIS(),
+          proofDIS.readInt(),
+          (1 to proofDIS.readShort()).map(_ => (labelFromInputStream(proofDIS).asInstanceOf[SchematicConnectorLabel], lffFromProofDIS())).toMap,
+          (1 to proofDIS.readShort()).map(_ => (labelFromInputStream(proofDIS).asInstanceOf[SchematicVarOrPredLabel], ltfFromProofDIS())).toMap,
+          (1 to proofDIS.readShort()).map(_ => (labelFromInputStream(proofDIS).asInstanceOf[SchematicTermLabel], lttFromProofDIS())).toMap
+        )
+      else if (psType == sorry) Sorry(sequentFromProofDIS())
+      else throw new Exception("Unknown proof step type: " + psType)
+    }
+
+    // for each given theorem, write it to the file.
+    val numberThm = proofDIS.readShort()
+    (1 to numberThm)
+      .map(_ =>
+        val thmName = proofDIS.readUTF()
+        val justificationsSize = proofDIS.readShort()
+        val justifications = (1 to justificationsSize).map(_ => proofDIS.readUTF()).toList
+        val importsSize = proofDIS.readInt()
+        val imports = (1 to importsSize).map(_ => sequentFromProofDIS()).toSeq
+        val noSteps = proofDIS.readInt()
+        val steps = (1 to noSteps).map(_ => proofStepFromProofDIS()).toSeq
+
+        (thmName, new SCProof(steps.toIndexedSeq, imports.toIndexedSeq), justifications)
+      )
+      .toSeq
+
+  }
+
+  /**
+   * Write a list of theorems to a pair of OutputStrem, one for the formulas and term trees, one for the proof.
+   * Each theorem has a name, a proof and a list of justifications, with a name for those justifications that can be fetched in the code base.
+   */
+  def thmsToDataStream(treesDOS: DataOutputStream, proofDOS: DataOutputStream, theory: RunningTheory, theorems: List[(String, SCProof, List[(String, theory.Justification)])]): Unit = {
+    proofsToDataStream(
+      treesDOS,
+      proofDOS,
+      theorems.map((name, proof, justs) =>
+        val justNames = justs.map {
+          case (obj, theory.Axiom(name, ax)) => "a" + obj + "$" + name
+          case (obj, theory.Theorem(name, proposition, withSorry)) => "t" + obj + "$" + name
+          case (obj, theory.FunctionDefinition(label, out, expression, withSorry)) => "f" + obj + "$" + label.id.name + "_" + label.id.no + "_" + label.arity
+          case (obj, theory.PredicateDefinition(label, expression)) => "p" + obj + "$" + label.id.name + "_" + label.id.no + "_" + label.arity
+        }
+        (name, minimizeProofOnce(proof), justNames)
+      )
+    )
+  }
+
+  /**
+   * Read theorems from two files, one for the formulas and term trees, one for the proof.
+   * Theorems are validated in the kernel. Justifications are fetched from the code base using the name written in the file.
+   * This uses java reflection, for example to obtain the theorem [[scala.mathematics.settheory.SetTheoryLibrary.russelsParadox]] from the
+   * string "scala.mathematics.settheory.SetTheoryLibrary.russelsParadox".
+   * A bit ugly, but don't really have better for now.
+   */
+  def thmsFromDataStream(treesDIS: DataInputStream, proofDIS: DataInputStream, theory: RunningTheory, debug: Boolean = false): Seq[(theory.Theorem, SCProof)] = {
+    proofsFromDataStream(treesDIS, proofDIS).map { (name, proof, justifications) =>
+      val justs = justifications.map { j =>
+        val nl = j.tail
+        val Array(obj, name) = nl.split("\\$")
+        try {
+          Class.forName(obj + "$").getField("MODULE$").get(null)
+        } catch { case _ => "Not found: " + obj }
+        Class.forName("lisa.settheory.SetTheoryLibrary" + "$").getField("MODULE$").get(null)
+
+        j(0) match
+          case 'a' => theory.getAxiom(name).get
+          case 't' =>
+            theory.getTheorem(name).get
+          case 'f' =>
+            name.split("_") match
+              case Array(name, no, arity) => theory.getDefinition(ConstantFunctionLabel(Identifier(name, no.toInt), arity.toInt)).get
+          case 'p' =>
+            name.split("_") match
+              case Array(name, no, arity) => theory.getDefinition(ConstantPredicateLabel(Identifier(name, no.toInt), arity.toInt)).get
+      }
+      if debug then
+        // To avoid conflicts where a theorem already exists, for example in test suits.
+        (theory.makeTheorem(name + "_test", proof.conclusion, proof, justs).get, proof)
+      else (theory.makeTheorem(name, proof.conclusion, proof, justs).get, proof)
+    }
+
+  }
+
+  /**
+   * Write a list of theorems to a pair file, one for the formulas and term trees, one for the proof.
+   * Each theorem has a name, a proof and a list of justifications, with a name for those justifications that can be fetched in the code base.
+   */
+  def thmsToFile(filename: String, theory: RunningTheory, theorems: List[(String, SCProof, List[(String, theory.Justification)])]): Unit = {
+    val directory = File(filename).getParentFile()
+    if (directory != null) && !directory.exists() then directory.mkdirs()
+    val treeFile = File(filename + ".trees")
+    if !treeFile.exists() then treeFile.createNewFile()
+    val proofFile = File(filename + ".proof")
+    if !proofFile.exists() then proofFile.createNewFile()
+    val treesDOS = new DataOutputStream(new BufferedOutputStream(new FileOutputStream(treeFile)))
+    val proofDOS = new DataOutputStream(new BufferedOutputStream(new FileOutputStream(proofFile)))
+    thmsToDataStream(treesDOS, proofDOS, theory, theorems)
+    treesDOS.close()
+    proofDOS.close()
+  }
+
+  /**
+   * Read theorems from two files, one for the formulas and term trees, one for the proof.
+   * Theorems are validated in the kernel. Justifications are fetched from the code base using the name written in the file.
+   */
+  def thmsFromFile(filename: String, theory: RunningTheory): Seq[(theory.Theorem, SCProof)] = {
+    val treesDIS = new DataInputStream(new BufferedInputStream(new FileInputStream(File(filename + ".trees"))))
+    val proofDIS = new DataInputStream(new BufferedInputStream(new FileInputStream(File(filename + ".proof"))))
+    val thm = thmsFromDataStream(treesDIS, proofDIS, theory, false)
+    treesDIS.close()
+    proofDIS.close()
+    thm
+  }
+
+  /**
+   * Same as [[thmsFromFile]] but only returns the first theorem (usually because we know there is only one theorem in the file).
+   */
+  def oneThmFromFile(filename: String, theory: RunningTheory): Option[theory.Theorem] = {
+    val treeFile = File(filename + ".trees")
+    val proofFile = File(filename + ".proof")
+    if treeFile.isFile() && proofFile.isFile() then
+      val treesDIS = new DataInputStream(new BufferedInputStream(new FileInputStream(treeFile)))
+      val proofDIS = new DataInputStream(new BufferedInputStream(new FileInputStream(proofFile)))
+      val thm = thmsFromDataStream(treesDIS, proofDIS, theory, false)
+      treesDIS.close()
+      proofDIS.close()
+      Some(thm.head._1)
+    else None
+  }
+
+}
diff --git a/lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala b/lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala
index a963d446..5d7ccd07 100644
--- a/lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala
+++ b/lisa-utils/src/test/scala/lisa/test/utils/ProofTacticTestLib.scala
@@ -17,7 +17,7 @@ class ProofTacticTestLib extends AnyFunSuite with BasicMain {
   private val P = predicate[1]
 
   // generate a placeholde theorem to take ownership of proofs for test
-  val placeholderTheorem = Theorem(P(x) |- P(x)) { have(P(x) |- P(x)) by Hypothesis }
+  val placeholderTheorem: THMFromProof = Theorem(P(x) |- P(x)) { have(P(x) |- P(x)) by Hypothesis }.asInstanceOf
 
   // generates an empty proof owned by the placeholder theorem for testing
   def generateTestProof() = new BaseProof(placeholderTheorem)
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index ff036871..9f4b15a4 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -12,7 +12,6 @@ private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
   private val z = variable
 
   final val tarskiAxiom: AXIOM = Axiom(
-    "tarskiAxiom",
     forall(
       x,
       in(x, universe(x)) /\
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 6e11a9f9..192ff736 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -19,7 +19,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    *
    * `() |- (x = y) ⇔ ∀ z. z ∈ x ⇔ z ∈ y`
    */
-  final val extensionalityAxiom: this.AXIOM = Axiom("extensionalityAxiom", forall(z, in(z, x) <=> in(z, y)) <=> (x === y))
+  final val extensionalityAxiom: this.AXIOM = Axiom(forall(z, in(z, x) <=> in(z, y)) <=> (x === y))
 
   /**
    * Pairing Axiom --- For any sets `x` and `y`, there is a set that contains
@@ -31,7 +31,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    * This axiom defines [[unorderedPair]] as the function symbol representing
    * this set.
    */
-  final val pairAxiom: AXIOM = Axiom("pairAxiom", in(z, unorderedPair(x, y)) <=> (x === z) \/ (y === z))
+  final val pairAxiom: AXIOM = Axiom(in(z, unorderedPair(x, y)) <=> (x === z) \/ (y === z))
 
   /**
    * Comprehension/Separation Schema --- For a formula `ϕ(_, _)` and a set `z`,
@@ -44,7 +44,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    * This schema represents an infinite collection of axioms, one for each
    * formula `ϕ(x, z)`.
    */
-  final val comprehensionSchema: AXIOM = Axiom("comprehensionSchema", exists(y, forall(x, in(x, y) <=> (in(x, z) /\ φ(x, z)))))
+  final val comprehensionSchema: AXIOM = Axiom(exists(y, forall(x, in(x, y) <=> (in(x, z) /\ φ(x, z)))))
 
   /**
    * Empty Set Axiom --- From the Comprehension Schema follows the existence of
@@ -56,7 +56,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    *
    * `() |- !(x ∈ ∅)`
    */
-  final val emptySetAxiom: AXIOM = Axiom("emptySetAxiom", !in(x, emptySet))
+  final val emptySetAxiom: AXIOM = Axiom(!in(x, emptySet))
 
   /**
    * Union Axiom --- For any set `x`, there exists a set `union(x)` which is the
@@ -69,7 +69,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    *
    * This axiom defines [[union]] as the function symbol representing this set.
    */
-  final val unionAxiom: AXIOM = Axiom("unionAxiom", in(z, union(x)) <=> exists(y, in(y, x) /\ in(z, y)))
+  final val unionAxiom: AXIOM = Axiom(in(z, union(x)) <=> exists(y, in(y, x) /\ in(z, y)))
 
   /**
    * Subset Axiom --- For sets `x` and `y`, `x` is a subset of `y` iff every
@@ -79,7 +79,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    *
    * This axiom defines the [[subset]] symbol as this predicate.
    */
-  final val subsetAxiom: AXIOM = Axiom("subsetAxiom", subset(x, y) <=> forall(z, in(z, x) ==> in(z, y)))
+  final val subsetAxiom: AXIOM = Axiom(subset(x, y) <=> forall(z, in(z, x) ==> in(z, y)))
 
   /**
    * Power Set Axiom --- For a set `x`, there exists a power set of `x`, denoted
@@ -90,7 +90,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    * This axiom defines [[powerSet]] as the function symbol representing this
    * set.
    */
-  final val powerAxiom: AXIOM = Axiom("powerAxiom", in(x, powerSet(y)) <=> subset(x, y))
+  final val powerAxiom: AXIOM = Axiom(in(x, powerSet(y)) <=> subset(x, y))
 
   /**
    * Infinity Axiom --- There exists an infinite set.
@@ -105,7 +105,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    *
    * `() |- ∃ x. inductive(x)`
    */
-  final val infinityAxiom: AXIOM = Axiom("infinityAxiom", exists(x, in(emptySet, x) /\ forall(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x))))
+  final val infinityAxiom: AXIOM = Axiom(exists(x, in(emptySet, x) /\ forall(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x))))
 
   /**
    * Foundation/Regularity Axiom --- Every non-empty set `x` has an `∈`-minimal
@@ -114,7 +114,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
    *
    * `() |- (x != ∅) ==> ∃ y ∈ x. ∀ z. z ∈ x ⇒ ! z ∈ y`
    */
-  final val foundationAxiom: AXIOM = Axiom("foundationAxiom", !(x === emptySet) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
+  final val foundationAxiom: AXIOM = Axiom(!(x === emptySet) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
 
   private val zAxioms: Set[(String, AXIOM)] = Set(
     ("EmptySet", emptySetAxiom),
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index aa363204..56c314f0 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -22,7 +22,6 @@ private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
    * satisfy `P` for each `a ∈ x`.
    */
   final val replacementSchema: AXIOM = Axiom(
-    "replacementSchema",
     forall(A, in(A, x) ==> existsOne(B, P(x, A, B))) ==>
       exists(y, forall(B, in(B, y) <=> exists(A, in(A, x) /\ P(x, A, B))))
   )
diff --git a/src/test/scala/lisa/automation/TableauTest.scala b/src/test/scala/lisa/automation/TableauTest.scala
new file mode 100644
index 00000000..4e11402e
--- /dev/null
+++ b/src/test/scala/lisa/automation/TableauTest.scala
@@ -0,0 +1,130 @@
+package lisa.test.automation
+
+import lisa.automation.Tableau._
+import lisa.prooflib.Exports.*
+import lisa.prooflib.Substitution.*
+import lisa.settheory.SetTheoryLibrary.{_, given}
+import lisa.utils.K.SCProofChecker.checkSCProof
+import lisa.utils.parsing.FOLPrinter.prettyFormula
+import lisa.utils.parsing.FOLPrinter.prettySCProof
+import lisa.utils.parsing.FOLPrinter.prettyTerm
+import org.scalatest.funsuite.AnyFunSuite
+
+class TableauTest extends AnyFunSuite {
+  import TableauTest.*
+
+  test(s"Propositional Positive cases (${posi.size})") {
+    assert(posi.forall(_._3), posi.map((i, f, b, proof, judg) => s"$i $b" + (if !b then s" $f" else "")).mkString("\n"))
+    if posi.exists(tup => tup._5.nonEmpty & !tup._5.get.isValid) then
+      fail("A proof is wrong: " + posi.map(tup => if tup._5.nonEmpty & !tup._5.get.isValid then prettySCProof(tup._5.get) + "\n").mkString("\n"))
+  }
+
+  test(s"First Order Quantifier Free Positive cases (${posqf.size})") {
+    assert(posqf.forall(_._3), posqf.map((i, f, b, proof, judg) => (s"$i $b" + (if !b then s" $f" else ""))).mkString("\n"))
+    if posqf.exists(tup => tup._5.nonEmpty & !tup._5.get.isValid) then
+      fail("A proof is wrong: " + posi.map(tup => if tup._5.nonEmpty & !tup._5.get.isValid then prettySCProof(tup._5.get) + "\n").mkString("\n"))
+  }
+
+  test(s"First Order Easy Positive cases (${poseasy.size})") {
+    assert(poseasy.forall(_._3), poseasy.map((i, f, b, proof, judg) => (s"$i $b" + (if !b then s" $f" else ""))).mkString("\n"))
+    if poseasy.exists(tup => tup._5.nonEmpty & !tup._5.get.isValid) then
+      fail("A proof is wrong: " + posi.map(tup => if tup._5.nonEmpty & !tup._5.get.isValid then prettySCProof(tup._5.get) + "\n").mkString("\n"))
+  }
+
+  test(s"First Order Hard Positive cases (${poshard.size})") {
+    assert(poshard.forall(_._3), poshard.map((i, f, b, proof, judg) => (s"$i $b" + (if !b then s" $f" else ""))).mkString("\n"))
+    if poshard.exists(tup => tup._5.nonEmpty & !tup._5.get.isValid) then
+      fail("A proof is wrong: " + posi.map(tup => if tup._5.nonEmpty & !tup._5.get.isValid then prettySCProof(tup._5.get) + "\n").mkString("\n"))
+  }
+
+}
+object TableauTest {
+
+  val w = variable
+  val x = variable
+  val y = variable
+  val z = variable
+
+  val a = formulaVariable
+  val b = formulaVariable
+  val c = formulaVariable
+  val d = formulaVariable
+  val e = formulaVariable
+
+  val f = function[1]
+  val g = function[1]
+  val h = function[2]
+
+  val P = predicate[1]
+  val Q = predicate[1]
+  val R = predicate[2]
+
+  var doprint: Boolean = false
+  def printif(s: Any) = if doprint then println(s) else ()
+
+  val posi = List(
+    a <=> a,
+    a \/ !a,
+    ((a ==> b) /\ (b ==> c)) ==> (a ==> c),
+    (a <=> b) <=> ((a /\ b) \/ (!a /\ !b)),
+    ((a ==> c) /\ (b ==> c)) <=> ((a \/ b) ==> c),
+    ((a ==> b) /\ (c ==> d)) ==> ((a \/ c) ==> (b \/ d))
+  ).zipWithIndex.map(f =>
+    val res = solve(() |- f._1)
+    (f._2, f._1, res.nonEmpty, res, res.map(checkSCProof))
+  )
+
+  // Quantifier Free
+
+  val posqf = List(
+    posi.map(fo => fo._2.substitute(a := P(h(x, y)), b := P(x), c := R(x, h(x, y)))),
+    posi.map(fo => fo._2.substitute(a := P(h(x, y)), b := P(h(x, y)), c := R(x, h(x, f(x))))),
+    posi.map(fo => fo._2.substitute(a := R(y, y), b := P(h(y, y)), c := R(h(x, y), h(z, y))))
+  ).flatten.zipWithIndex.map(f =>
+    val res = solve(() |- f._1)
+    (f._2, f._1, res.nonEmpty, res, res.map(checkSCProof))
+  )
+
+  // First Order Easy
+
+  val poseasy = List(
+    posi.map(fo => fo._2.substitute(a := forall(x, P(x)), b := forall(x, P(y)), c := exists(x, P(x)))),
+    posi.map(fo => fo._2.substitute(a := forall(x, P(x) /\ Q(f(x))), b := forall(x, P(x) \/ R(y, x)), c := exists(x, Q(x) ==> R(x, y)))),
+    posi.map(fo => fo._2.substitute(a := exists(y, forall(x, P(x) /\ Q(f(y)))), b := forall(y, exists(x, P(x) \/ R(y, x))), c := forall(y, exists(x, Q(x) ==> R(x, y)))))
+  ).flatten.zipWithIndex.map(f =>
+    val res = solve(() |- f._1)
+    (f._2, f._1, res.nonEmpty, res, res.map(checkSCProof))
+  )
+
+  // First Order Hard, from https://isabelle.in.tum.de/library/FOL/FOL-ex/Quantifiers_Cla.html
+
+  val poshard = List(
+    forall(x, P(x) ==> Q(x)) ==> (forall(x, P(x)) ==> forall(x, Q(x))),
+    forall(x, forall(y, R(x, y))) ==> forall(y, forall(x, R(x, y))),
+    forall(x, forall(y, R(x, y))) ==> forall(y, forall(x, R(y, x))),
+    exists(x, exists(y, R(x, y))) ==> exists(y, exists(x, R(x, y))),
+    exists(x, exists(y, R(x, y))) ==> exists(y, exists(x, R(y, x))),
+    (forall(x, P(x)) \/ forall(x, Q(x))) ==> forall(x, P(x) \/ Q(x)),
+    forall(x, a ==> Q(x)) <=> (a ==> forall(x, Q(x))),
+    forall(x, P(x) ==> a) <=> (exists(x, P(x)) ==> a),
+    exists(x, P(x) \/ Q(x)) <=> (exists(x, P(x)) \/ exists(x, Q(x))),
+    exists(x, P(x) /\ Q(x)) ==> (exists(x, P(x)) /\ exists(x, Q(x))),
+    exists(y, forall(x, R(x, y))) ==> forall(x, exists(y, R(x, y))),
+    forall(x, Q(x)) ==> exists(x, Q(x)),
+    (forall(x, P(x) ==> Q(x)) /\ exists(x, P(x))) ==> exists(x, Q(x)),
+    ((a ==> exists(x, Q(x))) /\ a) ==> exists(x, Q(x)),
+    forall(x, P(x) ==> Q(f(x))) /\ forall(x, Q(x) ==> R(g(x), x)) ==> (P(y) ==> R(g(f(y)), f(y))),
+    forall(x, forall(y, P(x) ==> Q(y))) ==> (exists(x, P(x)) ==> forall(y, Q(y))),
+    (exists(x, P(x)) ==> forall(y, Q(y))) ==> forall(x, forall(y, P(x) ==> Q(y))),
+    forall(x, forall(y, P(x) ==> Q(y))) <=> (exists(x, P(x)) ==> forall(y, Q(y))),
+    exists(x, exists(y, P(x) /\ R(x, y))) ==> (exists(x, P(x) /\ exists(y, R(x, y)))),
+    (exists(x, P(x) /\ exists(y, R(x, y)))) ==> exists(x, exists(y, P(x) /\ R(x, y))),
+    exists(x, exists(y, P(x) /\ R(x, y))) <=> (exists(x, P(x) /\ exists(y, R(x, y)))),
+    exists(y, forall(x, P(x) ==> R(x, y))) ==> (forall(x, P(x)) ==> exists(y, R(x, y))),
+    forall(x, P(x)) ==> P(y)
+  ).zipWithIndex.map(f =>
+    val res = solve(() |- f._1)
+    (f._2, f._1, res.nonEmpty, res, res.map(checkSCProof))
+  )
+
+}
diff --git a/src/test/scala/lisa/utilities/SerializationTest.scala b/src/test/scala/lisa/utilities/SerializationTest.scala
new file mode 100644
index 00000000..da2ba1aa
--- /dev/null
+++ b/src/test/scala/lisa/utilities/SerializationTest.scala
@@ -0,0 +1,187 @@
+package lisa.test.utils
+
+import lisa.test.automation.TableauTest
+import lisa.utils.K
+import lisa.utils.K.getJustification
+import lisa.utils.K.|-
+import lisa.utils.Serialization.*
+import org.scalatest.funsuite.AnyFunSuite
+
+import java.io._
+
+//import lisa.automation.TableauTest
+
+class SerializationTest extends AnyFunSuite {
+
+  val theory = K.RunningTheory()
+
+  val testfile = "SerializationTestuioavrebvtaevslbxfgh" // chances of collision with an existing file is quite low
+
+  def test(proof: K.SCProof, name: String, theory: K.RunningTheory, justs: List[theory.Justification]) = {
+    thmsToFile(testfile, theory, List((name, proof, justs.map(("test", _)))))
+    val thm = thmsFromFile(testfile, theory)
+    File(testfile + ".trees").delete()
+    File(testfile + ".proof").delete()
+    thm.head
+  }
+
+  def testMulti(theory: K.RunningTheory, thms: List[(String, K.SCProof, List[theory.Justification])]) = {
+    thmsToFile(testfile, theory, thms.map(thm => (thm._1, thm._2, thm._3.map(("test", _)))))
+    val thm = thmsFromFile(testfile, theory)
+    File(testfile + "test.trees").delete()
+    File(testfile + "test.proof").delete()
+    thm
+  }
+
+  test("exporting a proof to a file and back should work, propositional tableau") {
+    val proofs = TableauTest.posi
+    proofs.foreach(p =>
+      try {
+        val proof = p._4.get
+        val no = p._1
+        test(proof, "posi" + no, theory, Nil)
+      } catch {
+        case e: Exception =>
+          println("Exception thrown for test case posi" + p._1)
+          throw e
+      }
+    )
+  }
+
+  test("exporting a proof to a file and back should work, propositional OL tautology") {
+    val proofs = TableauTest.posi
+    proofs.foreach(p =>
+      try {
+        val formula = p._2
+        val no = p._1
+        val proof = lisa.automation.kernel.OLPropositionalSolver.solveSequent(() |- formula.underlying) match {
+          case Left(proof) => proof
+          case Right(_) => throw new Exception("OLPropositionalSolver failed to prove a tautology")
+        }
+        test(proof, "posiOL" + no, theory, Nil)
+      } catch {
+        case e: Exception =>
+          println("Exception thrown for test case posi" + p._1)
+          throw e
+      }
+    )
+  }
+
+  test("exporting a proof to a file and back should work, first order quantifier free tableau") {
+    val proofs = TableauTest.posqf
+    proofs.foreach(p =>
+      try {
+        val proof = p._4.get
+        val no = p._1
+        test(proof, "posqf" + no, theory, Nil)
+      } catch {
+        case e: Exception =>
+          println("Exception thrown for test case posqf" + p._1)
+          throw e
+      }
+    )
+  }
+
+  test("exporting a proof to a file and back should work, first order quantifier free OL tautology") {
+    val proofs = TableauTest.posqf
+    proofs.foreach(p =>
+      try {
+        val formula = p._2
+        val no = p._1
+        val proof = lisa.automation.kernel.OLPropositionalSolver.solveSequent(() |- formula.underlying) match {
+          case Left(proof) => proof
+          case Right(_) => throw new Exception("OLPropositionalSolver failed to prove a tautology")
+        }
+        test(proof, "posqfOL" + no, theory, Nil)
+      } catch {
+        case e: Exception =>
+          println("Exception thrown for test case posqf" + p._1)
+          throw e
+      }
+    )
+  }
+
+  test("exporting a proof to a file and back should work, first order easy tableau") {
+    val proofs = TableauTest.poseasy
+    proofs.foreach(p =>
+      try {
+        val proof = p._4.get
+        val no = p._1
+        test(proof, "poseasy" + no, theory, Nil)
+      } catch {
+        case e: Exception =>
+          println("Exception thrown for test case poseasy" + p._1)
+          throw e
+      }
+    )
+  }
+
+  test("exporting a proof to a file and back should work, first order hard tableau") {
+    val proofs = TableauTest.poshard
+    proofs.foreach(p =>
+      try {
+        val proof = p._4.get
+        val no = p._1
+        test(proof, "poshard" + no, theory, Nil)
+      } catch {
+        case e: Exception =>
+          println("Exception thrown for test case poshard" + p._1)
+          throw e
+      }
+    )
+  }
+
+  test("exporting a proof to a file and back should work, with imports") {
+    import lisa.mathematics.settheory.SetTheory as ST
+    val thms = List(
+      // ("russelsParadox", ST.russelsParadox),
+      ("setUnionMembership", ST.setUnionMembership),
+      ("inductiveSetExists", ST.inductiveSetExists),
+      ("setWithNoElementsIsEmpty", ST.setWithNoElementsIsEmpty),
+      ("emptySetIsItsOwnOnlySubset", ST.emptySetIsItsOwnOnlySubset)
+    )
+    thms.foreach(thm =>
+      try {
+        val proof = thm._2.kernelProof.get
+        val justifs = thm._2.highProof.get.justifications.map(_.innerJustification)
+
+        test(proof, thm._1 + "_test", ST.theory, justifs)
+      } catch {
+        case e: Exception =>
+          println("Exception thrown for string encoding-decoding of theorem " + thm._1)
+          throw e
+      }
+    )
+  }
+
+  test("exporting multiple theorems at once to a file and back should work") {
+    import lisa.mathematics.settheory.SetTheory as ST
+    val thms = List(
+      // ("russelsParadox", ST.russelsParadox),
+      ("setUnionMembership", ST.setUnionMembership),
+      ("inductiveSetExists", ST.inductiveSetExists),
+      ("setWithNoElementsIsEmpty", ST.setWithNoElementsIsEmpty),
+      ("emptySetIsItsOwnOnlySubset", ST.emptySetIsItsOwnOnlySubset)
+    )
+
+    val thmBack = testMulti(
+      ST.theory,
+      thms.map(thm =>
+        val proof = thm._2.kernelProof.get
+        val justifs = thm._2.highProof.get.justifications.map(_.innerJustification)
+
+        (thm._1, proof, justifs)
+      )
+    )
+    assert(thmBack.length == thms.length)
+    thmBack
+      .zip(thms)
+      .foreach(pair => {
+        val thm = pair._1
+        val thmOrig = pair._2
+        assert(thm._1.name == thmOrig._1)
+        assert(thm._1.proposition == thmOrig._2.innerJustification.proposition)
+      })
+  }
+
+}
-- 
GitLab