Agent Plugins Marketplace
← All plugins

english-to-lean

v0.1.0

Translate math statements from English into faithful, compilable Lean 4 + Mathlib theorems, with junk-value checks and back-translation.

Claude Code1 Skill

By tristan-mrtnLicense: MIT0 GitHub starsUpdated 3 hours ago

Directory evidence

Runtimes
Claude Code
Parsed components
1 skill or MCP entry
Source updated
Sep 30, 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 english-to-lean for Claude Code

Installs for the current user
claude plugin marketplace add IchenDEV/agent-plugin-mkt
claude plugin marketplace update agent-plugin-marketplace
claude plugin install english-to-lean@agent-plugin-marketplace

Paste and run these commands in a terminal with Claude Code. 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/tristan-mrtn/english-to-lean4

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

Plugin files

plugins/english-to-lean/
├── .claude-plugin/plugin.json
└── skills/english-to-lean/SKILL.md

Included Skills1

english-to-leanskills/english-to-lean/SKILL.md

Translate a natural-language math statement (English or other languages) into a faithful, compilable Lean 4 + Mathlib theorem statement, with junk-value checks and back-translation. Use for autoformalization, writing Lean statements from textbook or competition problems, or building formal datasets.

Plugin manifests1

plugins/english-to-lean/.claude-plugin/plugin.json
{
  "name": "english-to-lean",
  "version": "0.1.0",
  "description": "Translate math statements from English into faithful, compilable Lean 4 + Mathlib theorems, with junk-value checks and back-translation.",
  "author": {
    "name": "tristan-mrtn"
  },
  "license": "MIT",
  "keywords": [
    "lean",
    "lean4",
    "mathlib",
    "autoformalization",
    "math",
    "formal-verification"
  ]
}

For maintainers

If you maintain this plugin, link to this source-backed listing from your README so users can review its manifest and indexed components.

[english-to-lean on Agent Plugins Marketplace](https://pluginsmp.com/plugins/english-to-lean)