Formal system
Foundations and logic
A precisely specified language together with axioms and inference rules, in which proofs are finite objects that can be checked mechanically.
What is usually left out
Formalising a system is what makes questions about mathematics itself answerable mathematically. You cannot ask whether a statement is provable until "provable" names something definite, which is precisely what a formal system supplies and what Gödel’s results then exploit. The trade is that working mathematicians almost never write formal proofs; ordinary proofs are arguments in natural language, understood to be formalisable in principle rather than actually formalised. Proof assistants such as Lean close that gap deliberately, at considerable cost in effort.