MathGod - Learn

Peano

Math starts with counting. Ten-fingered humans have 10 symbols to write numbers: 0, 1, 2, 3, 4, 5, 6, 7, 8, 9. But fingerless transistor-based computers prefer binary, which is just 2 symbols: 0 and 1.

Bits vs. Qubits

Ergodicity in the Complex Plane

We both know how to go from one number to the next. In the 19-th century, Giuseppe Peano wrote down the rules of arithmetic based on successors. The successor of 0 is 1. The succesor of 1 is 2 (= 10 in binary). Et cetera. So to put humans and computers on the same page, Lean uses Peano's postulates to count, add, subtract, and multiply the natural numbers. Check out the natural number game from the Lean community.

Type Theory

In the early 20th century, math had a crisis. Bertrand Russell pointed out a logical contradiction in the basis of math: sets. A set is a collection of abstract objects, like numbers. We can use curly brackets for a set, like the natural numbers

$$\htmlData{tooltip=Some prefer to exclude 0 from the naturals but no biggie.}{\mathbb{N} = \{0, 1, 2, ...\},} $$

and the symbol $\in$ for elements of the set, like $$\htmlData{tooltip=50 is in the naturals but 3.14159... is not in.}{50 \in \mathbb{N}, \text{ but } \pi \notin \mathbb{N}.}$$ We want to define sets by properties, like $$\{ x \in \mathbb{N}, x > 50\},$$ the set of all natural numbers bigger than 50. Russell's paradox occurs when you let sets be elements of themselves. The set of all sets that do not contain themselves, $$X = \{ x \in \text{Sets}, x \notin x \}$$ creates a non-question: is $X \in X$? If true, then false, and vice versa, just like This sentence is false. cannot be true nor false. Religion encounters the same phenomenon in defining an all-powerful god, when you ask Can God create a rock too heavy for God to lift? If all-powerful, both creating and lifting should work, a contradiction.

The crisis in math was resolved by enhancing the concept of sets. One such enhancement is Type Theory. Types are just like sets, but there is a hierarchy that prevents Russell's paradox. $\mathbb{N}$ is a Type in Lean. And regular Types of Type(0) are elements of a higher type, Type(1). The type level in parentheses is called a universe, which organizes mathematical objects to maintain logical consistency. Other systems to avoid Russell's paradox are used in other formalization languages. Coq gets it name from calculus of constructions, and HOL from higher-order logic.

Lean uses Type Theory, which may be preferred by computer scientists who have a similar notion in data types, like Bool and Int. Computers crash when programs encounter contradictions, so formal verification, a way of checking programs by strict type-checking, is akin to formal mathematics. Basically computer scientists and mathematicians have the same problem with the same solution: the results are not perfectly trustworthy unless formalized.

De Bruijn factor

Formalization is slow. Human language has developed for thousands if not millions of years, and human mathematicians have an arsenal of shortcuts still to teach the computers. The ratio of formal language to informal language in programming math is known as the de Bruijn factor. Professional mathematicians operate on the premise that they could explain everything formally, with painstaking detail, but there is a trade-off between progress and perfection. The de Bruijn factor tends to be between 1 and 10,000. In the Liquid Tensor Experiment, mathematician Peter Scholze stated a result in roughly 5 lines of human language that took 80,000 lines of code to formalize. The Lean language uses tactics to prune the gap, putting meticulous code into single words that help computers catch up to human shortcuts. The #print theorem command unravels tactics into fully formal computer language in case checking is desired. Artificial intelligence may discover a mathematical proof which is too long for humans to check, even in human language, so the trade-off betweeen trust and testing will always persist.

