---
title: "Given the theorem name and file path of a Lean theorem in mathlib, initialize the proof search. The response includes the initial state and its state ID."
method: POST
path: "/initialize_proof_search"
---

# Given the theorem name and file path of a Lean theorem in mathlib, initialize the proof search. The response includes the initial state and its state ID.

`POST /initialize_proof_search`

## Request body

- InitializeProofSearchRequest
  - `theorem_name` string — The name of the target theorem to prove in mathlib.
  - `theorem_file_path` string — The file path of the target theorem in mathlib.

## Response `200`

OK

---

[API](https://skmtc.dev/lean-dojo/apis/lean.md) · [All operations](https://skmtc.dev/lean-dojo/apis/lean/llms.txt) · [OpenAPI document](https://skmtc-service-production.skmtc.workers.dev/v1/apis/lean-dojo/lean/revisions/7e9eba959783/schema)