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 computers prefer binary, which is just 2 symbols: 0 and 1. 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

One time a person named Brown was looking at cells or dust or something under a microscope or floating in sunlight and noticed they were wobbly, which turned out to have a statistical pattern that Einstein later used to explain Brownian motion, part of his "miracle year" of publishing 4 papers all worthy of a Nobel. Mathematicians know a lot about Brownian motion. Kakutani proved that harmonic measure from complex function theory is the probability distribution of a random traveller, Brownian traveller if you will. The Laplacian being zero of an analytic function and the Cauchy-Riemann equations are founding members of the gang.

AI Summary

Brownian motion is a continuous-time random walk, and when a particle starts at a point $z = h$ in a domain $\Omega$ and stops upon hitting the boundary $\partial \Omega$, the probability distribution of its hitting location is known as the Harmonic Measure.

For instance, if a random walker starts at height $h$ in the right half-plane $\mathbb{H}$, the probability density of hitting the imaginary axis at position $y$ is exactly given by the Poisson kernel: $$P_h(y) = \frac{1}{\pi} \frac{h}{h^2 + y^2}$$

The beauty of Complex Analysis is that random walks are conformally invariant! By Riemann's Mapping Theorem, we can smoothly stretch domains like slits and disks into the half-plane, allowing us to compute these exact theoretical distributions for very complex shapes.

While the Harmonic Walker visualizer demonstrates these theorems informally and empirically, we are in the process of auto-formalizing these rigorous statistical inference results in Lean 4. You can see the formal stub in our codebase at mathgod_lean/MathgodLean/HarmonicMeasure.lean.

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!

0, 0, 1, 0, 2, 0, 2, 2, 1, 6, 0, 5, 0, 2, 6, ?
📖 See an Explanation

The core rule of the sequence is entirely about counting STEPS BACK to the last occurrence of the current number:

Visualizing Steps Back (Swoop Arrows)
1 back2 back2 back2 back1 back6 back0n=00n=11n=20n=32n=40n=52n=62n=71n=86n=9
  1. We start with $a_0 = 0$. Since we have never seen $0$ before (0 steps back), the next term is $a_1 = 0$.
  2. At index $1$, the current term is $0$. It appeared before at index $0$. The number of STEPS BACK is $1 - 0 = 1$, so $a_2 = 1 leftarrow 1 ext{ step back}$.
  3. At index $2$, the current term is $1$. Since this is the first time we see $1$ (0 steps back), the next term is $a_3 = 0$.
  4. At index $3$, the current term is $0$. Its last occurrence was at index $1$. The number of STEPS BACK is $3 - 1 = 2$, so $a_4 = 2 leftarrow 2 ext{ steps back}$.
  5. At index $4$, the current term is $2$. This is the first time we see $2$ (0 steps back), so $a_5 = 0$.
  6. At index $5$, the current term is $0$. Its last occurrence was at index $3$. The number of STEPS BACK is $5 - 3 = 2$, so $a_6 = 2 leftarrow 2 ext{ steps back}$.
  7. At index $6$, the current term is $2$. Its last occurrence was at index $4$. The number of STEPS BACK is $6 - 4 = 2$, so $a_7 = 2 leftarrow 2 ext{ steps back}$.
  8. At index $7$, the current term is $2$. Its last occurrence was at index $6$. The number of STEPS BACK is $7 - 6 = 1$, so $a_8 = 1 leftarrow 1 ext{ step back}$.
  9. At index $8$, the current term is $1$. Its last occurrence was at index $2$. The number of STEPS BACK is $8 - 2 = 6$, so $a_9 = 6 leftarrow 6 ext{ steps back}$.
💻 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