Formal proof systems
One context in which the word "formal" comes in, is that of formal proof systems.
A formal proof system is a way to write theorems and their proof in the computer, such that after it have been done the proof can be automatically verified by a computer.
In such systems, theorems are just sequences of characters (strings), and starting from your axiom strings, you use a few well defined rules to transform those strings mechanically, and obtain new true strings (thus making a proof).
The huge advantage of such systems is that since each proof step is so simple and mechanical, computers can verify proofs, which can be an extremely difficult and error prone task for humans to do!
There are also cases where the proof itself requires tedious verification of thousands of cases, and would be too time consuming for any human. One notable example of this is the four color theorem.
The downside of such systems is that they are much harder to write your proofs in, because in order to communicate with the computer you have to write everything in a very precise way.
I do believe however, that if such systems are done well enough with good tooling and standard libraries, writing a proof should be no harder than writing a computer program, and the benefits would largely outweight the greater difficulty of writing the proof.
For a concrete well presented example, a have a look at Metamath's awesome proof that 2 + 2 = 4 http://us.metamath.org/mpeuni/mmset.html#trivia
Metamath is an older proof system, and there are likely better choices today as I have mentioned at: What is the current state of formalized mathematics? but their web presentation is very nice!
Such proofs require of course defining everything in terms of things that the proof system understands. In the case of Metamath, Zermelo–Fraenkel-like set theory is used to my understanding.
A TL;DR version of the classic set theory approach would be:
- we can use sets, forall, exists and modus ponens
- the naturals can be defined in terms of sets like this: https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers
- the rationals can be defined easily as an ordered pair of integers. Ordered pairs can be defined in terms of sets easily with Kiratowski's definition, see also: Please Explain Kuratowski Definition of Ordered Pairs
- the reals can be defined in terms of sets with Dedekind cuts, see also: True Definition of the Real Numbers
- functions are just a set of pairs: Is $f(x) = (x + 1)/(x +2)$ a function?
- once we have reals and functions, note how the epsilon delta definition of limits only uses concepts that we have previously defined: functions, reals, forall and exists! Once you see this, it is easy to believe, that, at least, we can formalize real analysis with this simple system
The fact that mathematics can be fully formalized is surprising, and was arguably only fully realized at the end of the 19th century, in particular through the seminal Principia Mathematica, and materialized with the invention of computers.
This is in my opinion the property of mathematics that best defines it, and that which clearly separates its preciseness from other arts such as poetry.
Once we have maths formally modelled, one of the coolest results is Gödel's incompleteness theorems, which states that for any reasonable proof system, there are necessarily theorems that cannot be proven neither true nor false starting from any given set of axioms: those theorems are independent from those axioms. Therefore, there are three possible outcomes for any hypothesis: true, false or independent!
Some famous theorems have even been proven to be independent of some famous axioms. One of the most notable is that the Continuum Hypothesis is independent from ZFC! Such independence proofs rely on modelling the proof system inside another proof system, and forcing is one of the main techniques used for this.