This blog post provides a review of the existing literature on agent-based systems for automated theorem proving, while presenting a general approach to the problem. Additionally, it serves as an informal specification outlining the requirements for a future system we intend to develop.
We want to write a series of blog posts about our efforts to use LLMs to formally verify code faster with the 
 Rocq/Coq theorem prover. Here, we present an experiment consisting of writing all that we are doing so that we can document our reasoning and help LLMs to pick up human techniques.
According to many publications about using generative AI to help formal verification, it is almost impossible to find a proof in "one shot". So, one certainly has to interact with the system, maybe by following the human way. Here we aim to document this "human way" of writing proofs.
