diff --git a/Main.lean b/Main.lean
index 9f2d459..9481f2b 100644
--- a/Main.lean
+++ b/Main.lean
@@ -46,6 +46,7 @@ def execute (command: Command): Subroutine Lean.Json := do
     match Lean.fromJson? command.payload with
     | .ok args => inspect args
     | .error x => return errorJson x
+  | "clear" => clear
   | "expr.type" =>
     match Lean.fromJson? command.payload with
     | .ok args => expr_type args
@@ -94,6 +95,11 @@ def execute (command: Command): Subroutine Lean.Json := do
         boundExpr? := boundExpr?,
         module? := module?
       }: InspectResult)
+  clear : Subroutine Lean.Json := do
+    let state ← get
+    let nTrees := state.proofTrees.size
+    set { state with proofTrees := #[] }
+    return Lean.toJson ({ nTrees := nTrees }: ClearResult)
   expr_type (args: ExprType): Subroutine Lean.Json := do
     let env ← Lean.MonadEnv.getEnv
     match syntax_from_str env args.expr with
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index d3b3f60..7d0cb8f 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -42,6 +42,10 @@ structure InspectResult where
   module?: Option String
   deriving Lean.ToJson
 
+structure ClearResult where
+  nTrees: Nat
+  deriving Lean.ToJson
+
 -- Get the type of an expression
 structure ExprType where
   expr: String