In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (known as well-formed formulas when relating to formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence, according to the rule of inference.
It differs from a natural language argument in that it is rigorous, unambiguous and mechanically verifiable.
The notion of theorem is generally effective, but there may be no method by which we can reliably find proof of a given sentence or determine that none exists.
For a well-formed formula to qualify as part of a proof, it must be the result of applying a rule of the deductive apparatus (of some formal system) to the previous well-formed formulas in the proof sequence.
It is synonymous with the set of strings over the alphabet of the formal language which constitute well formed formulas.