The mathematical proofs that AI finds will only be valuable if they are understandable to humans, which can happen to various degrees. A classic calculator can display about 10 digits of approximation to $\pi$, which would take a human infant quite a long time to learn individually and be a waste of time to do by hand. Trust is collective, and the people who make calculators can be trusted to implement circuits that do as advertised, including negative consequences for competitors who get it wrong. One common practical value of higher math is cryptographic, allowing you to buy things online. Perfect code cannot be hacked, but hackability is an imperfect test contingent on the skill and resources of the hacker. At Mathgod we endeavor to reduce the gap between computer and human understanding, championing transparency and explainability. We propose a scale that rates the gap. $\pi$ is a number known to humans for centuries if not millenia, so calculators that spit out digits of $\pi$ are a 1 out of 10 on our scale. Fermat's Last Theorem, actively being formalized, was proved without computers, so once formalized it also is 1 out of 10. If some result in fact turns out impossible to formalize, perhaps requiring a new language or philosophical choice, we rank it 0 out of 10 on the Mathgod scale (not intended as an insult). Some modern results, such as the Four Color Theorem, were, like estimating many digits of pi, too tedious to achieve by hand, but their acceptance is not as universal as digits of $\pi$ because the algorithms are more complicated and not understood by as many people. We rate those 2 out of 10. We intend the scale to have plenty of room at the top and be human-centric, but have scientific basis. Using the de Bruijn factor, recency of proof, and breadth of acceptance and practical value, we propose to rate computer proofs of mathematical results, as much a social exercise as a numerical one, inviting debate.

Harmonic Measure & Random Walks

VanEck Sequence

The VanEck Sequence (also known as the Van Eck sequence) is a fascinating, self-referencing integer sequence first proposed by Jan Ritsema van Eck in 2010. It is defined as follows:

Start with $a_0 = 0$. For any term $a_n$, to determine the next term $a_{n+1}$:

If $a_n$ has never appeared in the sequence before, then $a_{n+1} = 0$.
If $a_n$ has appeared before, then $a_{n+1}$ is the number of steps back to its most recent previous appearance.

For a deep dive into its behavior and mystery, check out the famous Numberphile Video on the VanEck Sequence featuring Neil Sloane.

🎮 Guess the Next Term!

Sequence Length: 20 terms

 0,  0,  1,  0,  2,  0,  2,  2,  1,  6,  0,  5,  0,  2,  6,  5,  4,  0,  5,  3, ?

📖 See an Explanation

💻 Show Lean 4 Code (Credit: Justin Kong)

import Mathlib.Data.Nat.Basic
import Mathlib.Data.List.Basic

def vanEckStep (l : List ℕ) : List ℕ :=
  match l with
  | [] => [0]
  | hd :: tl =>
    let idx := tl.findIdx (· == hd)
    if idx < tl.length then
      (idx + 1) :: hd :: tl
    else
      0 :: hd :: tl

def vanEckList : ℕ → List ℕ
  | 0 => [0]
  | n + 1 => vanEckStep (vanEckList n)

def vanEckNthTerm (n : ℕ) : ℕ :=
  match vanEckList n with
  | [] => 0
  | hd :: _ => hd

Single Deletion Correcting Codes (VT)

Abstract Algebra: Groups, Rings, & Varieties

Abstract algebra is the study of algebraic structures such as groups, rings, and fields. Rather than studying specific numbers, we study the underlying symmetries and rules that govern operations.

🟢 Groups (One Operation)

A Group gives you a set and a single operation (like addition or composition) that is reversible, has an identity, and is associative. It's the mathematical language of symmetry.

Example 1: The Cyclic Group $n=3$ ($\mathbb{Z}_3$)

Imagine a clock with only 3 hours: 0, 1, and 2. If you are at 2 and add 1, you wrap around back to 0. This is modular addition! It forms a simple Abelian (commutative) group.

Show Group Table for $\mathbb{Z}_3$

Example 2: Symmetries of a Square ($D_4$)

Take a physical square. You can rotate it by 90°, 180°, 270°, or flip it along its axes. There are exactly 8 such rigid motions. If you do one motion, then another, the result is always equivalent to a single motion. This forms a non-commutative group, because rotating then flipping is not the same as flipping then rotating!

Show Group Table for $D_4$

