Logic and arithmetic of proofs nowadays are partially automated. The We differentiate between different orders of logic. First-Order logic defined by Presburger Arithmetic can be automated, however the problem of computational complexity persists. However this Arithmetic has good properties like decidability and provability of every theorem described by Presburger arithmetic. Extensions of this arithmetic like the Peano arithmetic lead to problems as the result of Gödel with the incompleteness theorem. As an example we looked at a few examples of code implemented with the Coq IDE. As a next step we looked a definition of boolean formulas that would apply to formulations of a proof. Solving for the existence of theorem.