diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..14795ae
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,69 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    name: Build Arrow
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v5
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Arrow
+        run: lake build Arrow
+
+  docs:
+    name: Build and Deploy Documentation
+    runs-on: ubuntu-latest
+    needs: build
+    if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v5
+
+      - name: Install Lean
+        uses: leanprover/lean-action@v1
+        with:
+          test: false
+          lint: false
+          use-github-cache: true
+
+      - name: Build Documentation
+        working-directory: docbuild
+        run: lake build Arrow:docs
+
+      - name: Setup Pages
+        uses: actions/configure-pages@v4
+
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v3
+        with:
+          path: 'docbuild/.lake/build/doc'
+
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
deleted file mode 100644
index c48bd68..0000000
--- a/.github/workflows/lean_action_ci.yml
+++ /dev/null
@@ -1,14 +0,0 @@
-name: Lean Action CI
-
-on:
-  push:
-  pull_request:
-  workflow_dispatch:
-
-jobs:
-  build:
-    runs-on: ubuntu-latest
-
-    steps:
-      - uses: actions/checkout@v5
-      - uses: leanprover/lean-action@v1
diff --git a/README.md b/README.md
index 2afe363..ed17dbe 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,5 @@
 # Arrow's impossibility theorem in Lean 4
 
+[![CI](https://github.com/ChihChengLiang/arrow/actions/workflows/ci.yml/badge.svg)](https://github.com/ChihChengLiang/arrow/actions/workflows/ci.yml)
+
 This is an attempt to implement Arrow's impossibility theorem, [Yu 2012](https://sites.math.rutgers.edu/~zeilberg/EM22/yu2012.pdf) specifically, in Lean to practice the language.
diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
new file mode 100644
index 0000000..cca9d86
--- /dev/null
+++ b/docbuild/lake-manifest.json
@@ -0,0 +1,142 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "13ecfbb8be8bbea477028cd3dcf5eae0c92e47b1",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "13ecfbb",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "Arrow",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "474983579ecce1ca7d8a63e65c7ae0b1a22db6a3",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "9484dd63d30bce157c7f98007a9f26ca4dfb7fb6",
+   "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": "29e7df238aa51dba17463e360e68657a8d433f43",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7e097e9a076d5fbe48aa39aceee871af0d011101",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "35029c2f2b553bb408ececd7a3e690bf40b46b3f",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a8191ec244102f576a8cd93399cdd8cc489e47cd",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7ccd5e026eb2b3581915ff3f0d1cd918e18c2ab9",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "06c949a3f4a3b2eb0bd8601e31269b9f4f820aa6",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.88",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "eb165126bfb2988738792c9ae37e09d58e2fec83",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "90217e10b2db6c6c445d30faae7fea453d9782c0",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "77d10578945b31d794214a66937b75a6d4311674",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "docbuild",
+ "lakeDir": ".lake"}
diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml
new file mode 100644
index 0000000..769fcaf
--- /dev/null
+++ b/docbuild/lakefile.toml
@@ -0,0 +1,14 @@
+name = "docbuild"
+reservoir = false
+version = "0.1.0"
+
+[[require]]
+name = "Arrow"
+path = "../"
+
+[[require]]
+scope = "leanprover"
+name = "doc-gen4"
+# If you are developing against a release candidate or a stable version `v4.x`, replace `main` below by `v4.x`.
+# If you do not use `main` keep in mind to update this field as you update your Lean version.
+rev = "13ecfbb"
\ No newline at end of file
diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain
new file mode 100644
index 0000000..c7ad81a
--- /dev/null
+++ b/docbuild/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0-rc1