Formalization of mathematics

Much of this section will be dumped at Section "Website front-end for a mathematical formal proof system" instead.

QED manifesto

If Ciro Santilli ever becomes rich, he's going to solve this with: website front-end for a mathematical formal proof system, promise.

Web-based proof assistant

A more verbose description of this at: Section "Website front-end for a mathematical formal proof system".

The Math Genome Project (2023-)

Ciro Santilli asked: discord.com/channels/1096393420408360989/1096393420408360996/1137047842159079474

www.themathgenome.com/

Appears to support multiple proof assistant backends including Lean, Hol and Coq.

A discussion on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20Math.20Genome.20Project/near/352639129. Lean people are not convinced about the model in general it seems however.

TODO closed source? Really? www.themathgenome.com/pricing

TODO not viewable without login?

Has conjectures feature.

Built by this dude John Mercer: www.linkedin.com/in/johnmercer/. He must be independently wealthy or something? What a hero.

A failed Hacker News self post: news.ycombinator.com/item?id=35775071

Does the website actually automatically check the formal proofs, or is this intended to be implemented at some point? And if yes, is it intended to allow proofs to depend on other proofs of the website (possibly by other people)

Owner:

Hi Ciro, yes we will be releasing in-browser proof assistant environments/checkers (e.g. Lean). Our goal is not to replace the underlying open-source repos (e.g. Mathlib) so the main dependency will be on the current repos; then when statement formalizations and proofs come in and are certified they can be PR'd to the respective repos. So we will be the source of truth for the informal latex code but only a stepping stone and orchestration layer on the way to the respective formal libraries.

So apparently there will be proof checking, but nodependencies between proofs, you still have to pull request everywhing back and face the pain.

List of proof assistants

Lean (proof assistant)

Coq (software)

Formal proof

A proof in some system for the formalization of mathematics.

Formal proof is useless

The only cases where formal proof of theorems seem to have had actual mathematical value is for theorems that require checking a very large number of case, so much so that no human can be fully certain that no mistakes were made. Some examples:

Mathematical proof

Formal system

Zermelo-Fraenkel set theory (ZF)

One of the first formal proof systems. This is actually understandable!

This is Ciro Santilli-2020 definition of the foundation of mathematics (and the only one he had any patience to study at all).

TODO what are its limitations? Why were other systems created?

Zermelo-Fraenkel axioms (ZF)

Zermelo-Fraenkel axioms with the axiom of choice (ZFC)

Set theory

When Ciro Santilli says set theory, he basically means. Zermelo-Fraenkel set theory.

Metamath

metamath.org/

It seems to implement Zermelo-Fraenkel set theory.

Axiom

Consistency

A set of axioms is consistent if they don't lead to any contradictions.

When a set of axioms is not consistent, false can be proven, and then everything is true, making the set of axioms useless.

Independence (mathematical logic)

A theorem is said to be independent from a set of axioms if it cannot be proven neither true nor false from those axioms.

It or its negation could therefore be arbitrarily added to the set of axioms.

Open problem in mathematics

Conjecture

A conjecture is an open problem in mathematics for which some famous dude gave heuristic arguments which indicate if the theorem is true or false.

Famous conjecture

This section groups conjectures that are famous, solved or unsolved.

They are usually conjectures that have a strong intuitive reasoning, but took a very long time to prove, despite great efforts.

The list: en.wikipedia.org/wiki/List_of_unsolved_problems_in_mathematics

Collatz conjecture (1937-)

Given stuff like arxiv.org/pdf/2107.12475.pdf on Erdős' conjecture on powers of 2, it feels like this one will be somewhere close to computer science/Halting problem issues than number theory. Who knows. This is suggested e.g. at The Busy Beaver Competition: a historical survey by Pascal Michel.

Collatz-like problem

We ust use the if mod notation definition as mentioned at: math.stackexchange.com/questions/4305972/what-exactly-is-a-collatz-like-problem/4773230#4773230

The Busy Beaver Competition: a historical survey by Pascal Michel (2013)

arxiv.org/abs/0906.3749

Erdős' conjecture on powers of 2

Described at: arxiv.org/pdf/2107.12475.pdf where a relation to the Busy beaver scale is proven, and the intuitive relation to the Collatz conjecture described. Perhaps more directly: demonstrations.wolfram.com/CollatzSequenceComputedByATuringMachine/

Theorem

Corollary

An easy to prove theorem that follows from a harder to prove theorem.

Lemma (mathematics)

