diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
new file mode 100644
index 0000000..09cd4ca
--- /dev/null
+++ b/.github/workflows/lean_action_ci.yml
@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..d620926
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,4 @@
+/.lake
+
+# import graph
+import_graph.*
\ No newline at end of file
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..27870e5
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+# Summary
\ No newline at end of file
diff --git a/Summary.lean b/Summary.lean
new file mode 100644
index 0000000..a66165b
--- /dev/null
+++ b/Summary.lean
@@ -0,0 +1,2 @@
+import Summary.Modal
+import Summary.Incompleteness
diff --git a/Summary/Incompleteness.lean b/Summary/Incompleteness.lean
new file mode 100644
index 0000000..2d25473
--- /dev/null
+++ b/Summary/Incompleteness.lean
@@ -0,0 +1,6 @@
+import Incompleteness.Arith.First
+import Incompleteness.Arith.Second
+
+#print axioms LO.FirstOrder.Arith.goedel_first_incompleteness
+
+#print axioms LO.FirstOrder.Arith.goedel_second_incompleteness
diff --git a/Summary/Modal.lean b/Summary/Modal.lean
new file mode 100644
index 0000000..9da447c
--- /dev/null
+++ b/Summary/Modal.lean
@@ -0,0 +1,3 @@
+import Foundation.Modal.Kripke.GL.Completeness
+
+#print axioms LO.Modal.Kripke.GL_complete
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..75c21fb
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,145 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "937cd3219c0beffa7b623d2905707d1304da259e",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.39",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "ab9dec5b351bc7e92f30b47031edf13458bc7a1d",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "ab9dec5b351bc7e92f30b47031edf13458bc7a1d",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/FormalizedFormalLogic/Foundation",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "33e08c2b47f966f772df9af60cbdbc5688295bbf",
+   "name": "foundation",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/FormalizedFormalLogic/Arithmetization",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "85e327734277b7f5b91d272d34a060ed21cbfdfa",
+   "name": "arithmetization",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/FormalizedFormalLogic/Incompleteness",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a8ad9e0408c932c95aca6dc136cb081f789aeab9",
+   "name": "incompleteness",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "f93115d0209de6db335725dee900d379f40c0317",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "Summary",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..4ca5ab7
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+require foundation from git "https://github.com/FormalizedFormalLogic/Foundation" @ "master"
+require arithmetization from git "https://github.com/FormalizedFormalLogic/Arithmetization" @ "master"
+require incompleteness from git "https://github.com/FormalizedFormalLogic/Incompleteness" @ "master"
+
+require importGraph from git "https://github.com/leanprover-community/import-graph" @ "68b518c9b352fbee16e6d632adcb7a6d0760e2b7"
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04"
+
+package "Summary" where
+
+@[default_target]
+lean_lib Summary where
+  -- add library configuration options here
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..6a4259f
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.10.0-rc2