odin-lean

v2.0.2

ODIN workflows for Lean proofs and formal verification.

CodexClaude Code1 Skill

By OutlineDrivenLicense: SEE LICENSE IN LICENSE35 GitHub starsUpdated 3 hours ago

Directory evidence

Runtimes: Codex and Claude Code
Parsed components: 1 skill or MCP entry
Source updated: Sep 3, 2026
Manifest status: Canonical path parsed

The directory validates manifest shape and source location. It does not execute the plugin or provide a security endorsement. Review the indexing methodology →

Install odin-lean for Codex and Claude Code

Installs for the current user

codex plugin marketplace add IchenDEV/agent-plugin-mkt
codex plugin marketplace upgrade agent-plugin-marketplace
codex plugin add odin-lean@agent-plugin-marketplace

Paste and run these commands in a terminal with Codex. They add and refresh the PluginsMP catalog, then install this plugin.

The installer fetches third-party code from the source repository shown on this page. This directory validates manifest structure and source location, but does not perform a security audit; review the manifest, components, and source before installing.

Get the source manually

$ git clone https://github.com/OutlineDriven/odin-claude-plugin

Clone the source repository, then follow its setup instructions to add the plugin to a compatible client. The plugin root is plugins/odin-lean/.

Plugin files

plugins/odin-lean/

├── .codex-plugin/plugin.json
├── .claude-plugin/plugin.json
└── skills/writing-lean-proofs/SKILL.md

Included Skills1

writing-lean-proofsskills/writing-lean-proofs/SKILL.md

Use when asked to design, write, review, refactor, lint, or performance-diagnose Lean 4 proofs, libraries, or tactic extensions under Mathlib conventions. Not for non-Lean code or changes outside Lean source, library API, proof structure, and linter configuration.

Plugin manifests2

plugins/odin-lean/.codex-plugin/plugin.json

{
  "name": "odin-lean",
  "version": "2.0.2",
  "description": "ODIN workflows for Lean proofs and formal verification.",
  "keywords": [
    "odin",
    "outlinedriven",
    "agent-skills",
    "lean"
  ],
  "author": {
    "name": "OutlineDriven",
    "url": "https://github.com/OutlineDriven"
  },
  "interface": {
    "displayName": "ODIN Lean",
    "shortDescription": "ODIN workflows for Lean proofs and formal verification.",
    "category": "Coding"
  }
}

plugins/odin-lean/.claude-plugin/plugin.json

{
  "$schema": "https://json.schemastore.org/claude-code-plugin-manifest.json",
  "name": "odin-lean",
  "displayName": "ODIN Lean",
  "version": "2.0.2",
  "description": "ODIN workflows for Lean proofs and formal verification.",
  "author": {
    "name": "OutlineDriven",
    "url": "https://github.com/OutlineDriven"
  },
  "homepage": "https://github.com/OutlineDriven/odin-claude-plugin",
  "repository": "https://github.com/OutlineDriven/odin-claude-plugin",
  "license": "SEE LICENSE IN LICENSE",
  "keywords": [
    "odin",
    "outlinedriven",
    "agent-skills",
    "lean"
  ]
}