A theorem that is not very important on its own, often an intermediate step to proving something that the author feels deserves the name "theorem".

Set (mathematics)

Intuitively: unordered container where all the values are unique, just like C++ std::set.

More precisely for set theory formalization of mathematics:

everything is a set, including the elements of sets
string manipulation wise:
- {} is an empty set. The natural number 0 is defined as {} as well.
- {{}} is a set that contains an empty set
- {{}, {{}}} is a set that contains two sets: {} and {{}}
- {{}, {}} is not well formed, because it contains {} twice

Union (set theory, $A ⋃ B$ )

Cardinality

The size of a set.

For finite sizes, the definition is simple, and the intuitive name "size" matches well.

But for infinity, things are messier, e.g. the size of the real numbers is strictly larger than the size of the integers as shown by Cantor's diagonal argument, which is kind of what justifies a fancier word "cardinality" to distinguish it from the more normal word "size".

The key idea is to compare set sizes with bijections.

Function (mathematics)

Set of ordered pairs. That's it! This is illustrated at: math.stackexchange.com/questions/1480651/is-fx-x-1-x-2-a-function/1481099#1481099

Domain, codomain and image

Bijection

Injective function

Mnemonic: in means into. So we are going into a codomain that is large enough so that we can have a different image for every input.

Surjective function

Mnemonic: sur means over. So we are going over the codomain, and covering it entirely.

Domain of a function

Codomain

Vs: image: the codomain is the set that the function might reach.

The image is the exact set that it actually reaches.

E.g. the function:

f (x) = x^{2}

could have:

codomain $R$
image $R_{+}$

Note that the definition of the codomain is somewhat arbitrary, e.g.

x^{2}

could as well technically have codomain:

R ⋃ R^{2}

(2)

even though it will obviously never reach any value in

R^{2}

The exact image is in general therefore harder to characterize.

Endofunction

A function where the domain is the same as the codomain.

Image (mathematics)

Periodic function

Square wave

Rectangular wave

Function by signature

In this section we classify some functions by the type of inputs and outputs they take and produce.

Functional function

This is about functions that take functions as input or output.

Convolution

Set function

This section is about functions that operates on arbitrary sets.

Cartesian product

A function that maps two sets to a third set.

Direct product

A Cartesian product that carries over some extra structure of the input groups.

E.g. the direct product of groups carries over group structure on both sides.

Numeric function

This section is about functions that operate on numbers such as the integers or real numbers.

Addition

Subtraction

Multiplication

Division

Exponentiation ( $x^{y}$ )

nth root

Square root

Exponentiation functional equation

We define this as the functional equation:

f (x, y) = f (x) f (y)

It is a bit like cauchy's functional equation but with multiplication instead of addition.

Exponential function ( $e^{x}$ )

Exponential function differential equation

The differential equation that is solved by the exponential function:

