claudecodex

autoform

Set up, plan, publish, prove, and review Lean formalizations as linked Markdown nodes checked through Lean LSP and REPL.

143 on GitHubby Vivien Cabannesv0.7.0MITupdated todayproductivity
/

Plugin autoform from marketplace autoform in facebookresearch/autoform-bot. Commands read from the repo's manifest — today.

This plugin runs code on your machine — it starts local MCP servers. The exact commands are listed below; read them before installing.

What it installs

Skills (7)

  • agent-review

    Judge an Autoform mathematical roadmap or Lean formalization with explicit, evidence-based rubrics. Use for an independent agent audit of source coverage, DAG quality, statement faithfulness, proof integrity, axioms, sorries, or Mathlib contribution quality; do not use merely to prepare a visualizat

  • debrief-orchestrator

    Once a Setup, Roadmap, or Formalize run is over, record what got in the way: friction from the user's local setup, kept apart from friction with AutoformBot itself, and draft an AutoformBot issue from the latter for the user to review and send. On by default; `AUTOFORM_DEBRIEF=0` turns it off.

  • develop-plugin

    Maintain AutoformBot's code, skills, tests, examples, and installation.

  • formalize

    Formalize ready leaves from an existing Autoform Markdown roadmap in Lean, using native agents and recording only verified progress. Use for proof execution; send missing scope or DAG structure to Roadmap.

  • human-review

    Prepare and guide human inspection of an Autoform roadmap or formalization through its Obsidian vault and rendered blueprint site. Use when a person wants to browse, approve, reject, or discuss scope, dependencies, progress, source links, or Lean artifacts visually; do not substitute an autonomous a

  • roadmap

    Build, continue, inspect, or visualize a source-grounded mathematical roadmap and theorem DAG in an existing Autoform Markdown blueprint. Use for source research, repository-wide inventories of existing and planned mathematics, scope, coverage, milestones, and roadmap articles; do not create reposit

  • setup

    Set up, inspect, or repair repository infrastructure for an Autoform Lean project, including the Lean/Mathlib shell, an in-repository Obsidian-compatible blueprint vault, ignore rules, MkDocs, GitHub Pages, and verification CI, with optional Zulip community synchronization. Use for new repositories,

MCP servers (2)

  • autoform-lsp

    runs: uv run --project ${CLAUDE_PLUGIN_ROOT} python -m servers.lsp.server

  • autoform-repl

    runs: uv run --project ${CLAUDE_PLUGIN_ROOT} --extra repl python -m servers.repl.server

View source on GitHub

Similar plugins

caveman

claude

Talk like caveman. Cut filler. Keep technical details explicit.

22 skills · 1 command · 3 agents · hooks

JuliusBrussee/caveman 119,462

claude-mem

claudecodex

Persistent memory for Claude Code: the next session starts where the last one left off.

29 skills · 1 MCP server · hooks

thedotmack/claude-mem 116,618

Taste Skill

claudecodex

tasteskill 2.5.1: professional company websites at the figma.com and x.ai level, with one section per screen, real photographs, real product UI, effects kept for tech and gaming pages, and a real-browser checker and finish gate.

1 skill

Leonxlnx/taste-skill 114,391

career-ops

claudecodex

Open-source AI job search that runs locally in your AI coding CLI: scan job portals, evaluate listings into a structured A-H report with a 1-5 score, tailor your CV, track applications

5 skills · hooks

career-ops-hq/career-ops 82,253

mem0

claudecodex

Cross-session memory and token savings for coding agents.

6 skills · 1 agent · 1 MCP server · hooks

mem0ai/mem0 68,893

pake

claudecodex

Package any website or local web build into a lightweight desktop app with Pake CLI.

1 skill

tw93/Pake 63,463

Maintain autoform?

This page updates itself from your repo. Add the badge to your README, or get it Featured to pin it above the organic results with a followed link to your site.

claude & codex pluginslisted