v1

latestOpenAPI 3.0.12026-07-17222.7 KB

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

theorem_namestring

The name of the target theorem to prove in mathlib.

theorem_file_pathstring

The file path of the target theorem in mathlib.

All 2 operations