# References — Chapter ᚇ(D): The locomotive *Teclam Áirme, the Mathematical Compendium — a copy for AI readers of https://www.teclamairme.com/#ref-ch-9, as of 2026-09-30. Links are relative to https://www.teclamairme.com/fortheaireaders/.* [Guide for AI readers](index.md) · [The chapter](ch09.md) *Each entry: one plain sentence saying exactly what it is cited for, its status, then every source with a note saying what that source actually carries. "Own computation" / "Own reading" entries are the author's own work, not outside sources.* ### 9.1 {#r-9.1} The untyped lambda calculus is a formal model of computation; Church first published it in 1932, in A set of postulates for the foundation of logic, and beta-reduction applies a function to an argument. Church numerals encode n as a function that applies its argument n times, so zero is λf.λx.x; the λ-definition of the predecessor function is Kleene’s. *Status: confirmed* - [Wikipedia, Lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) — defines lambda calculus as a formal system based on abstraction and application, attributes its introduction to Alonzo Church in the 1930s, and gives beta-reduction for (λx.t)s. - [Wikipedia, Church encoding](https://en.wikipedia.org/wiki/Church_encoding) — describes Church numerals as repeated function application and gives zero as λf.λx.x. - [Internet Encyclopedia of Philosophy, Lambda Calculi](https://iep.utm.edu/lambda-calculi/) — ‘Alonzo Church first introduced the λ-calculus as A set of postulates for the foundation of logic in two papers of that title published in 1932 and 1933’; says Church gave the numeral encoding at the end of the 1933 paper, and that Kleene found how to define the predecessor function. ### 9.2 {#r-9.2} Turing’s 1936 work establishes that no general mechanical procedure can decide whether an arbitrary machine and input will halt; the diagonal/self-reference argument is the standard proof idea. *Status: confirmed* - [A. M. Turing, On Computable Numbers (interactive edition)](https://biomorphbuilder.com/turing-paper/) — gives the paper’s 1936 receipt/read dates, describes machines with finite control and unbounded tape, states that no general process can determine which machines are circle-free, and connects this to the modern halting problem. ### 9.3 {#r-9.3} Church’s lambda-definability, Herbrand and Gödel’s general recursion, and Turing computability are extensionally equivalent; the Church–Turing thesis is a thesis about what counts as an effective procedure, not a theorem proved from a formal definition of ‘effective’. Gödel set out the general recursive functions in his 1934 Princeton lectures, on a suggestion of Herbrand. Church’s answer to the Entscheidungsproblem was published earlier in 1936 than Turing’s, which was received on 28 May 1936 and printed in two parts on 30 November and 23 December 1936, so Church’s was in print first; the appendix Turing added shows that the lambda-definable and the machine-computable functions are the same class. No model of computation proposed since has escaped that class: a quantum computer can always be simulated by a Turing machine, and changes what is efficient rather than what is computable. Quantum Turing machines are equivalent to deterministic Turing machines; the models that compute non-computable functions are the theoretical hypercomputers. *Status: judgement* - [A. M. Turing, On Computable Numbers (interactive edition)](https://biomorphbuilder.com/turing-paper/) — Turing says Church’s effective calculability is equivalent to his computability and discusses the equivalence in an appendix. - [Wikipedia, Lambda calculus](https://en.wikipedia.org/wiki/Lambda_calculus) — states that untyped lambda calculus can simulate any Turing machine and vice versa. - [Wikipedia, Church–Turing thesis](https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis) — Gödel ‘with Jacques Herbrand, formalized the definition of the class of general recursive functions’ and modified his approach on Herbrand’s suggestion in his 1934 Princeton lectures; Turing’s appendix ‘showed that the classes of functions defined by λ-calculus and Turing machines coincided’; the thesis ‘cannot be formally proven, as the concept of effective calculability is only informally defined’; and (read as raw HTML, 17 September 2026) a strict containment of BPP in BQP “would not however invalidate the original Church–Turing thesis, since a quantum computer can always be simulated by a Turing machine, but it would invalidate the classical complexity-theoretic Church–Turing thesis for efficiency reasons.” - [Wikipedia, Entscheidungsproblem](https://en.wikipedia.org/wiki/Entscheidungsproblem) — ‘Church’s paper was presented to the American Mathematical Society on 19 April 1935 and published on 15 April 1936’; Turing’s paper ‘was received by the Proceedings of the London Mathematical Society on 28 May 1936, read on 12 November 1936, and published in series 2, volume 42 (1936–7)’, in parts issued 30 November and 23 December 1936, with corrections in volume 43. Editorial note: We call the equivalence a confirmed mathematical result for the formal models, but retain ‘thesis’ for the broader claim about every possible machine or effective procedure: that extension is methodological and not a theorem from an agreed formal definition of human computation. ### 9.4 {#r-9.4} A Turing machine has finite control, a tape of cells, and a scanned head whose transition rules specify what to write, which way to move, and the next state; a universal machine can simulate machines described on its tape. *Status: confirmed* - [A. M. Turing, On Computable Numbers (interactive edition)](https://biomorphbuilder.com/turing-paper/) — section 1 describes finite m-configurations, an unbounded tape divided into squares, and a scanned square. - [Wikipedia, Turing machine](https://en.wikipedia.org/wiki/Turing_machine) — describes the transition function and universal-machine simulation. ### 9.5 {#r-9.5} Radó introduced the Busy Beaver problem in 1962; in the step-count convention BB(n) is the maximum number of steps made by a halting n-state, two-symbol machine started on a blank tape. *Status: confirmed* - [Busy Beaver Challenge, July 2024 announcement](https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237) — history line attributes the busy-beaver game and functions S and Σ to Radó in 1962. - [Busy Beaver Challenge paper](https://github.com/bbchallenge/bbchallenge-paper) — defines S(n) as the maximum steps of an n-state, two-symbol machine from the all-zero tape and identifies Radó in 1962. ### 9.6 {#r-9.6} For the step-count convention used here, BB(1)=1, BB(2)=6, BB(3)=21, and BB(4)=107; S(3)=21 was settled by Lin and Radó in 1965 and S(4)=107 by Brady in 1983. Radó’s own paper left the two-state step count open; Michel’s survey credits S(2) = 6, probably, to Lin in 1963, and Lin’s 1963 proof of S(3) = 21 was published by Lin and Radó in 1965. *Status: confirmed* - [Wikipedia, Busy beaver](https://en.wikipedia.org/wiki/Busy_beaver) — gives the standard small step-count values 1, 6, 21, and 107, distinguishes step-count from productivity conventions, and credits Lin and Radó (Computer Studies of Turing Machine Problems, 1965) with S(3) = 21 and Brady with S(4) = 107 in 1983. - [Pascal Michel, Historical survey of Busy Beavers](https://bbchallenge.org/~pascal.michel/ha.html) — “Rado (1963) claimed that Sigma(2, 2) = 4, but that S(2, 2) was yet unknown. The value S(2, 2) = 6 was probably set by Lin in 1963.”; “Lin (1963) proved this conjecture and this proof was eventually published by Lin and Rado (1965).”; “Brady (1974, 1975) proved this conjecture, and the proof was eventually published in Brady (1983).” ### 9.7 {#r-9.7} BB(5)=47,176,870 was proved in July 2024 by the collaborative Busy Beaver Challenge, using a formally checked Coq proof; the five-state machine that runs the 47,176,870 steps was itself found by Heiner Marxen and Jürgen Buntrock in 1989 and published in 1990, and BB(6) remains a frontier problem. *Status: confirmed* - [Busy Beaver Challenge, We have proved BB(5) = 47,176,870](https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237) — dated July 2, 2024; states the value, describes the Coq proof, reports the symmetry-reduced enumeration, and says BB(6) is a next target. - [The bbchallenge Collaboration, Determination of the fifth Busy Beaver value](https://arxiv.org/abs/2509.12337) — abstract states S(5)=47,176,870 and that the proof enumerates 181,385,789 five-state machines, deciding halting for each; posted 15 September 2025, revised 23 March 2026. - [Wikipedia, Busy beaver](https://en.wikipedia.org/wiki/Busy_beaver) — ‘The 5-state busy beaver was discovered by Heiner Marxen and Jürgen Buntrock in 1989, but only proved to be the winning fifth busy beaver in 2024 by an online amateur mathematical collective, using a proof formalized in Rocq.’ ### 9.8 {#r-9.8} Busy Beaver grows faster than every computable function and is uncomputable, because a sufficiently effective exact computation of its values would decide halting for bounded-size machines. *Status: confirmed* - [Wikipedia, Busy beaver](https://en.wikipedia.org/wiki/Busy_beaver) — states that the Busy Beaver function is non-computable and eventually dominates every computable function, with the halting-problem reduction. ### 9.9 {#r-9.9} Ackermann’s function is a total computable function that is not primitive recursive; the common two-variable recurrence has A(0, n)=n+1, A(m, 0)=A(m−1, 1), and A(m, n)=A(m−1, A(m, n−1)). *Status: confirmed* - [NIST Dictionary of Algorithms and Data Structures, Ackermann’s function](https://xlinux.nist.gov/dads/HTML/ackermann.html) — gives the recurrence, attributes the 1928 observation to Wilhelm Ackermann, and states that the function is recursive but not primitive recursive. - [Stanford Encyclopedia of Philosophy, History of the Ackermann and Péter functions](https://seop.illc.uva.nl/entries/recursive-functions/ackermann-peter.html) — explains that Ackermann’s result was growth beyond functions defined by ordinary recursion and discusses the historical qualification. ### 9.10 {#r-9.10} Under the displayed Péter-style recurrence, A(3, 3)=61 and A(4, 2)=2^65536−3, a 19,729-digit integer; A(4, 3)=2^(2^65536)−3, which has far too many digits to write out. *Status: confirmed* - [Wikipedia, Ackermann function](https://en.wikipedia.org/wiki/Ackermann_function) — gives the common recurrence, A(3, 3)=61, and A(4, 2)=2^65536−3 with 19,729 decimal digits. - [NIST Dictionary of Algorithms and Data Structures, Ackermann’s function](https://xlinux.nist.gov/dads/HTML/ackermann.html) — provides the recurrence used to recompute A(3, 3). Editorial note: Own arithmetic check: the recurrence gives A(3, 3)=61; 2^65536−3 has floor(65536 log10 2)+1 = 19,729 digits; A(4, n) = 2↑↑(n+3) − 3, so A(4, 3) = 2^(2^65536) − 3, whose decimal expansion has about 10^19,728 digits. ### 9.11 {#r-9.11} P is contained in NP: a deterministic polynomial-time solver is also a polynomial-time verifier that can ignore its certificate; the status of P versus NP remains open. In the notation those classes are written in, f = O(g) means |f| is eventually bounded by a constant multiple of g; Bachmann proposed the notation in 1894, Landau extended it in 1909, and Knuth fixed Ω and Θ for the family in 1976. Comparison sorting needs Ω(n log n) comparisons, and Harvey and van der Hoeven multiply two n-digit integers in O(n log n) bit operations. Harvey and van der Hoeven announced their O(n log n) multiplication algorithm in March 2019; it was published in 2021. *Status: confirmed* - [Wikipedia, P versus NP problem](https://en.wikipedia.org/wiki/P_versus_NP_problem) — defines P and NP through polynomial-time solving and verification and states the open P-versus-NP question. - [Wikipedia, Big O notation](https://en.wikipedia.org/wiki/Big_O_notation) — ‘Bachmann proposed the notation in 1894 and Landau extended it in 1909’; ‘In 1976, Donald Knuth defined f(x) = Ω(g(x)) ⟺ g(x) = O(f(x))’; f(x) = O(g(x)) if there is a positive real M with |f(x)| ≤ M·g(x) throughout the domain. Its table of orders gives n log n as the “fastest possible comparison sort; heapsort and merge sort.” - [Wikipedia, Comparison sort](https://en.wikipedia.org/wiki/Comparison_sort) — ‘A comparison sort must have an average-case lower bound of Ω(n log n) comparison operations’. - [David Harvey and Joris van der Hoeven, Integer multiplication in time O(n log n)](https://doi.org/10.4007/annals.2021.193.2.4) — Annals of Mathematics 193 (2021), 563–617 (the March 2019 preprint announcement is on the Multiplication algorithm line). Multiplies two n-bit integers in O(n log n) bit operations, confirming the 1971 conjecture of Schönhage and Strassen. - [Multiplication algorithm, Wikipedia](https://en.wikipedia.org/wiki/Multiplication_algorithm) — “In March 2019, David Harvey and Joris van der Hoeven announced their discovery of an O(n log n) multiplication algorithm.”; “It was published in the Annals of Mathematics in 2021.” ### 9.12 {#r-9.12} The historical attributions in the card are Cook (1971) for NP-completeness of satisfiability, Levin (1973) for the independent theorem, and Karp (1972) for a list of 21 NP-complete problems; Cobham and Edmonds supplied early polynomial-time formulations in 1965. Karp’s list includes the undirected Hamilton circuit, the round trip that visits every point of a network exactly once. *Status: confirmed* - [Wikipedia, P versus NP problem](https://en.wikipedia.org/wiki/P_versus_NP_problem) — records Cook 1971, Levin 1973, and Karp’s 21 NP-complete problems (without a year; 1972 is on the Karp line) in the history of NP-completeness and the P-versus-NP problem. - [Wikipedia, Cobham’s thesis](https://en.wikipedia.org/wiki/Cobham%27s_thesis) — ‘Alan Cobham’s 1965 paper entitled The intrinsic computational difficulty of functions is one of the earliest mentions of the concept of the complexity class P’, and ‘Jack Edmonds’s 1965 paper Paths, trees, and flowers is also credited with identifying P with tractable problems’. - [Karp’s 21 NP-complete problems, Wikipedia](https://en.wikipedia.org/wiki/Karp%27s_21_NP-complete_problems) — “In his 1972 paper, ‘Reducibility Among Combinatorial Problems’, Richard Karp used Stephen Cook’s 1971 theorem that the Boolean satisfiability problem is NP-complete (also called the Cook–Levin theorem) to show that there is a polynomial time many-one reduction from the Boolean satisfiability problem to each of 21 combinatorial and graph theoretical computational problems, thereby showing that they are all NP-complete.”; its list includes “Undirected Hamilton circuit (Karp’s name, now usually called Undirected Hamiltonian cycle),” and it calls the paper “one of the first demonstrations that many natural computational problems occurring throughout computer science are computationally intractable.” ### 9.13 {#r-9.13} IEEE binary64 uses 53 bits of significand precision; the next representable number above 1 is 1+2^−52, so the spacing immediately above 1 is 2^−52 ≈ 2.220446×10^−16. Decimal fractions such as 0.1 and 0.2 have no finite binary expansion, so they are stored rounded, which is a separate mechanism from the spacing at 1 and is why 0.1 + 0.2 does not equal 0.3 in binary64. The name machine epsilon has two prevailing definitions: in the mainstream one it is this gap, 2^−52; in the formal one (unit roundoff) it is half of it, 2^−53. *Status: confirmed* - [Wikipedia, IEEE 754](https://en.wikipedia.org/wiki/IEEE_754) — describes binary64 as having 53 bits of precision and gives the binary64 spacing/precision facts: “The binary32 (single) and binary64 (double) formats are two of the most common formats used today.” - [Double-precision floating-point format, Wikipedia](https://en.wikipedia.org/wiki/Double-precision_floating-point_format) — (§ IEEE 754 double-precision binary floating-point format: binary64, § Double-precision examples): “Significand precision: 53 bits (52 explicitly stored),” and the smallest number greater than 1 is 1.0000000000000002220…, so the spacing immediately above 1 is 2⁻⁵² ≈ 2.220446 × 10⁻¹⁶; “The maximum relative rounding error when rounding a number to the nearest representable one (the machine epsilon) is therefore 2⁻⁵³.” (exponent as typeset on the page) - [Floating-point arithmetic, Wikipedia](https://en.wikipedia.org/wiki/Floating-point_arithmetic) — read as raw wikitext: “The classical toy problem that illustrates the issue with decimals is 0.1 + 0.2 - 0.3, which evaluates to about 5.551e-17 in double precision instead of the expected 0, because as stated above in Representable numbers, conversion and rounding all three numbers cannot be represented by a finite binary expansion.” - [Machine epsilon, Wikipedia](https://en.wikipedia.org/wiki/Machine_epsilon) — “There are two prevailing definitions, denoted here as rounding machine epsilon or the formal definition and interval machine epsilon or mainstream definition.”; “In the mainstream definition, machine epsilon is independent of rounding method, and is defined simply as the difference between 1 and the next larger floating point number.” Its table gives binary64 a rounding machine epsilon of 2⁻⁵³ ≈ 1.11e-16 and an interval machine epsilon of 2⁻⁵² ≈ 2.22e-16 (exponents as typeset on the page). ### 9.14 {#r-9.14} With round-to-nearest, ties-to-even, binary64 evaluates fl(1+2^−53) to 1 because the exact value is halfway between 1 and 1+2^−52 and 1 has an even low significand bit; subtracting 1 therefore gives 0. *Status: confirmed* - [Wikipedia, IEEE 754](https://en.wikipedia.org/wiki/IEEE_754) — describes round-to-nearest, ties-to-even and binary floating-point formats. - [David Goldberg, What Every Computer Scientist Should Know About Floating-Point Arithmetic, ACM Computing Surveys 23(1), March 1991](https://docs.oracle.com/cd/E19957-01/806-3568/ncg_goldberg.html) — sets out the round-to-even rule and argues for it (Theorem 5), then adopts it — “Throughout the rest of this paper, round to even will be used” — and defines machine epsilon. It is the classic exposition, not the specification; the ties-to-even default itself is carried by the IEEE 754 entry above. Editorial note: Own computation: 1+2^−53 is exactly the midpoint of 1 and 1+2^−52; the significand of 1 has an even trailing bit, so the rounded result is 1 and the subtraction is exactly zero. ### 9.15 {#r-9.15} Kolmogorov complexity is the length of the shortest program in a fixed language that outputs a string; it is uncomputable, by an argument modeled on Berry’s paradox. Solomonoff published the idea in 1960 and described it more fully in 1964; Kolmogorov published it independently in 1965 and acknowledged Solomonoff’s priority once he became aware of that work; Chaitin’s Journal of the ACM paper appeared in 1966. Chaitin’s constant Ω is the halting probability of a universal machine, one for each encoding of programs. *Status: confirmed* - [Wikipedia, Kolmogorov complexity](https://en.wikipedia.org/wiki/Kolmogorov_complexity) — defines the shortest-program measure and explains uncomputability through a construction ‘modeled on a self-referential construction used in Berry’s paradox’; says Solomonoff ‘published it in 1960’ in A Preliminary Report on a General Theory of Inductive Inference and ‘gave a more complete description in his 1964 publications’, that Kolmogorov ‘later independently published this theorem in Problems Inform. Transmission in 1965’, that Chaitin presents it in the Journal of the ACM, and that ‘When Kolmogorov became aware of Solomonoff’s work, he acknowledged Solomonoff’s priority’. - [Algorithmic information theory, Wikipedia](https://en.wikipedia.org/wiki/Algorithmic_information_theory) — “Algorithmic information theory was later developed independently by Andrey Kolmogorov, in 1965 and Gregory Chaitin, around 1966.”; its references list Chaitin, “On the Length of Programs for Computing Finite Binary Sequences,” Journal of the ACM 13 (4): 547–569 (1966). - [Chaitin’s constant, Wikipedia](https://en.wikipedia.org/wiki/Chaitin%27s_constant) — a real number that, “informally speaking, represents the probability that a randomly constructed program will halt”; “Although there are infinitely many halting probabilities, one for each (universal, see below) method of encoding programs, it is common to use the letter Ω to refer to them as if there were only one.” ### 9.16 {#r-9.16} Rice’s theorem says every nontrivial semantic property of the partial function computed by a program is undecidable; Rice proved the theorem in his 1951 dissertation and published it in 1953. *Status: confirmed* - [Wikipedia, Rice’s theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem) — states the theorem for nontrivial semantic properties of programs and gives the 1951 dissertation/1953 publication history. ### 9.17 {#r-9.17} In combinatory logic, S=λxyz.xz(yz), K=λxy.x, and I=SKK; every lambda term can be represented using S and K, while Curry’s Y combinator satisfies Yf=f(Yf). Schönfinkel introduced the combinators in 1920 and published them in 1924; Curry rediscovered them at Princeton in 1927 and published Grundlagen der kombinatorischen Logik in 1930. Schönfinkel’s 1920 introduction was a talk to the Göttingen Mathematics Society. *Status: confirmed* - [Wikipedia, Combinatory logic](https://en.wikipedia.org/wiki/Combinatory_logic) — gives the S, K, and I combinators, the S/K basis, and the fixed-point combinator construction; says the combinators ‘were introduced by Schönfinkel in 1920’ and published in 1924, and that Curry ‘rediscovered the combinators while working as an instructor at Princeton University in late 1927’, publishing Grundlagen der Kombinatorischen Logik in 1930. - [Wikipedia, Fixed-point combinator](https://en.wikipedia.org/wiki/Fixed-point_combinator) — gives Y = λf.(λx.f (x x)) (λx.f (x x)) as ‘Haskell Curry’s paradoxical combinator Y’, satisfying Y g = g (Y g). - [Stephen Wolfram, Where Did Combinators Come From? Hunting the Story of Moses Schönfinkel](https://writings.stephenwolfram.com/2020/12/where-did-combinators-come-from-hunting-the-story-of-moses-schonfinkel/) — “On Tuesday, December 7, 1920, the Göttingen Mathematics Society held its regular weekly meeting—at which a 32-year-old local mathematician named Moses Schönfinkel with no known previous mathematical publications gave a talk entitled ‘Elemente der Logik’ (‘Elements of Logic’).”; “Moses Schönfinkel described the result of his 1920 talk in an 11-page paper published in 1924” ### 9.18 {#r-9.18} Gödel numbering encodes symbols, formulas, and proofs as natural numbers so arithmetic can represent syntactic statements; Turing’s universal machine similarly encodes program descriptions on its tape. Under the numbering, Gödel’s sentence says that a certain calculation yields the Gödel number of an unprovable formula; ⌜φ⌝ is the standard notation for the numeral of φ’s code. *Status: confirmed* - [Wikipedia, Gödel numbering](https://en.wikipedia.org/wiki/G%C3%B6del_numbering) — describes the encoding of symbols, formulas, and proofs by natural numbers and its role in incompleteness; “Gödel used a system based on prime factorization..” - [A. M. Turing, On Computable Numbers (interactive edition)](https://biomorphbuilder.com/turing-paper/) — describes machine descriptions and universal-machine computation. - [Gödel’s incompleteness theorems, Wikipedia](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems) — “The statement p is not literally equal to ~Bew(G(p)); rather, p states that if a certain calculation is performed, the resulting Gödel number will be that of an unprovable statement.” - [Diagonal lemma, Wikipedia](https://en.wikipedia.org/wiki/Diagonal_lemma) — “For n̄, the standard numeral of n (i.e. 0̄ =df 0 and n+1̄ =df S(n̄)), let ⌜φ⌝ be the standard numeral of the code of φ.” ### 9.19 {#r-9.19} The displayed arithmetic checks are correct: (λf.λx.x) S 0 reduces in two beta steps to 0; 1+6+21+107=135, so 47,176,870 + 61 + 135 = 47,177,066; and the three denominator terms are positive step counts while [P⊆NP]=1 and the binary64 rounding numerator is 0. *Status: confirmed* - **Own computation** (the author's own work) — Direct symbolic/arithmetic check: (λf.λx.x) S 0 → (λx.x) 0 → 0; 1+6+21+107=135 and 47,176,870 + 61 + 135 = 47,177,066; the cited Busy Beaver values are positive; P⊆NP is a true inclusion; and the midpoint tie calculation in binary64 gives fl(1+2^−53)−1=0. ### 9.20 {#r-9.20} The BB(5) proof enumerates 181,385,789 five-state, two-symbol Turing machines and decides halting for each; the July 2024 announcement describes that as the search space reduced by symmetry to about 180 million machines. The unreduced space is 21^10 = 16,679,880,978,201 machines, about 17 trillion, since each of the ten state-and-symbol pairs takes one of twenty transitions or halts. *Status: confirmed* - [The bbchallenge Collaboration, Determination of the fifth Busy Beaver value](https://arxiv.org/abs/2509.12337) — abstract explicitly says the proof enumerates 181,385,789 five-state machines. - [Busy Beaver Challenge, July 2024 announcement](https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237) — says the space was reduced to approximately 180 million machines using symmetries. Editorial note: Own arithmetic: five states and two symbols give ten table entries, each of which writes one of two symbols, moves one of two ways and enters one of five states, or halts, so 21^10 = 16,679,880,978,201. Both counts are correct and count different things; the number the chapter gives is the one the proof actually enumerates. ### 9.21 {#r-9.21} David Hilbert and Wilhelm Ackermann posed the Entscheidungsproblem in 1928; it asks for an algorithm that answers yes or no according to whether an input statement is universally valid, that is, valid in every structure. In 1936 Alonzo Church and Alan Turing published independent papers showing that a general solution is impossible. *Status: confirmed* - [Entscheidungsproblem, Wikipedia](https://en.wikipedia.org/wiki/Entscheidungsproblem) — attributes the problem to ‘David Hilbert and Wilhelm Ackermann in 1928’; states that it asks for ‘an algorithm that considers an input statement and answers yes or no according to whether it is universally valid, i.e., valid in every structure’; and that ‘In 1936, Alonzo Church and Alan Turing published independent papers showing that a general solution to the Entscheidungsproblem is impossible’; and ‘Turing reduced the question of the existence of an ‘algorithm’ or ‘general method’ able to solve the Entscheidungsproblem to the question of the existence of a ‘general method’ that decides whether any given Turing machine halts or not (the halting problem).’ Editorial note: The dates of the two 1936 papers, and Turing’s appendix showing the two answers describe the same class, are carried separately by 9.3. ### 9.22 {#r-9.22} The first IEEE standard for floating-point arithmetic, IEEE 754-1985, was published in 1985, and round to nearest, ties to even is its default rounding for binary floating point. Almost all modern machines follow it, and on most systems the double type is its binary64 format. *Status: confirmed* - [IEEE 754, Wikipedia](https://en.wikipedia.org/wiki/IEEE_754) — ‘The first IEEE standard for floating-point arithmetic, IEEE 754-1985, was published in 1985’, and ‘Round to nearest, ties to even’ is given as the default for binary floating point. - [Floating-point arithmetic, Wikipedia](https://en.wikipedia.org/wiki/Floating-point_arithmetic) — “This first standard is followed by almost all modern machines.” - [Double-precision floating-point format, Wikipedia](https://en.wikipedia.org/wiki/Double-precision_floating-point_format) — “Double precision is not required by the standards (except by the optional annex F of C99, covering IEEE 754 arithmetic), but on most systems, the double type corresponds to double precision.” Editorial note: Added in the V14 prose pass: the chapter’s 1985 date and the card line ‘the double of every mainstream language since the 1985 standard’ previously stood on 9.13, whose claim covers only binary64 precision and spacing and carries no date. ### 9.23 {#r-9.23} The chapter epigraph is the opening sentence of Turing’s On Computable Numbers, with an Application to the Entscheidungsproblem, received 28 May 1936 and read 12 November 1936. *Status: confirmed* - [A. M. Turing, On Computable Numbers (full text)](https://biomorphbuilder.com/turing-paper/) — read as raw HTML: “Received 28 May, 1936 — Read 12 November, 1936. Proceedings of the London Mathematical Society, s2-42 (1937), pp. 230–265,” and the paper opens “The ‘computable’ numbers may be described briefly as the real numbers whose expressions as a decimal are calculable by finite means,” which is the epigraph word for word. Editorial note: Added 17 September 2026 to source the chapter epigraph, which carried no marker. The footer dates the paper 1936, which is the year it was received and read; the volume it appeared in is dated 1937, as r-9.3 already records. ### 9.24 {#r-9.24} Dates and attributions printed on this chapter’s glossary cards and in its field notes, each checked against the source listed: Goedel’s 1931 proof introduced the numbering; Turing’s universal machine of 1936. *Status: confirmed* - [Gödel numbering, Wikipedia](https://en.wikipedia.org/wiki/G%C3%B6del_numbering) — read raw: “Since the publishing of Gödel’s paper in 1931, the term “Gödel numbering” or “Gödel code” has been used to refer to more general assignments of natural numbers to mathematical objects..” - [Universal Turing machine, Wikipedia](https://en.wikipedia.org/wiki/Universal_Turing_machine) — read raw: “Turing introduced the idea of such a machine in 1936–1937..” Editorial note: Added 18 September 2026 by the V42 citation sweep. citecheck.py found these years printed on a card or in a paragraph whose cited entries did not carry them; each was then verified against a source fetched raw that day, and the quotation in each source note is verbatim. ### 9.25 {#r-9.25} States the recursive definition of Ackermann’s function and that it is total and computable yet not primitive recursive. Notes Ackermann’s 1928 three-argument original, Péter’s two-argument form, A(3, 3) = 61, and that A(4, 2) has 19,729 decimal digits. *Status: confirmed* - [Ackermann function, Wikipedia](https://en.wikipedia.org/wiki/Ackermann_function) — gives the Ackermann-Peter recurrence and states the function is computable but grows faster than any primitive recursive function. - [Wilhelm Ackermann, MacTutor](https://mathshistory.st-andrews.ac.uk/Biographies/Ackermann/) — carries the two-argument simplification: “A(x, y, z) was simplified to a function P(x, y) of two variables by Rozsa Peter whose initial condition was simplified by Raphael Robinson.”