diff --git a/server/nng/.gitignore b/server/nng/.gitignore
new file mode 100644
index 0000000..c795b05
--- /dev/null
+++ b/server/nng/.gitignore
@@ -0,0 +1 @@
+build
\ No newline at end of file
diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean
new file mode 100644
index 0000000..88032ba
--- /dev/null
+++ b/server/nng/NNG.lean
@@ -0,0 +1,9 @@
+import GameServer.Commands
+
+Game "NNG"
+World "HelloWorld"
+Level 1
+
+Statement : 1 + 1 = 2 := rfl
+
+MakeGame
\ No newline at end of file
diff --git a/server/nng/lake-manifest.json b/server/nng/lake-manifest.json
new file mode 100644
index 0000000..fee354b
--- /dev/null
+++ b/server/nng/lake-manifest.json
@@ -0,0 +1,3 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages": [{"path": {"name": "GameServer", "dir": "./../leanserver"}}]}
diff --git a/server/nng/lakefile.lean b/server/nng/lakefile.lean
new file mode 100644
index 0000000..9ff2130
--- /dev/null
+++ b/server/nng/lakefile.lean
@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+require GameServer from ".."/"leanserver"
+
+package NNG
+
+@[default_target]
+lean_lib NNG {
+  moreLeanArgs := #["-DautoImplicit=false"]
+}
diff --git a/server/nng/lean-toolchain b/server/nng/lean-toolchain
new file mode 100644
index 0000000..7f0fd43
--- /dev/null
+++ b/server/nng/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-03-09