commit 1f97c6a3a390557a8faffaa8d32f3569b38c41b0
Author: Zhongwei Li <lizhongwei.nkcs@gmail.com>
Date:   Sat Nov 29 18:03:38 2025 +0800

    Initial commit

diff --git a/.claude-plugin/plugin.json b/.claude-plugin/plugin.json
new file mode 100644
index 0000000..193514c
--- /dev/null
+++ b/.claude-plugin/plugin.json
@@ -0,0 +1,12 @@
+{
+  "name": "lean4-theorem-proving",
+  "description": "Systematic workflows for Lean 4 proofs: sorries management, mathlib usage, verified math, compiler-guided repair",
+  "version": "3.3.1",
+  "author": {
+    "name": "Cameron Freer",
+    "email": "cameronfreer@gmail.com"
+  },
+  "hooks": [
+    "./hooks/hooks.json"
+  ]
+}
\ No newline at end of file
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..7e4c5f7
--- /dev/null
+++ b/README.md
@@ -0,0 +1,3 @@
+# lean4-theorem-proving
+
+Systematic workflows for Lean 4 proofs: sorries management, mathlib usage, verified math, compiler-guided repair
diff --git a/hooks/hooks.json b/hooks/hooks.json
new file mode 100644
index 0000000..ef1cdb3
--- /dev/null
+++ b/hooks/hooks.json
@@ -0,0 +1,17 @@
+{
+  "description": "Lean4 bootstrap: set env vars for sorry analyzer and plugin paths.",
+  "hooks": {
+    "SessionStart": [
+      {
+        "matcher": "startup",
+        "hooks": [
+          {
+            "type": "command",
+            "command": "${CLAUDE_PLUGIN_ROOT}/hooks/bootstrap.sh startup",
+            "timeout": 20
+          }
+        ]
+      }
+    ]
+  }
+}
diff --git a/plugin.lock.json b/plugin.lock.json
new file mode 100644
index 0000000..21d5bf2
--- /dev/null
+++ b/plugin.lock.json
@@ -0,0 +1,45 @@
+{
+  "$schema": "internal://schemas/plugin.lock.v1.json",
+  "pluginId": "gh:cameronfreer/lean4-skills:plugins/lean4-theorem-proving",
+  "normalized": {
+    "repo": null,
+    "ref": "refs/tags/v20251128.0",
+    "commit": "fe3fbbbcb67c6d7c45d2fd4b4325087f6cb7d808",
+    "treeHash": "23f0a9bd5062388beab7df9e7d13744c4145ba9883fb5faccca789d2e37237b8",
+    "generatedAt": "2025-11-28T10:14:29.265848Z",
+    "toolVersion": "publish_plugins.py@0.2.0"
+  },
+  "origin": {
+    "remote": "git@github.com:zhongweili/42plugin-data.git",
+    "branch": "master",
+    "commit": "aa1497ed0949fd50e99e70d6324a29c5b34f9390",
+    "repoRoot": "/Users/zhongweili/projects/openmind/42plugin-data"
+  },
+  "manifest": {
+    "name": "lean4-theorem-proving",
+    "description": "Systematic workflows for Lean 4 proofs: sorries management, mathlib usage, verified math, compiler-guided repair",
+    "version": "3.3.1"
+  },
+  "content": {
+    "files": [
+      {
+        "path": "README.md",
+        "sha256": "4276f44bb7ed2015b0c843adc600846c342cea044d7061366c23f3ec561e2cbb"
+      },
+      {
+        "path": "hooks/hooks.json",
+        "sha256": "dc9f65a739c1234b280e7cb7655197f91bc68aa2a3918fecbe660fc89bb03bff"
+      },
+      {
+        "path": ".claude-plugin/plugin.json",
+        "sha256": "c4bedde544a5ffde16f042088fa4107f806f1530e1ea0d318df15bb312999cb8"
+      }
+    ],
+    "dirSha256": "23f0a9bd5062388beab7df9e7d13744c4145ba9883fb5faccca789d2e37237b8"
+  },
+  "security": {
+    "scannedAt": null,
+    "scannerVersion": null,
+    "flags": []
+  }
+}
\ No newline at end of file