y^{'} (x) = y (x)

with initial condition:

y (0) = 1

(2)

TODO find better name for it, "linear homogenous differential equation of degree one" almost fully constrainst it except for the exponent constant and initial value.

Definition of the exponential function

Taylor expansion definition of the exponential function

The Taylor series expansion is the most direct definition of the expontial as it obviously satisfies the exponential function differential equation:

the first constant term dies
each other term gets converted to the one before
because we have infinite many terms, we get what we started with!

e^{x} = \sum_{n = 0}^{\infty} \frac{x ^{n}}{n !} = 1 + \frac{x}{1} + \frac{x ^{2}}{2} + \frac{x ^{3}}{2 \times 3} + \frac{x ^{4}}{2 \times 3 \times 4} + \dots

Product definition of the exponential function

e^{x} = lim_{n \to \infty} (1 + \frac{x}{n})^{n}

The basic intuition for this is to start from the origin and make small changes to the function based on its known derivative at the origin.

More precisely, we know that for any base b, exponentiation satisfies:

$b^{x + y} = b^{x} b^{y}$ .
$b^{0} = 1$ .

And we also know that for

b = e

in particular that we satisfy the exponential function differential equation and so:

\frac{d e ^{x}}{d x} (0) = 1

(2)

One interesting fact is that the only thing we use from the exponential function differential equation is the value around

x = 0

, which is quite little information! This idea is basically what is behind the importance of the ralationship between Lie group-Lie algebra correspondence via the exponential map. In the more general settings of groups and manifolds, restricting ourselves to be near the origin is a huge advantage.

Now suppose that we want to calculate

e^{1}

. The idea is to start from

e^{0}

and then then to use the first order of the Taylor series to extend the known value of

e^{0}

e^{1}

E.g., if we split into 2 parts, we know that:

e^{1} = e^{1 / 2} e^{1 / 2}

(3)

or in three parts:

e^{1} = e^{1 / 3} e^{1 / 3} e^{1 / 3}

(4)

so we can just use arbitrarily many parts

e^{1 / n}

that are arbitrarily close to

x = 0

e^{1} = (e^{1 / n})^{n}

(5)

and more generally for any

x

we have:

e^{x} = (e^{x / n})^{n}

(6)

Let's see what happens with the Taylor series. We have near

y = 0

in little-o notation:

e^{y} = 1 + y + o (y)

(7)

Therefore, for

y = x / n

, which is near

y = 0

for any fixed

x

e^{x / n} = 1 + x / n + o (1 / n)

(8)

and therefore:

e^{x} = (e^{x / n})^{n} = (1 + x / n + o (1 / n))^{n}

(9)

which is basically the formula tha we wanted. We just have to convince ourselves that at

lim_{n \to \infty}

, the

o (1 / n)

disappears, i.e.:

(1 + x / n + o (1 / n))^{n} = (1 + x / n)^{n}

(10)

To do that, let's multiply

e^{y}

by itself once:

e^{y} e^{y} = (1 + y + o (y)) (1 + y + o (y)) = 1 + 2 y + o (y)

(11)

and multiplying a third time:

e^{y} e^{y} e^{y} = (1 + 2 y + o (y)) (1 + y + o (y)) = 1 + 3 y + o (y)

(12)

TODO conclude.

Gaussian function ( $e - x^{2}$ )

Logarithm

Matrix exponential

Is the solution to a system of linear ordinary differential equations, the exponential function is just a 1-dimensional subcase.

Note that more generally, the matrix exponential can be defined on any ring.

The matrix exponential is of particular interest in the study of Lie groups, because in the case of the Lie algebra of a matrix Lie group, it provides the correct exponential map.

Video 1.

How (and why) to raise e to the power of a matrix by 3Blue1Brown (2021)

Source.

Logarithm of a matrix

Existence of the matrix logarithm

en.wikipedia.org/wiki/Logarithm_of_a_matrix#Existence mentions it always exists for all invertible complex matrices. But the real condition is more complicated. Notable counter example: -1 cannot be reached by any real

e^{t k}

The Lie algebra exponential covering problem can be seen as a generalized version of this problem, because

Lie algebra of $G L (n)$ is just the entire $M_{n}$
we can immediately exclude non-invertible matrices from being the result of the exponential, because $e^{t M}$ has inverse $e^{- t M}$ , so we already know that non-invertible matrices are not reachable

Polynomial

Degree of a polynomial

Algebraic equation (Polynomial equation)

Named algebraic equation

Quadratic equation

Quadratic equation modulo n (Quadratic equation over a cyclic group)

math.stackexchange.com/questions/229218/modulo-version-of-the-quadratic-formula-and-eulers-criterion

Quadratic formula

Cubic equation

Quartic equation

Quintic equation

Abel-Ruffini theorem

Algebraic equation over a field

In this section we collect results about algebraic equations over more "exotic" fields

Algebraic equation modulo n

Algebraic number (Root of a polynomial)

Algebraic number field ( $\overline{Q}$ )

The set of all algebraic numbers forms a field.

This field contains all of the rational numbers, but it is a quadratically closed field.

Like the rationals, this field also has the same cardinality as the natural numbers, because we can specify and enumerate each of its members by a fixed number of integers from the polynomial equation that defines them. So it is a bit like the rationals, but we use potentially arbitrary numbers of integers to specify each number (polynomial coefficients + index of which root we are talking about) instead of just always two as for the rationals.

Each algebraic number also has a degree associated to it, i.e. the degree of the polynomial used to define it.

$e + π$

Video 1.

Why π^π^π^π could be an integer by Stand-up Maths (2021)

Source. Sponsored by Jane Street. Shame.

Diophantine equation

Polynomial (possibly a multivariate polynomial) with integer coefficients.

Sometimes systems of Diophantine equations are considered.

Problems generally involve finding integer solutions to the equations, notably determining if any solution exists, and if infinitely solutions exist.

The general problem is known to be undecidable: Hilbert's tenth problem.

The Pythagorean triples, and its generalization Fermat's last theorem, are the quintessential examples.

Beauty Is Suffering

. Source.

Hilbert's tenth problem (1970, Determine if one Diophantine equation has a solution)