Here is a more understandable description of the semi-satire that follows: 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 "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 "conjecture".
Mathematicians call the list of transformation rules used to reach a string a "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 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 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 Zermelo-Fraenkel set theory! Such independence proofs rely on modelling the proof system inside another proof system, and forcing is one of the main techniques used for this.
Not to be confused with algebra over a field, which is a particular algebraic structure studied within algebra.
Well summarized as "the branch of mathematics that deals with limits".
Techniques to get numerical approximations to numeric mathematical problems.
The entire field comes down to estimating the true values with a known error bound, and creating algorithms that make those error bounds asymptotically smaller.
Not the most beautiful field of pure mathematics, but fundamentally useful since we can't solve almost any useful equation without computers!
The solution visualizations can also provide valuable intuition however.
Important numerical analysis problems include solving:
As mentioned at Human Compatible by Stuart J. Russell (2019), game theory can be seen as the part of artificial intelligence that deas with scenarios where multiple intelligent agents are involved.