Introduction
Idea
How hard are questions about mathematics? Some have remained open for millennia, some are considered too hard for all known techniques, and some have only been answered with the help of computers. Nonetheless, some questions are harder than others; in particular, sometimes progress on one question can contribute answers to other questions.
How do computers help with mathematical questions? Mathematics can be formalized: reduced to manipulation of abstract symbols, like letters on a page or beads on an abacus. Answers to questions can be formalized as proofs, which are sequences of manipulations that follow some predetermined rules. A computer can be programmed to perform a search for a proof. (Indeed, in a certain sense, all programs are searches for proofs.) However, if there is no proof, then the program will run forever, and whether a program will halt is itself uncomputable (WP, nLab).
What use is a program that might run forever? On its own, not much. However, this living book presents a collection of several different programs, collated by formalism and mathematical question, which all search for proofs in one way or another. We may then roughly gauge the difficulty of questions by comparing the sizes of different programs which each search for proofs answering the same question.
As a quick aside: the search for bounds on halting programs is known as the busy beaver game, and so this book is naturally known as the Busy Beaver Gauge.
Presentation
The bulk of this book dedicates a page per computational formalism. At the top of each page, various results are graphed for visual comparison on a one- or two-dimensional plot. Three regions are distinguished on each plot:
- Known Values: regions where every program has been enumerated and the Busy Beaver values have been calculated
- Turing regime (universality): regions where some programs exhibit Turing-completeness (WP) and universal behaviors
- Futamura regime (specializing): regions where some programs implement Futamura projections (WP) and other partial evaluators
Nuts & Bolts
To make this whole concept useful, we choose machines and languages which are Turing-complete and seem relatively simple to describe (in the sense of Kolmogorov complexity) but are otherwise not particularly good for expressing any facet of mathematics, in order to be unbiased. We also must find reasonable ways of measuring the size of programs such that smaller programs are simpler than larger programs.
We also need a good list of unsolved problems in mathematics. These problems need to be questions; specifically, we need to be able to search for a definite answer to the question using only one infinite loop or infinite recursion.
Finally, we wish to thank the many folks who authored the programs that we study here. Credits are given per-program in the following pages, in tables of values at the bottom of each page. Where possible, we also link to English Wikipedia (WP), the esoteric languages wiki (esolangs), and the nLab.
Problems
In order to calibrate any busy beaver gauge, we must first define a common set of problems. A problem must be:
- Semidecidable: either proof search or disproof search must terminate once the first theorem or counterexample is found
- Arithmetic: it is either true or false of the natural numbers
- Encodable: we know how to express it as a low-level bookkeeping computation
- Meaningful: an affirmative or negative answer to the problem would advance the art of mathematics
Solved problems
Some problems are no longer open, but they are still useful as gauges since they can give bounds for busy beavers.
Pólya's problem
Let n be some upper bound. Do more than half of the natural numbers less than n have an odd number of prime factors? Pólya noticed in 1919 that, if true, this statement would imply the Riemann hypothesis. Haselgrove showed in 1958 that the statement is false, and Tanaka found that it is first false for n = 906,150,257 in Tanaka 1980.
See also WP.
Natural Numbers
We will always have open questions about the natural numbers.
Catalan–Mersenne conjecture
Are there a finite number of Catalan–Mersenne primes; does OEIS A7013 contain any composite numbers? Catalan conjectured this in 1876 while editing a letter from Lucas.
See also WP.
Collatz conjecture
Does the graph of the Collatz function have multiple strongly-connected components? Equivalently, does every natural number map to one under some number of iterations of the Collatz function? Collatz may have first introduced the function in 1937.
See also WP.
Erdős–Lagarias conjecture
Let k > 8. Can any k'th power of two be written as a sum of distinct powers of three; is any k'th power of two expressible in ternary with only the digits 0 and 1? Erdős conjectured that there is no such k and Lagarias studied the problem in Lagarias 2005.
Fermat prime conjecture
Is there a sixth Fermat prime? Fermat conjectured that all Fermat numbers are prime, but Euler showed that the sixth Fermat number F₅ is composite in 1732.
See also WP.
Goldbach conjecture
Aside from two, is every even number a sum of two prime numbers? Goldbach claimed this in a 1742 letter to Euler.
See also WP.
Weak Goldbach conjecture
Aside from one, three, and five; is every odd number a sum of three prime numbers? This statement is a strict weakening of the Goldbach conjecture. A proof was proposed in Helfgott 2013 but has not yet been accepted by the community.
Legendre conjecture
For all positive n, is there a prime number between n² and (n + 1)²? Legendre investigated this question.
See also WP.
Odd perfect number
Are any perfect numbers odd? The earliest examination of this question is unknown but may have been by Euclid or Nicomachus of Gerasa.
See also WP.
Period 32 Laver table
Is there a Laver table with period 32; does 32 appear in OEIS A98820? Laver showed in Laver 1995 that a Laver table exists for any power-of-two period, given ZFC plus the axiom that an I3 rank-into-rank cardinal exists.
See also WP. A collection of attempts at encoding this problem can be found at Code Golf Stack Exchange.
Riemann hypothesis
Do all non-trivial zeros of Riemann's zeta function have real part 1/2? Riemann guessed that all non-trivial zeros are real in 1859, and it is known that all non-trivial zeros have real parts in [0,1].
Equivalently, as given by Robin in 1984 and explained by Lagarias 2001, let H(n) denote the n'th harmonic number; is the sum of divisors of n always smaller than H(n) + exp(H(n)) × ln(H(n))?
Consistency
For any formal system with a notion of negation, antimony, or contradiction; we may ask whether it is consistent: whether the system fails to prove any pair of mutually-exclusive statements. When phrased in terms of semidecidability, consistency problems are often a form of proof search, since it can be shown that searching for one specific sort of contradiction can be sufficient to find all contradictions.
Theories which have been investigated include:
Notes
Style
- We denote open conjectures and hypotheses with non-possessive labels. This is both to recognize a lack of primacy, as anybody can speculate on interesting matters, and a lack of proof, as we normally celebrate the effort required to prove a statement above the effort required merely to state it.
- Some conjectures are attached to those who studied or documented them, rather than the original conjecturer, as in the case of Firoozbakht's second conjecture. Look, they have to come from somewhere. We can only hope that Firoozbakht is not upset.
- It is tempting to over-generalize and define e.g. perfect numbers in terms of sum-of-divisors functions which are then introduced at the top of the page. However, this obscures the history of the problems, as in the case of odd perfect numbers.
Turing Machines
This article covers the uncomputable function BB. BB(n,k) is the maximum number of steps taken by any n-state k-symbol halting Turing machine. As a historically-important special case, BB(n,2) is OEIS A60843, also known as S(n).
Some machines require a non-zero initial tape, which can be accounted for by appending the length of the initial tape to the symbol count: we treat them as shorthand for machines which use one state per symbol to write the initial tape before jumping to their main algorithm.
Summary
The following diagram summarizes known values and problems relative to BB. It is hard to read due to relatively high dimensionality; the solid violet barrier from the top to the left gives known values of BB, the blue wall is given by Rogozhin's machines, and the other known implementations are a smattered constellation of dots.
Known Values
BB(1,k) is defined as 1 for all k.
BB(n,k) | 2 symbols | 3 | 4 |
---|---|---|---|
2 states | 6 | 38 | 3,932,964 |
3 | 21 | ||
4 | 107 | ||
5 | 47,176,870 |
This table is tight in the sense that all unknown cells are bounded by the hardest open problems in mathematics, known as cryptids.
Tables of Values
Goldbach conjecture
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
Code Golf Addict 2016 | (27, 2) | (27, 2) |
Showalter 2016 | (47, 2) | (47, 2) |
LittlePeng9 2013 | ('goldbach.tm', 0) | (54, 4) |
O'Rear 2016 | goldbach.nql | (432, 2) |
Period 32 Laver table
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
Taylor 2016 | (64, 2) | (64, 2) |
Erdős–Lagarias conjecture
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
Stérin & Woods 2021 | (5, 4) | (5, 4) |
Stérin & Woods 2021 | (15, 2) | (15, 2) |
Interp(Tag(2))
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
Rogozhin 1996 | (2, 18) | (2, 18) |
Rogozhin 1996 | (3, 10) | (3, 10) |
Rogozhin 1996 | (4, 6) | (4, 6) |
Rogozhin 1996 | (5, 5) | (5, 5) |
Rogozhin 1996 | (7, 4) | (7, 4) |
Rogozhin 1996 | (10, 3) | (10, 3) |
Rogozhin 1996 | (24, 2) | (24, 2) |
Catalan–Mersenne conjecture
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
LittlePeng9 2013 | ('catalan-mersenne.tm', 2) | (29, 4) |
LittlePeng9 2013 | ('catalan-mersenne.tm', 2) | (29, 4) |
Fermat prime conjecture
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
LittlePeng9 2013 | ('fermat-prime.tm', 9) | (40, 4) |
Weak Goldbach conjecture
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
LittlePeng9 2013 | ('goldbach-ternary.tm', 0) | (79, 13) |
Legendre conjecture
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
LittlePeng9 2013 | ('legendre.tm', 9) | (39, 4) |
Odd perfect number
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
LittlePeng9 2013 | ('odd-perfect.tm', 0) | (79, 13) |
Pólya's problem
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
LittlePeng9 2013 | ('polya.tm', 0) | (37, 6) |
Riemann hypothesis
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
Aaronson & Matiyasevich 2016 | riemann-matiyasevich-aaronson.nql | (734, 2) |
O'Rear 2016 | riemann.nql | (916, 2) |
Con(ZF)
Source | Program Name/Parameters | BB(n,k) |
---|---|---|
O'Rear 2016 | zf2.nql | (748, 2) |
O'Rear 2016 | zf.nql | (1887, 2) |
Binary Lambda Calculus
This article covers the uncomputable function OEIS A333479, known as BBλ. BBλ(n) is the size of the largest normal form of any normalizing closed lambda term of size n, where the size of a term is its length when encoded in BLC.
Summary
The following diagram summarizes known values and problems relative to BBλ.
Tables of Values
Interp(BF)
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Felgenhauer & Tromp 2011 | ait/bf.lam | 829 |
Goldbach conjecture
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Felgenhauer 2013 | fast_growing_and_conjectures/goldbach.lam | 267 |
Goodstein's theorem
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Felgenhauer 2014 | fast_growing_and_conjectures/goodstein.lam | 351 |
Period 32 Laver table
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Felgenhauer & Tromp 2016 | fast_growing_and_conjectures/laver.lam | 213 |
Felgenhauer & Tromp 2016 | codegolf/laver.lam | 215 |
Odd perfect number
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Tromp 2020 | fast_growing_and_conjectures/oddperfect.lam | 247 |
Felgenhauer 2020 | fast_growing_and_conjectures/perfect.lam | 288 |
Interp(BLC)
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Felgenhauer & Tromp 2011 | ait/uni.lam | 232 |
Tromp 2024 | ait/uniK.lam | 975 |
Interp(BLC2)
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Tromp 2024 | ait/uni2.lam | 334 |
Interp(BLC2[8])
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Tromp 2024 | ait/uni28.lam | 500 |
Interp(BLC[8])
Source | Program Name/Parameters | BBλ(n) |
---|---|---|
Felgenhauer & Tromp 2011 | ait/uni8.lam | 355 |
Brainfuck
This article covers the Busy Brain Beaver function BBB(n) counting the maximum number of steps taken by non-interactive right-unbounded Brainfuck programs of length n.
Definition
A non-interactive Brainfuck program has six instructions: move the head left and right, increment and decrement the highlighted cell, and start and end loops. A right-unbounded Brainfuck program only moves to the right of the starting cell, but has access to an unbounded number of cells. Every single instruction takes a single step, including loop tests.
Summary
The following diagram summarizes known values and problems relative to BBB.
Known Values
Lower bounds for small n are established here on a variant of Brainfuck with unbounded cell values, and are identical up to 255.
We include lower bounds for selected n from this golfing challenge.
n | BBB(n) |
---|---|
1 | 1 |
2 | 2 |
3 | 3 |
4 | 4 |
5 | ≥ 7 |
39 | ≥ 31,919,535,558 |
41 | ≥ 10 ↑ (10 ↑ 28) |
63 | ≥ 255 ↑↑ 2 |
Tables of Values
Interp(BF,[!])
Source | Program Name/Parameters | BBB(n) |
---|---|---|
Cristofani 2002 | dbfi.b | 423 |
Faase 2002 | interp-faase.b | 6376 |
Interp(BF²)
Source | Program Name/Parameters | BBB(n) |
---|---|---|
NYYRIKKI 2002 | bit-doubler.b | 1408 |
Erdős–Lagarias conjecture
Source | Program Name/Parameters | BBB(n) |
---|---|---|
Simpson 2024 | erdos-lagarias.b | 363 |
Interp(BF,[:])
Source | Program Name/Parameters | BBB(n) |
---|---|---|
NYYRIKKI 2002 | interp-nyyrikki.b | 1243 |
Period 32 Laver table
Source | Program Name/Parameters | BBB(n) |
---|---|---|
Simpson 2024 | laver.b | 515 |
Interp(Tag(2))
Source | Program Name/Parameters | BBB(n) |
---|---|---|
Cristofani | utm.b | 467 |
Metainterp(BF)
Source | Program Name/Parameters | BBB(n) |
---|---|---|
Bologov 2023 | meta.bf | 1712 |
Interp(BCL)
Source | Program Name/Parameters | BBB(n) |
---|---|---|
Felgenhauer 2024 | bcl.bf | 2079 |
Future Directions
What should we document next?
Problems
Found by surveying Wikipedia and also from Code Golf Stack Exchange.
- Brocard conjecture: For all prime numbers p ≥ 5 and q the next prime after p, is it the case that there are at least four prime numbers between p² and q²? Note that while Brocard's name is attached to this, I don't have evidence that they are the conjecturer. There is a clear similarity to the Legendre conjecture, although they are not directly connected.
- Brocard–Ramanujan conjecture, also called "Brocard's problem": Is there a fourth solution to the factorial equation n! + 1 = m²? Erdős thought not.
- Erdős–Mollin–Walsh conjecture: Are there any triples of consecutive powerful numbers? There are infinitely many pairs. Conjectured to not exist by Erdős in 1976 and Mollin & Walsh in 1986.
- Erdős–Moser conjecture: Does a certain equation have any non-trivial solutions? Equivalently, do any of the convergents of a certain transcendental constant fulfill a certain equation? The latter sounds like it could be done on a machine.
- Firoozbakht's second conjecture: Is there a fourth natural number k such that k exponentiated to the k'th power, plus three, is prime? Given by Firoozbakht in 2009. Not to be confused with Firoozbakt's first conjecture about the distribution of primes, which seems harder to encode on a computer.
- Friendly number conjecture: Is ten a solitary number? There are other small open cases, like fourteen or fifteen, which could also be studied.
- Generalized taxicab conjecture: Is the generalized taxicab function well-defined at Taxicab(5,2,2); are there four natural numbers a, b, c, and d such that a⁵ + b⁵ = c⁵ + d⁵? Guy noted it as an open problem in 2004, but it is unlikely that Ramanujan was unaware of it.
- Greathouse conjecture: Is there a fourth natural number expressible as four sums of distinct powers; of powers of two, three, four, and five respectively? Conjectured by Greathouse in 2016 while editing OEIS; this is OEIS A146025.
- Quasiperfect numbers: Do they exist? It's not clear who introduced the concept, but there's a rich literature going back over a century of folks studying the properties such numbers must have.
- Van Landingham conjecture: In base 10, does the map which reverses the digits of a number and adds it to the original ("reverse-and-add") always have palindromes among its iterates? In particular, does 196 ever lead to a palindrome? This one is not amenable or useful to number theory, but is still useful as a gauge due to its ease of implementation.
- Wall-Sun-Sun conjecture: Is there at least one Wall-Sun-Sun prime? Wall asked in 1960 as part of an examination into Fibonacci sequences (mod n), and Sun & Sun asked in 1992 as part of the quest to prove Fermat's Last Theorem.
Languages
Suggested by ais523:
- Tag systems: programs are triples of a positive natural number ("skip"), a set ("alphabet") with a chosen element ("halting symbol"), and a map ("production") mapping the alphabet to strings of the alphabet ("words"); indices are the skip, the cardinality of the alphabet, and the maximum length of any word in the production
- The Waterfall Model: programs are square matrices of natural numbers; indices are matrix size, maximum starting waterclock (maximum over first column), maximum trigger value (maximum over rest of matrix)
For tag systems, they note that skip is usually 2 ("2-tag"), and that Turing-completeness begins to manifest around 5 symbols or maximum word length 3, with an explicit UTM in 2-tag, 19 symbols, maximum word length 4. Lore is that word length 2 is bounded in space, word length 3 is universal due to an algorithm which compiles down longer words, and that even though 3 is where universality starts, word length 4 is much easier for humans to work with.