$\circ$	$R_0$	$R_{90}$	$R_{180}$	$R_{270}$	$H$	$V$	$D_1$	$D_2$
$R_0$	$R_0$	$R_{90}$	$R_{180}$	$R_{270}$	$H$	$V$	$D_1$	$D_2$
$R_{90}$	$R_{90}$	$R_{180}$	$R_{270}$	$R_0$	$D_1$	$D_2$	$V$	$H$
$R_{180}$	$R_{180}$	$R_{270}$	$R_0$	$R_{90}$	$V$	$H$	$D_2$	$D_1$
$R_{270}$	$R_{270}$	$R_0$	$R_{90}$	$R_{180}$	$D_2$	$D_1$	$H$	$V$
$H$	$H$	$D_2$	$V$	$D_1$	$R_0$	$R_{180}$	$R_{270}$	$R_{90}$
$V$	$V$	$D_1$	$H$	$D_2$	$R_{180}$	$R_0$	$R_{90}$	$R_{270}$
$D_1$	$D_1$	$H$	$D_2$	$V$	$R_{90}$	$R_{270}$	$R_0$	$R_{180}$
$D_2$	$D_2$	$V$	$D_1$	$H$	$R_{270}$	$R_{90}$	$R_{180}$	$R_0$

Read as: Row element applied first, then Column element.
$R_d$: Rotation by $d$ degrees clockwise. $H$: Horizontal flip. $V$: Vertical flip. $D_1$ / $D_2$: Diagonal flips.
F = Front (Unflipped), B = Back (Flipped). Corners: Yellow (0), Red (1), Green (2), Blue (3).
Note: $R_{90}$ and $H$ are generators of the group. Every other element can be built just by combining those two!

Example 3: The Monster Group

The "Monster" is the largest of the sporadic simple groups, containing $808,017,424,794,512,875,886,459,904,961,710,757,005,754,368,000,000,000$ elements! It acts as a symmetry group on a 196,883-dimensional space and is intimately tied to string theory and modular functions (Monstrous Moonshine).

🔵 Rings (Two Operations)

A Ring is an Abelian group (under addition) that comes with a second operation (multiplication) that distributes over the first. Unlike group elements, ring elements don't always have multiplicative inverses (you can't always divide).

Example 1: Integers Modulo 3 ($\mathbb{Z}_3$)

Just like our group example, but now we can multiply! The addition table is exactly the same, but the multiplication table adds a new layer.

Show Ring Tables & Distributive Rule

$+$	0	1	2
0	0	1	2
1	1	2	0
2	2	0	1

$\times$	1	2
0	0	0
1	1	2
2	2	1

The Distributive Rule in Action

Let's verify that multiplication distributes over addition: $a \times (b + c) = (a \times b) + (a \times c)$. Let $a=2$, $b=1$, $c=2$.

Left Side: $2 \times (1 + 2) = 2 \times 0 = \mathbf{0}$ 
Right Side: $(2 \times 1) + (2 \times 2) = 2 + 1 = \mathbf{0}$ 
 They match perfectly! 

Example 2: The Integers ($\mathbb{Z}$)

The classic ring. You can add, subtract, and multiply integers, and the result is always an integer. But you can't divide 3 by 2 and stay in the integers, which is why $\mathbb{Z}$ is a ring, but not a field.

Example 3: Polynomial Rings

Let's look at the polynomial ring $\mathbb{R}[x]$. The elements are polynomials. We have both additive and multiplicative parts.

Addition:
 $(x^3 - 2x + 1) + (x^2 + 7) = x^3 + x^2 - 2x + 8$

Multiplication:
 $(x^3 - 2x + 1) \times (x^2 + 7)$
 $= x^3(x^2 + 7) - 2x(x^2 + 7) + 1(x^2 + 7)$
 $= x^5 + 7x^3 - 2x^3 - 14x + x^2 + 7$
 $= x^5 + 5x^3 + x^2 - 14x + 7$ 

🟣 Ideals and Algebraic Varieties

Just as a group has normal subgroups, a ring has ideals. An ideal is a subset that absorbs multiplication (multiplying anything in the ideal by any polynomial keeps it trapped inside the ideal).

The Textbook Definition of a Variety

An affine algebraic variety defined by a set of polynomials $S$ is the set of all geometric points where every polynomial in $S$ evaluates exactly to zero.

The Inclusion-Reversing Dictionary

Hilbert's Nullstellensatz proves there is a dictionary mapping Ideals directly to Geometric Varieties. If a geometric shape gets larger (e.g., a 0D point expands to a 1D line), its corresponding Algebraic Ideal gets smaller! When you manipulate the algebra, you are directly manipulating the geometry.

Learn

1. The Irrational Rotation (Dense Orbits)

2. The Doubling Map (Sensitive Dependence)