Свой агент считает и доказывает через математическое ядро MathKernel по MCP
MathKernel это MCP-сервер со 162 инструментами, через который свой агент считает и доказывает с помощью SymPy, Z3, Lean и других движков, а каждый результат получает метку доверия. Результатов и бенчмарков в источнике нет.
Сделано со своим агентом
Что сделали
MathKernel работает как MCP-сервер (mathkernel-mcp через stdio, 162 инструмента с префиксом math_). Модель разбирает задачу и планирует, а вычисления делает ядро с помощью SymPy, Z3, Lean, mpmath и numba/CUDA. В обычной сессии агент сначала узнаёт доступные возможности, разбирает выражение и создаёт контекст. Потом он вызывает math_reason, чтобы решить задачу и проверить решение. Долгие переборы идут через асинхронные задания. У каждого результата есть метка доверия и цепочка вывода.
Что получилось
Бенчмарков и цифр по результатам источник не приводит, он описывает устройство. Доверие к результату не выше, чем к самому слабому доказательству. Если на входе десятичные числа, результат понижается до численного, и тогда доказательства через Lean и SMT недоступны.
На что обратить внимание
При первом запуске сервера ставятся Lean 4 и Mathlib, если не задать MATHKERNEL_SKIP_LEAN_INSTALL=1. Для CUDA нужны дополнительные pip-пакеты nvidia, иначе вычисления идут на процессоре.
Пояснение
SymPy это библиотека символьной математики на Python, Z3 это решатель логических ограничений (SMT), Lean это система формальных доказательств, а Mathlib его математическая библиотека. mpmath считает с произвольной точностью, numba и CUDA ускоряют вычисления на процессоре и видеокарте.
Кому пригодится
Исследователям и инженерам, которым нужно, чтобы агент не просто считал, а показывал, чем подтверждён результат.
Попробуйте сами
Подключи к этому проекту MCP-сервер [математический инструмент, например MathKernel или система компьютерной алгебры], затем реши с его помощью [задача или система уравнений] и покажи результат, какой движок его получил и как он проверен. Если движки расходятся, отметь это и объясни. Задача готова, когда у меня есть ответ, доказательства к нему и заметка о сделанных допущениях.
Нужна помощь с запуском? Вступайте в сообщество AI Pack ↗
Источник: github.com ·