diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index df8db18..3fc828e 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -326,6 +326,11 @@ Arguments:
 -/
 elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
 
+  -- Check that the statement name is a lemma in the doc
+  match statementName with
+  | some name => checkInventoryDoc .Lemma name.getId
+  | none => pure Unit.unit
+
   let lvlIdx ← getCurLevelIdx
   let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
     ("level" ++ toString lvlIdx : String)