Машинно-верифицированная математика для Claude Code

general

math — это скилл для Claude Code, который реализует многоуровневый стек машинно-верифицированного решения математических задач. Архитектура включает четыре слоя: SymPy для точных символьных вычислений, Z3 для решения задач удовлетворения ограничений (SAT/SMT), Scratchpad для пошаговой проверки выводов и Lean 4 для формальной верификации теорем. Скилл охватывает десять математических областей — абстрактную алгебру, теорию категорий, комплексный анализ, функциональный анализ, линейную алгебру, математическую логику, теорию меры, вещественный анализ и топологию, — каждая со своими файлами SKILL.md, THEOREMS.md и EXAMPLES.md. Подходит исследователям и инженерам, которым нужно не просто получить ответ, а доказать корректность: скрипты sympy_compute.py запускаются через uv, а Lean 4 компилируется командой lake build.