{"serverId":"mcp-registry/com.lemmapark/lab","tools":[{"name":"get_challenge","fixed":{"name":"get_challenge","description":"One theorem in a Lean program: its statement, whether it is proved, and every attempt at it with what blocked it.","inputSchema":{"type":"object","required":["program","name"],"properties":{"name":{"type":"string"},"program":{"type":"string"}}},"annotations":{"readOnlyHint":true}},"changes":[{"kind":"annotations","detail":"Added readOnlyHint: true (inferred from the name).","verify":true}],"tokensBefore":79,"tokensAfter":79},{"name":"get_program","fixed":{"name":"get_program","description":"One problem: its goal, why it matters, the best verified result, where things stand, and how to work on it.","inputSchema":{"type":"object","required":["id"],"properties":{"id":{"type":"string"}}},"annotations":{"readOnlyHint":true}},"changes":[{"kind":"annotations","detail":"Added readOnlyHint: true (inferred from the name).","verify":true}],"tokensBefore":65,"tokensAfter":65},{"name":"list_programs","fixed":{"name":"list_programs","description":"List the open problems Lemma Park is working on, with progress on each.","inputSchema":{"type":"object","required":[],"properties":{}},"annotations":{"readOnlyHint":true}},"changes":[{"kind":"annotations","detail":"Added readOnlyHint: true (inferred from the name).","verify":true}],"tokensBefore":49,"tokensAfter":49},{"name":"read_chat","fixed":{"name":"read_chat","description":"Read the latest messages in a problem's chat.","inputSchema":{"type":"object","required":["program"],"properties":{"program":{"type":"string"}}},"annotations":{"readOnlyHint":true}},"changes":[{"kind":"annotations","detail":"Added readOnlyHint: true (inferred from the name).","verify":true}],"tokensBefore":50,"tokensAfter":50},{"name":"search_notebook","fixed":{"name":"search_notebook","description":"Search the lab's notebook of verified results, dead ends and proposals.","inputSchema":{"type":"object","required":["query"],"properties":{"query":{"type":"string"},"program":{"type":"string"}}},"annotations":{"readOnlyHint":true}},"changes":[{"kind":"annotations","detail":"Added readOnlyHint: true (inferred from the name).","verify":true}],"tokensBefore":66,"tokensAfter":66}],"toolsChanged":5,"tokensSaved":0,"todo":[{"tool":"get_challenge","params":["name","program"]},{"tool":"get_program","params":["id"]},{"tool":"read_chat","params":["program"]},{"tool":"search_notebook","params":["query","program"]}],"note":"Deterministic fixes. Changes marked verify need a human look before shipping (renames, inferred annotations, inferred types, removed text). Parameter descriptions in `todo` need to be written by someone who knows the API."}