= Formalization of mathematics
= Foundation of mathematics
{synonym}
Mathematics is a <art>[beautiful game] played on https://en.wikipedia.org/wiki/String_(computer_science[strings], which <mathematicians> call https://en.wikipedia.org/wiki/Theorem["theorems"].
Here is a more understandable description of the semi-satire that follows: https://math.stackexchange.com/questions/53969/what-does-formal-mean/3297537\#3297537
You start with a very small list of:
* certain arbitrarily chosen initial strings, which mathematicians call "<axioms>"
* rules of how to obtain new strings from old strings, called https://en.wikipedia.org/wiki/Rule_of_inference["rules of inference"] Every transformation rule is very simple, and can be verified by a computer.
Using those rules, you choose a target string that you want to reach, and then try to reach it. Before the target string is reached, mathematicians call it a https://en.wikipedia.org/wiki/Conjecture["conjecture"].
Mathematicians call the list of transformation rules used to reach a string a https://en.wikipedia.org/wiki/Mathematical_proof["proof"].
Since every step of the proof is very simple and can be verified by a computer automatically, the entire proof can also be automatically verified by a computer very easily.
Finding proofs however is undoubtedly an <computable problem>[uncomputable problem].
Most mathematicians can't code or deal with the real world in general however, so they haven't created the obviously necessary: <website front-end for a mathematical formal proof system>.
The fact that Mathematics happens to be the best way to describe <physics> and that humans can use physical intuition heuristics to reach the NP-hard proofs of mathematics is one of the great miracles of the universe.
Once we have mathematics formally modelled, one of the coolest results is https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems[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 http://en.wikipedia.org/wiki/Continuum_hypothesis[Continuum Hypothesis] is <independent (mathematical logic)> from <Zermelo-Fraenkel set theory>! Such independence proofs rely on modelling the proof system inside another proof system, and https://en.wikipedia.org/wiki/Forcing_(mathematics)[forcing] is one of the main techniques used for this.
\Image[https://web.archive.org/web/20190430151331im_/http://abstrusegoose.com/strips/i_dont_give_a_shit_about_your_mountain.png]
{title=The landscape of modern Mathematics comic by Abstruse Goose}
{description=This comic shows that Mathematics is one of the most diversified areas of <art>[useless] human knowledge.}
{source=https://abstrusegoose.com/211}