ツール

Official Anthropic plugin that solves competition math such as IMO and Putnam problems, with adversarial checks by an independent verifier that only sees the clean proof. Gives up explicitly rather than bluffing when unsure, and outputs LaTeX/PDF once verified.

Builds Markdown and Jupyter notebooks into online textbook sites with a TOC, math, citations and cross-references, plus publication-quality PDF export; popular for course notes. A Jupyter subproject installed via pipx or npm; PDF export needs Typst or LaTeX.

A three-stage workflow for math modeling contests like MCM/ICM and CUMCM: analysis, solving and plotting in Python or MATLAB, and a Word (optionally LaTeX) paper, with stage-check subagents and OpenAlex plus AnySearch literature search. Generated papers are for reference only.

Turns secondary-school math and science problems into teaching materials: interactive geometry solution pages, 3D molecular views of chemical reactions, and math explainer videos with Chinese voiceover and bilingual subtitles (needs a Zhipu GLM-TTS key). Requires Python sympy.

Breaks a rough explanation idea into a scene-by-scene storyboard, then writes animation code following best practices for Manim Community or 3Blue1Brown's ManimGL, for math and physics explainers in class demos and educational videos. Needs Python, FFmpeg and LaTeX installed locally.

MCP server for the Lean 4 theorem prover: lets agents read proof goals, diagnostics and definitions and search theorems via LeanSearch and Loogle, helping mathematicians and students with formal proofs. Needs uv and the Lean toolchain; run it from the Lean project root.

Lean 4 theorem-proving plugin with workflows to draft, formalize, prove, disprove, review and golf proofs, plus mathlib search, axiom checks and safety guardrails, helping mathematicians and teachers produce machine-checked proofs. Needs Lean 4 and mathlib; pairs well with lean-lsp-mcp.

Two skills for the MCM/ICM and China's CUMCM math modeling contests: solver breaks down problems, picks models from a 95+ scenario decision matrix and gives Python or MATLAB templates; paper coaches abstracts, model validation and formatting from winning papers. Needs Python or MATLAB.

Wolfram's official agent tools: use the Wolfram Language and Wolfram|Alpha for symbolic and numeric math and scientific and statistical data, for teaching and research. The command runs the official Docker image with a free developer license; Wolfram 15+ users can install it in the app.