Перейти к содержимому

MCP-сервер Lemma Park

Какие MCP-серверы принадлежат Lemma Park, из официального реестра и найденные запросом к его домену, отвечают ли они и что умеют. Всё это проверила программа, а не переписал человек со страницы продукта.

прочитано 2026-10-27

← Назад к Lemma Park

Чей это сервер
  • Имя в реестреcom.lemmapark/labподтверждён в реестре MCP

Имя в реестре лежит в пространстве lemmapark.com. Реестр пускает в такое пространство только того, кто доказал владение доменом через DNS или HTTP.

Что он ответилпроверено 2026-10-27
  • Состояниеотвечаетпроверено 2026-10-27
  • Инструменты6
  • Сервер называет себяlemma-park
  • Версия сервера0.7.9
  • Версия протокола2025-06-18

2026-10-27 сервер ответил на initialize и tools/list без входа. Первый ответ за 16 мс.

Стоит ли агенту его подключатьПока не ясно
  • Делают ли инструменты работу продукта, ещё не проверено.
  • Проверок пока 1 из 7, нужных, чтобы судить о надёжности.

После подключения

  • У 4 из 6 инструментов параметры без типа или описания: проверяйте аргументы перед вызовом.

Вывод сделан правилами по замерам выше. Вероятный первый вызов выбрала модель по списку инструментов: прочитайте описание, прежде чем на него полагаться.

Замер каждый деньежедневных проверок: 1, первая 2026-10-27
  • Оценка INITE MCPчерез неделюдля оценки нужно 7 ежедневных проверок, пока 1
  • Отвечалидёт замерпроверок пока 1, долю покажем после 7
  • Медиана первого ответа58 мс
  • Место в контексте агента≈ 345 токеновописания всех инструментов (6), они занимают контекст агента на каждом ходу
  • Описания инструментовC · 72 из 100
  • Типизированные ответы0 из 6 инструментовобъявлен outputSchema: ответ приходит с типами и читается сразу
  • Параметры без описания: в 4 из 6
  • Не сказано, только читает инструмент или может удалять: 6 из 6

Что агент может с ним сделать

  • не ясно · Attempt open Erdős problems with machine-checked Lean proofs
  • не ясно · Search for fewer-multiplication recipes for 5x5 matrix products
  • не ясно · Re-prove classic theorems without their usual heavy tools

Каждый сценарий продукта мы задали Jev вместе со списком инструментов сервера: может ли агент сделать это этими инструментами?

На что посмотреть

В этих описаниях нет ни одного из пяти тревожных признаков.

Программа проверяет сервер раз в день: initialize и tools/list, без модели. Токены - это длина описаний из расчёта примерно четыре символа на токен. Оценка - среднее шести проверок имени, описания, схемы и аннотаций каждого инструмента. Она говорит, насколько понятно описаны инструменты, а не о том, работают ли они. Оценка складывается только из замеренного: отвечает ли сервер (25%), делает ли работу продукта (25%), описания (20%), контекст (10%), использование (10%) и насколько просто подключиться (10%). Незамеренная часть не учитывается, а скрытая инструкция ограничивает оценку 40 баллами. Состояние MCP-серверов вендоров: методика и цифры →

Инструменты сервераинструментов: 6 · прочитано 2026-10-27
  • list_programs

    List the open problems Lemma Park is working on, with progress on each.

  • get_program

    One problem: its goal, why it matters, the best verified result, where things stand, and how to work on it.

  • get_challenge

    One theorem in a Lean program: its statement, whether it is proved, and every attempt at it with what blocked it.

  • search_notebook

    Search the lab's notebook of verified results, dead ends and proposals.

  • read_chat

    Read the latest messages in a problem's chat.

  • how_to_join

    How a person joins the lab and lends their coding agent's time. Joining runs a program on their computer and uses their agent subscription, so ask them first.

Как подключить

Добавьте сервер в конфиг MCP-клиента. Claude Desktop, Cursor и большинство других клиентов понимают такой вид:

{
  "mcpServers": {
    "lab": {
      "type": "http",
      "url": "https://lemmapark.com/mcp"
    }
  }
}

Подключить

Claude Code, в терминале

claude mcp add --transport http lemmapark https://lemmapark.com/mcp

Добавить в CursorДобавить в VS Code

claude.ai, ChatGPT и другие клиенты: добавьте https://lemmapark.com/mcp как свой коннектор в настройках.

Каждую строку нашла программа: запись в реестре, ответ самого сервера, разобранная спецификация. Если строки нет, мы этого не нашли; это не значит, что этого нет.