diff --git a/README.md b/README.md
index a3c2d38..c4fd0c6 100644
--- a/README.md
+++ b/README.md
@@ -51,6 +51,13 @@ jobs:
     # Allowed values: "true" or "false".
     # Default: false
     check-reservoir-eligibility: false
+    
+    # Check environment with lean4checker.
+    # Lean version must be 4.8 or higher.
+    # The version of lean4checker is automatically detected using `lean-toolchain`.
+    # Allowed values: "true" or "false".
+    # Default: false
+    lean4checker: false 
 ```
 
 ## Examples
diff --git a/action.yml b/action.yml
index 9d26479..7d46952 100644
--- a/action.yml
+++ b/action.yml
@@ -36,9 +36,19 @@ inputs:
     description: |
       Check if the repository is eligible for the reservoir.
       Allowed values: "true" or "false".
-      If check-reservoir-elibility input is not provided, the action will not check for reservoir eligibility.
+      If check-reservoir-eligibility input is not provided, the action will not check for reservoir eligibility.
     required: false
     default: "false"
+  lean4checker:
+    description: |
+      Check environment with lean4checker.
+      Lean version must be 4.8 or higher.
+      The version of lean4checker is automatically detected using `lean-toolchain`.
+      Allowed values: "true" or "false".
+      If lean4checker input is not provided, the action will not check the environment with lean4checker.
+    required: false
+    default: "false"
+
 runs:
   using: "composite"
   steps:
@@ -97,3 +107,8 @@ runs:
           "${{ github.event.repository.stargazers_count }}"\
           "${{ github.event.repository.license.spdx_id }}"
       shell: bash
+
+    - name: check environment with lean4checker
+      if: ${{ inputs.lean4checker == 'true' }}
+      run: ${{ github.action_path }}/scripts/run_lean4checker.sh
+      shell: bash
diff --git a/scripts/run_lean4checker.sh b/scripts/run_lean4checker.sh
new file mode 100755
index 0000000..78d48a5
--- /dev/null
+++ b/scripts/run_lean4checker.sh
@@ -0,0 +1,30 @@
+#!/bin/bash
+set -e
+
+echo "Checking environment with lean4checker"
+
+# clone lean4checker
+echo "Cloning and building lean4checker"
+git clone https://github.com/leanprover/lean4checker
+
+# build and test lean4checker in a subshell
+(
+# detect toolchain version from lean-toolchain file
+# assumes toolchain is of the form ".*:{VERSION}" (e.g., "leanprover/lean4:v4.8.0-rc1")
+toolchain_version=$(< lean-toolchain cut -d: -f 2)
+echo "Detected toolchain version: $toolchain_version"
+
+# checkout version of lean4checker corresponding to toolchain version
+cd lean4checker || exit
+git config advice.detachedHead false # turn off git warning about detached head
+git checkout "$toolchain_version"
+cp ../lean-toolchain .
+
+# build lean4checker and test lean4checker
+lake build
+./test.sh
+)
+
+# run lean4checker
+echo "Running lean4checker"
+lake env lean4checker/.lake/build/bin/lean4checker