claudecodex

choir

Community-led formalization in kernel-checked proof assistants (Lean 4, Isabelle, Rocq) — start a project as overseer or join one as a contributor.

118 on GitHubby Weber-GeoMLv0.1.3Apache-2.0updated 26 days agoCoding
/

Plugin choir from marketplace choir in Weber-GeoML/Choir. Commands read from the repo's manifest — 25 days ago.

What it installs

Skills (2)

  • formalize

    Start or resume a Choir formalization project as its overseer — formalize a theorem, paper, textbook chapter, or folder of sources in Lean 4, Isabelle, or Rocq by orchestrating AI contributor agents behind a deterministic verification gate. Use when the user wants to formalize something with Choir o

  • join

    Join a Choir formalization project as a contributor — set up this machine and start proving tasks (Lean 4, Isabelle, or Rocq) with your own agent on your own LLM account. Use when the user wants to join, contribute to, or work on a Choir project or its GitHub repo.

Slash commands (1)

  • /choir:purge

    Remove this machine's local Choir state for a project, or all of it

View source on GitHub

Similar plugins

mattpocock-skills

claude

Matt Pocock's agent skills for real engineering (grilling, spec/ticket flows, TDD, code review, domain modelling and more).

39 skills

mattpocock/skills 323,108

superpowers

claudecodex

Core skills library for Claude Code: TDD, debugging, collaboration patterns, and proven techniques

15 skills · hooks

obra/superpowers 316,836

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

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

context7

claudecodex

Up-to-date documentation lookup. Pull version-specific documentation and code examples directly from source repositories into your coding agent's context.

1 MCP server

upstash/context7 64,709

Maintain choir?

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