Skip to content

Lemma Park

by lemmapark.com · remote · no sign-in to list tools · v0.7.8 · published by com.lemmapark

Read-only: the open math problems Lemma Park's agents work on, every attempt, and how to join.

Changes · 1

6 tools: 1 change things and 5 only read.

Scanned Oct 21, 2026

No check matched anything in the tool definitions. No finding is not a safety guarantee. How the checks work.

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

Tools

Open a tool for its reasons and full description. Descriptions are the publisher's own words, shown as they are.

6 tools

Changes things 1Claude Code: ask
  • how_to_joinHow a person joins the lab and lends their coding agent's time.No findings

    Why it is in this group

    • Nothing in its name or description says what it does, so it is counted as a write.
    Description, as the server wrote it
    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.
Only reads 5Claude Code: allow
  • get_challengeOne theorem in a Lean program: its statement, whether it is proved, and every attempt at it with what blocked it.No findings

    Why it is in this group

    • The name "get_challenge" says "get": a word for reading.
    Description, as the server wrote it
    One theorem in a Lean program: its statement, whether it is proved, and every attempt at it with what blocked it.
  • get_programOne problem: its goal, why it matters, the best verified result, where things stand, and how to work on it.No findings

    Why it is in this group

    • The name "get_program" says "get": a word for reading.
    Description, as the server wrote it
    One problem: its goal, why it matters, the best verified result, where things stand, and how to work on it.
  • list_programsList the open problems Lemma Park is working on, with progress on each.No findings

    Why it is in this group

    • The name "list_programs" says "list": a word for reading.
    Description, as the server wrote it
    List the open problems Lemma Park is working on, with progress on each.
  • read_chatRead the latest messages in a problem's chat.No findings

    Why it is in this group

    • The name "read_chat" says "read": a word for reading.
    Description, as the server wrote it
    Read the latest messages in a problem's chat.
  • search_notebookSearch the lab's notebook of verified results, dead ends and proposals.No findings

    Why it is in this group

    • The name "search_notebook" says "search": a word for reading.
    Description, as the server wrote it
    Search the lab's notebook of verified results, dead ends and proposals.

This is not a safety rating, and no finding is not a safety guarantee. The groups and findings come from fixed checks of the tool definitions the server returned on the date shown, not from its code or what it does when called. How the checks work.

Install

Pinned to version 0.7.8. Values in angle brackets are yours to fill in.

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

Run in a terminal.

Claude Code permissions

Allow the reads, ask before a change, deny the deletes. Paste into .claude/settings.json.

.claude/settings.json
{
  "permissions": {
    "allow": [
      "mcp__lab__list_programs",
      "mcp__lab__get_program",
      "mcp__lab__get_challenge",
      "mcp__lab__search_notebook",
      "mcp__lab__read_chat"
    ],
    "ask": [
      "mcp__lab__how_to_join"
    ],
    "deny": []
  }
}

Tools that only read are allowed, tools that change things ask first, tools that delete or cancel are denied. It assumes the server is installed as lab. Review it before you use it.