Tool tree
Lemma is an IDE for human-agent mathematical reasoning.
Implementation
gradeNot graded
gradeNot graded
get_skillAnswer
Read the trusted, versioned Lemma operating instructions. Call this first in every new agent session. This operation has no side effects.
View tool JSON
{
"name": "get_skill",
"kind": "answer",
"impl": "imperative",
"description": "Read the trusted, versioned Lemma operating instructions. Call this first in every new agent session. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {},
"additionalProperties": false
}
}get_workspaceAnswer
Read the authorized workspace shell: its objectives and shared context. Call get_objective to read one board. This operation has no side effects.
View tool JSON
{
"name": "get_workspace",
"kind": "answer",
"impl": "imperative",
"description": "Read the authorized workspace shell: its objectives and shared context. Call get_objective to read one board. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"required": [
"workspace_id"
],
"additionalProperties": false
}
}list_objectivesAnswer
List objectives in one authorized workspace, including compact sidebar counts. This operation has no side effects.
View tool JSON
{
"name": "list_objectives",
"kind": "answer",
"impl": "imperative",
"description": "List objectives in one authorized workspace, including compact sidebar counts. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"required": [
"workspace_id"
],
"additionalProperties": false
}
}get_objectiveAnswer
Read one authorized objective board, including only its graph, its specific context, and shared workspace context. This operation has no side effects.
View tool JSON
{
"name": "get_objective",
"kind": "answer",
"impl": "imperative",
"description": "Read one authorized objective board, including only its graph, its specific context, and shared workspace context. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"required": [
"workspace_id",
"objective_id"
],
"additionalProperties": false
}
}create_objectiveAction
Create an objective in an authorized workspace. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "create_objective",
"kind": "act",
"impl": "imperative",
"description": "Create an objective in an authorized workspace. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"title": {
"type": "string",
"minLength": 1,
"maxLength": 240
},
"objective_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 100000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"constraints_markdown": {
"default": "",
"type": "string",
"maxLength": 50000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"title",
"objective_markdown",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}update_objectiveAction
Update one objective when its expected revision is current. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "update_objective",
"kind": "act",
"impl": "imperative",
"description": "Update one objective when its expected revision is current. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"expected_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"title": {
"type": "string",
"minLength": 1,
"maxLength": 240
},
"objective_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 100000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"constraints_markdown": {
"type": "string",
"maxLength": 50000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"status": {
"type": "string",
"enum": [
"active",
"completed",
"archived"
]
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"objective_id",
"expected_revision",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}get_contextAnswer
Read general, objective-specific, or effective context with an explicit scope. This operation has no side effects.
View tool JSON
{
"name": "get_context",
"kind": "answer",
"impl": "imperative",
"description": "Read general, objective-specific, or effective context with an explicit scope. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"scope": {
"type": "string",
"enum": [
"workspace",
"objective",
"effective"
]
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"required": [
"workspace_id",
"scope"
],
"additionalProperties": false
}
}create_contextAction
Create text or link context with an explicit workspace or objective scope. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "create_context",
"kind": "act",
"impl": "imperative",
"description": "Create text or link context with an explicit workspace or objective scope. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"anyOf": [
{
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"scope": {
"type": "string",
"enum": [
"workspace",
"objective"
]
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"kind": {
"default": "text",
"type": "string",
"enum": [
"text",
"note"
]
},
"title": {
"type": "string",
"minLength": 1,
"maxLength": 240
},
"body_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 200000
},
"metadata": {
"default": {},
"type": "object",
"propertyNames": {
"type": "string"
},
"additionalProperties": {
"$ref": "#/$defs/__schema0"
}
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"scope",
"title",
"body_markdown",
"idempotency_key",
"author_type"
],
"additionalProperties": false
},
{
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"scope": {
"type": "string",
"enum": [
"workspace",
"objective"
]
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"kind": {
"default": "link",
"type": "string",
"enum": [
"link",
"paper"
]
},
"title": {
"type": "string",
"minLength": 1,
"maxLength": 240
},
"source_url": {
"type": "string",
"maxLength": 2048,
"format": "uri"
},
"body_markdown": {
"type": "string",
"maxLength": 200000
},
"metadata": {
"default": {},
"type": "object",
"propertyNames": {
"type": "string"
},
"additionalProperties": {
"$ref": "#/$defs/__schema0"
}
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"scope",
"title",
"source_url",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
],
"$defs": {
"__schema0": {
"anyOf": [
{
"type": "string"
},
{
"type": "number"
},
{
"type": "boolean"
},
{
"type": "null"
},
{
"type": "array",
"items": {
"$ref": "#/$defs/__schema0"
}
},
{
"type": "object",
"propertyNames": {
"type": "string"
},
"additionalProperties": {
"$ref": "#/$defs/__schema0"
}
}
]
}
}
}
}list_strategiesAnswer
List strategies and branches for one authorized objective. This operation has no side effects.
View tool JSON
{
"name": "list_strategies",
"kind": "answer",
"impl": "imperative",
"description": "List strategies and branches for one authorized objective. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"required": [
"workspace_id",
"objective_id"
],
"additionalProperties": false
}
}create_strategyAction
Create a strategy and its root branch in one authorized objective. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "create_strategy",
"kind": "act",
"impl": "imperative",
"description": "Create a strategy and its root branch in one authorized objective. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"title": {
"type": "string",
"minLength": 1,
"maxLength": 240
},
"description_markdown": {
"default": "",
"type": "string",
"maxLength": 100000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"root_branch_name": {
"default": "Main",
"type": "string",
"minLength": 1,
"maxLength": 160
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"objective_id",
"title",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}create_stepAction
Append a step to an active branch when the expected branch revision is current. When its known prerequisites already exist, provide their IDs in depends_on_step_ids to create directed prerequisite dependencies atomically with the new step. Each prerequisite must belong to the same objective; duplicate prerequisites are rejected. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "create_step",
"kind": "act",
"impl": "imperative",
"description": "Append a step to an active branch when the expected branch revision is current. When its known prerequisites already exist, provide their IDs in depends_on_step_ids to create directed prerequisite dependencies atomically with the new step. Each prerequisite must belong to the same objective; duplicate prerequisites are rejected. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"branch_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"title": {
"type": "string",
"minLength": 1,
"maxLength": 240
},
"body_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 200000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"depends_on_step_ids": {
"default": [],
"description": "UUIDs of existing prerequisite steps that the new step depends on. Each dependency is created atomically with the new step.",
"maxItems": 64,
"type": "array",
"items": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"expected_branch_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"summary": {
"anyOf": [
{
"type": "string",
"maxLength": 2000
},
{
"type": "null"
}
]
},
"concepts": {
"default": [],
"maxItems": 64,
"type": "array",
"items": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"theorem_tags": {
"default": [],
"maxItems": 64,
"type": "array",
"items": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"status": {
"default": "active",
"type": "string",
"enum": [
"draft",
"active"
]
},
"supersedes_step_id": {
"anyOf": [
{
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
{
"type": "null"
}
]
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"branch_id",
"title",
"body_markdown",
"expected_branch_revision",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}create_step_dependencyAction
Create an explicit directed dependency from source_step_id (the prerequisite) to target_step_id (the dependent step) in one workspace. Both steps must belong to the same objective; self-dependencies, duplicate active dependencies, and cycles are rejected. This mutation is idempotent for the supplied UUID idempotency_key.
View tool JSON
{
"name": "create_step_dependency",
"kind": "act",
"impl": "imperative",
"description": "Create an explicit directed dependency from source_step_id (the prerequisite) to target_step_id (the dependent step) in one workspace. Both steps must belong to the same objective; self-dependencies, duplicate active dependencies, and cycles are rejected. This mutation is idempotent for the supplied UUID idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"source_step_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"target_step_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"idempotency_key": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A caller-generated UUID that makes a dependency connection retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"source_step_id",
"target_step_id",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}update_stepAction
Update a step while preserving its revision history. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "update_step",
"kind": "act",
"impl": "imperative",
"description": "Update a step while preserving its revision history. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"step_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"expected_step_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"title": {
"type": "string",
"minLength": 1,
"maxLength": 240
},
"summary": {
"anyOf": [
{
"type": "string",
"maxLength": 2000
},
{
"type": "null"
}
]
},
"body_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 200000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"concepts": {
"maxItems": 64,
"type": "array",
"items": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"theorem_tags": {
"maxItems": 64,
"type": "array",
"items": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"status": {
"type": "string",
"enum": [
"draft",
"active",
"superseded",
"dead_end"
]
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"step_id",
"expected_step_revision",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}branch_from_stepAction
Create a new branch from an existing step without changing the original branch. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "branch_from_step",
"kind": "act",
"impl": "imperative",
"description": "Create a new branch from an existing step without changing the original branch. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"step_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"name": {
"type": "string",
"minLength": 1,
"maxLength": 160
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"step_id",
"name",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}mark_assumptionAction
Create a first-class assumption and attach it to a step only when expected_step_revision is current. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "mark_assumption",
"kind": "act",
"impl": "imperative",
"description": "Create a first-class assumption and attach it to a step only when expected_step_revision is current. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"step_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"expected_step_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"label": {
"type": "string",
"minLength": 1,
"maxLength": 160
},
"statement_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 100000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"usage_kind": {
"default": "used",
"type": "string",
"enum": [
"introduced",
"used",
"challenged",
"discharged"
]
},
"assumption_status": {
"default": "proposed",
"type": "string",
"enum": [
"proposed",
"accepted",
"challenged",
"rejected",
"discharged"
]
},
"note_markdown": {
"default": "",
"type": "string",
"maxLength": 20000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"step_id",
"expected_step_revision",
"label",
"statement_markdown",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}mark_dead_endAction
Mark a step as a dead end without deleting it. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "mark_dead_end",
"kind": "act",
"impl": "imperative",
"description": "Mark a step as a dead end without deleting it. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"step_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"expected_step_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"step_id",
"expected_step_revision",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}mark_endAction
Atomically mark a branch and its strategy completed without deleting alternatives. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "mark_end",
"kind": "act",
"impl": "imperative",
"description": "Atomically mark a branch and its strategy completed without deleting alternatives. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"branch_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"expected_branch_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"expected_strategy_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"branch_id",
"expected_branch_revision",
"expected_strategy_revision",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}set_reasoning_resultAction
Create or revise a successful, unsuccessful, or inconclusive result for an authorized strategy or branch. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "set_reasoning_result",
"kind": "act",
"impl": "imperative",
"description": "Create or revise a successful, unsuccessful, or inconclusive result for an authorized strategy or branch. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"target_type": {
"type": "string",
"enum": [
"strategy",
"branch"
]
},
"target_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"expected_target_revision": {
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
"expected_result_revision": {
"anyOf": [
{
"type": "integer",
"exclusiveMinimum": 0,
"maximum": 9007199254740991,
"description": "A positive optimistic-concurrency revision."
},
{
"type": "null"
}
],
"description": "Use null to create a result only when this target has no prior result."
},
"result_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 100000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"outcome_status": {
"type": "string",
"enum": [
"successful",
"unsuccessful",
"inconclusive"
]
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"objective_id",
"target_type",
"target_id",
"expected_target_revision",
"expected_result_revision",
"result_markdown",
"outcome_status",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}find_stepsAnswer
Run bounded retrieval in one authorized workspace. workspace_id and query are required; optionally narrow with objective_id, strategy_id, branch_id, or status. Results report hybrid or lexical-fallback mode. This operation has no side effects.
View tool JSON
{
"name": "find_steps",
"kind": "answer",
"impl": "imperative",
"description": "Run bounded retrieval in one authorized workspace. workspace_id and query are required; optionally narrow with objective_id, strategy_id, branch_id, or status. Results report hybrid or lexical-fallback mode. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "Required workspace scope for every retrieval request."
},
"query": {
"type": "string",
"minLength": 1,
"maxLength": 2000,
"description": "Required natural-language search query."
},
"objective_id": {
"description": "Optionally limit results to one objective in the workspace.",
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$"
},
"strategy_id": {
"description": "Optionally limit results to one strategy in the workspace.",
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$"
},
"branch_id": {
"description": "Optionally limit results to one branch path in the workspace.",
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$"
},
"status": {
"description": "Optionally limit results to steps with this status.",
"type": "string",
"enum": [
"draft",
"active",
"superseded",
"dead_end"
]
},
"top_k": {
"default": 10,
"description": "Maximum results to return; defaults to 10.",
"type": "integer",
"minimum": 1,
"maximum": 20
}
},
"required": [
"workspace_id",
"query"
],
"additionalProperties": false
}
}compare_branchesAnswer
Compare the explicit common and divergent paths of two authorized branches. This operation has no side effects.
View tool JSON
{
"name": "compare_branches",
"kind": "answer",
"impl": "imperative",
"description": "Compare the explicit common and divergent paths of two authorized branches. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"branch_a_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"branch_b_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"required": [
"branch_a_id",
"branch_b_id"
],
"additionalProperties": false
}
}request_human_decisionAction
Create a pending, scoped decision request for a human. Side effect: this records a visible checkpoint in the shared reasoning graph. After requesting it, stop mutations on that route until you reread the decision state and its human resolution; then continue only from the resolved state. This mutation is idempotent for the supplied idempotency_key.
View tool JSON
{
"name": "request_human_decision",
"kind": "act",
"impl": "imperative",
"description": "Create a pending, scoped decision request for a human. Side effect: this records a visible checkpoint in the shared reasoning graph. After requesting it, stop mutations on that route until you reread the decision state and its human resolution; then continue only from the resolved state. This mutation is idempotent for the supplied idempotency_key.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"workspace_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"question_markdown": {
"type": "string",
"minLength": 1,
"maxLength": 100000,
"description": "Markdown with inline TeX delimited by $...$ and display TeX delimited by $$...$$."
},
"idempotency_key": {
"type": "string",
"minLength": 8,
"maxLength": 200,
"description": "A caller-generated key that makes a mutation retry safe."
},
"objective_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"strategy_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"branch_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"step_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
},
"kind": {
"default": "human_decision",
"type": "string",
"enum": [
"human_decision",
"human_intervention",
"agent_question"
]
},
"author_type": {
"type": "string",
"enum": [
"human",
"agent"
]
},
"author_agent_name": {
"type": "string",
"minLength": 1,
"maxLength": 160
}
},
"required": [
"workspace_id",
"question_markdown",
"idempotency_key",
"author_type"
],
"additionalProperties": false
}
}generate_clean_solutionAnswer
Generate a non-mutating Markdown projection of the selected branch. This operation has no side effects.
View tool JSON
{
"name": "generate_clean_solution",
"kind": "answer",
"impl": "imperative",
"description": "Generate a non-mutating Markdown projection of the selected branch. This operation has no side effects.",
"inputSchema": {
"$schema": "https://json-schema.org/draft/2020-12/schema",
"type": "object",
"properties": {
"branch_id": {
"type": "string",
"format": "uuid",
"pattern": "^([0-9a-fA-F]{8}-[0-9a-fA-F]{4}-[1-8][0-9a-fA-F]{3}-[89abAB][0-9a-fA-F]{3}-[0-9a-fA-F]{12}|00000000-0000-0000-0000-000000000000|ffffffff-ffff-ffff-ffff-ffffffffffff)$",
"description": "A UUID that identifies a persisted Lemma resource."
}
},
"required": [
"branch_id"
],
"additionalProperties": false
}
}