Mathlas — проверка математики
Поиск известных теорем и строгая проверка математических результатов без нейросети
uvx mathlas-mcp
Запускается на вашем компьютере. RusMcp не запускает и не проверяет код пакета — посмотрите исходный код перед установкой.
Установка
Пакет mathlas-mcp из PyPI, последняя версия. Выберите ассистент и добавьте сервер в его настройки.
Настройки → Developer → Edit Config: файл claude_desktop_config.json
{
"mcpServers": {
"mathlas-proverka-matematiki": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
}Выполните в терминале
claude mcp add --transport stdio mathlas-proverka-matematiki -- uvx mathlas-mcpФайл .cursor/mcp.json в проекте или ~/.cursor/mcp.json — для всех проектов
{
"mcpServers": {
"mathlas-proverka-matematiki": {
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
}Файл .vscode/mcp.json в проекте
{
"servers": {
"mathlas-proverka-matematiki": {
"type": "stdio",
"command": "uvx",
"args": [
"mathlas-mcp"
]
}
}
}Переменные окружения
Замените значения вида YOUR_… своими. Необязательные в конфиг не добавлены — допишите их в env, если нужны.
MATHLAS_SEEDнеобязательная- Set to 1 to force the lightweight built-in seed corpus and never load the multi-GB prebuilt index (fast cold start).
MATHLAS_INDEXнеобязательная- Path to a prebuilt index .npz to serve for search_existing_math (optional; the seed corpus is used when absent).
Описание
Mathlas — набор инструментов для ИИ-агентов, решающих математические задачи. Он нужен, чтобы опираться на проверяемые расчёты и известные результаты, а не на догадки модели. Внутри — индекс примерно из 3,68 млн документов с теоремами и результатами. Сервер ищет существующие теоремы по описанию задачи и объявления в библиотеке mathlib через Loogle, распознаёт замкнутую форму для числа и находит целочисленные последовательности в локальной копии OEIS. Можно численно проверить, что выражение равно заданному значению, и запустить настоящее ядро Lean 4 для формальной проверки. Есть помощники для разбора условий теоремы, поиска соотношений между константами, программного поиска в стиле FunSearch и составления плана поиска статей на arXiv; найденные результаты можно добавлять в индекс. Ключ для работы не нужен. Сервер ставится как пакет и запускается на компьютере пользователя.
Инструменты
Список инструментов появится после проверки. Пакет запускается у вас — посмотрите README в исходном коде.
Вопросы, новые серверы, обсуждение MCP
t.me/rusmcp · t.me/RusMcp_bot