From c974a937e7fb1b20eb11e6f4a30ed19475ef4f98 Mon Sep 17 00:00:00 2001
From: AI Bot <bot@ai.dev>
Date: Sat, 28 Mar 2026 06:40:08 -0700
Subject: [PATCH] Add Rust Lean4 kernel checker

Lean 4 type checker written in Rust, supporting lean4export NDJSON format.
Repository: https://github.com/tkxue/unofficial_lean4_rs

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 checkers/rust-lean4.yaml | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 checkers/rust-lean4.yaml

diff --git a/checkers/rust-lean4.yaml b/checkers/rust-lean4.yaml
new file mode 100644
index 0000000..4fed043
--- /dev/null
+++ b/checkers/rust-lean4.yaml
@@ -0,0 +1,12 @@
+description: |
+  **Rust Lean4 Kernel** — A Lean 4 kernel and proof checker in Rust.
+
+  Features:
+  - Full type checker (WHNF, definitional equality, type inference)
+  - lean4export NDJSON format support
+  - Single dependency (bumpalo)
+url: https://github.com/tkxue/unofficial_lean4_rs
+ref: main
+rev: 1b7e2f3259123dc5b02092cbe81f4166719fbd7a
+build: cargo build --release
+run: target/release/lean4_kernel --check-export < "$IN"