---
title: "Run a tactic on a state (specified by its state ID), assuming the proof search has been initialized and some state is available. The response is either the next state and its state ID or an error message, in which ChatGPT should explain the error and consider decrementing the \"state_id\"."
method: POST
path: "/run_tactic"
---

# Run a tactic on a state (specified by its state ID), assuming the proof search has been initialized and some state is available. The response is either the next state and its state ID or an error message, in which ChatGPT should explain the error and consider decrementing the "state_id".

`POST /run_tactic`

## Request body

- RunTacticRequest
  - `state_id` integer — The ID of the state on which to run the tactic.
  - `tactic` string — The tactic to run on a state (specified by its state ID), assuming the proof search has been initialized.

## 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)