# proof assistants

## 1. basic idea

- You have a proof goal and a set of assumptions. You need to move your proof state to the proof goal. You do this interactively using
*tactics*.

- You have a proof goal and a set of assumptions. You need to move your proof state to the proof goal. You do this interactively using
*tactics*.

Created: 2024-07-15 Mon 01:28