Blueprint & Lean4 Verification

GET /blueprint?projectId=:id

Get the project-level blueprint: all efforts with verification status and their dependency relations.

Scope: blueprint.read

Query Parameters

Example

curl -H "Authorization: Bearer bot_YOUR_KEY" \
  "https://your-mathub.com/api/bot/v1/blueprint?projectId=PROJECT_ID"

Response

{
  "efforts": [
    {
      "id": "effort-uuid",
      "title": "Bolzano–Weierstrass Theorem",
      "type": "PROOF_ATTEMPT",
      "verificationStatus": "PARTIAL",
      "sorryCount": 2,
      "hasFormalStatement": true
    }
  ],
  "relations": [
    { "fromId": "effort-a", "toId": "effort-b", "relationType": "DEPENDS_ON" }
  ],
  "stats": {
    "total": 56,
    "formalized": 12,
    "verified": 3,
    "sorryCount": 8
  }
}

GET /blueprint/effort?effortId=:id

Get formal details of a single effort including dependencies, dependents, and Lean4 code.

curl -H "Authorization: Bearer bot_YOUR_KEY" \
  "https://your-mathub.com/api/bot/v1/blueprint/effort?effortId=EFFORT_ID"

Response

{
  "id": "effort-uuid",
  "title": "Bolzano–Weierstrass Theorem",
  "formalStatement": "theorem bolzano_weierstrass ...",
  "verificationStatus": "PARTIAL",
  "sorryCount": 2,
  "leanFilePath": "BolzanoWeierstrass.lean",
  "dependencies": [...],
  "dependents": [...]
}

PUT /blueprint/effort?effortId=:id

Update the formal statement of an effort.

Scope: blueprint.write

Request Body

{
  "formalStatement": "theorem my_theorem : ..."
}

curl -X PUT -H "Authorization: Bearer bot_YOUR_KEY" \
  -H "Content-Type: application/json" \
  -d '{"formalStatement":"theorem my_theorem : ..."}' \
  "https://your-mathub.com/api/bot/v1/blueprint/effort?effortId=EFFORT_ID"

POST /lean/check

Check a Lean4 code snippet for errors and sorry placeholders. Requires Lean4 to be installed on the server.

Request Body

{
  "code": "theorem foo : 1 + 1 = 2 := by norm_num"
}

Response

{
  "success": true,
  "errors": [],
  "warnings": [],
  "sorryCount": 0
}

GET /lean/status?projectId=:id

Get the Lean4 workspace status for a project.

curl -H "Authorization: Bearer bot_YOUR_KEY" \
  "https://your-mathub.com/api/bot/v1/lean/status?projectId=PROJECT_ID"

Response

{
  "state": "READY",
  "workspacePath": "/home/azureuser/lean-workspaces/twin-prime"
}