[paper] [intro] bbchallenge: change "88664064 Turing machines" to "ab…

…out 180 million Turing machines" (teorth#971)

Hello,

I maintain bbchallenge.org and I wanted to thank you for mentioning our
project in your intro.

Although currently (and unfortunately) unclear on [our
website](https://bbchallenge.org/) at present time but touched on on
[our wiki
](https://wiki.bbchallenge.org/wiki/Tree_Normal_Form#Number_of_TNF_TMs),
the number of machines enumerated and analysed by the [Coq
proof](https://github.com/ccz181078/Coq-BB5) of "BB(5) = 47,176,870" is
about 180 million and not 88664064.

Reason for discrepancies in these numbers:

1. The author of the [Coq proof](https://github.com/ccz181078/Coq-BB5)
implemented their own enumeration of Turing machines in Coq rather than
using the database provided by the website (which contained 88664064
machines)

2. They enumerated both machines that write a 0 and machines that write
a 1 at the first step (whereas the database provided on the website only
enumerated machines that write a 1 first (this is in fact enough))

3. The ~180 million number of machines that the Coq proof enumerates
contains both halting and non-halting machines whereas the 88664064
number contained only machines that were suspected not to halt

4. We are in the process of extracting from the Coq proof the exact
number of enumerated machines but we know for sure that it is between
180 and 185 million (other implementations report 181,385,789). We
should know the exact number in the coming weeks (meanwhile, and maybe
in all cases, "about 180 million" is probably good wording unless you
prefer the specific number, which I can post here when we have it).

Thank you very much again :)

paper/intro.tex

@@ -30,7 +30,7 @@ \subsection{The Equational Theories Project}
 
 As noted in \Cref{numbering-app}, there are $4694$ equational laws of order at most $4$. The primary mathematical goal of the ETP was to completely determine the \emph{implication graph} for these laws, in which there is a directed edge from $E$ to $E'$ precisely when $E \vdash E'$. Such systematic determinations of implication graphs have been seen previously in the literature; for instance, in \cite{phillips-vojtechovsky}, the relations between $60$ identities of Bol--Moufang type were established, and in the blog post \cite[\S 17]{Wolfram_2022}, some initial steps towards generating this graph for the first hundred or so laws on our list were performed. However, to our knowledge, the ETP is the first project to study such implications at the scale of thousands of laws.
 
-The ETP requires the determination of the truth or falsity of $4694^2 = 22033636$ implications; while one can use properties such as the transitivity of entailment to reduce the work somewhat, this is clearly a task that requires significant automation. It was also a project highly amenable to crowdsourcing, in which different participants could work on developing different techniques, each of which could be used to fill out a different part of the implication graph. In this respect, the project could be compared with a Polymath project \cite{Gowers2009}, which used online forums such as blogs and wikis to openly collaborate on a mathematical research problem. However, the Polymath model required human moderators to review and integrate the contributions of the participants, which clearly would not scale to the ETP which required the verification of over twenty million mathematical statements. Instead, the ETP was centered around a Github repository in which the formal mathematical contributions had to be entered in the proof assistant language \emph{Lean}, where they could be automatically verified. In this respect, the ETP was more similar to the recently concluded Busy Beaver Challenge\footnote{\url{https://bbchallenge.org/}}, which was a similarly crowdsourced project that computed the fifth Busy Beaver number $BB(5)$ to be $47176870$ through an analysis of $88664064$ Turing machines, with the halting analysis being verified in a variety of computer languages, with the final formal proof written in the proof assistant language \emph{Coq}. One of the aims of the ETP was to explore potential workflows for such collaborative, formally verified mathematical research projects that could serve as a model for future projects of this nature.
+The ETP requires the determination of the truth or falsity of $4694^2 = 22033636$ implications; while one can use properties such as the transitivity of entailment to reduce the work somewhat, this is clearly a task that requires significant automation. It was also a project highly amenable to crowdsourcing, in which different participants could work on developing different techniques, each of which could be used to fill out a different part of the implication graph. In this respect, the project could be compared with a Polymath project \cite{Gowers2009}, which used online forums such as blogs and wikis to openly collaborate on a mathematical research problem. However, the Polymath model required human moderators to review and integrate the contributions of the participants, which clearly would not scale to the ETP which required the verification of over twenty million mathematical statements. Instead, the ETP was centered around a Github repository in which the formal mathematical contributions had to be entered in the proof assistant language \emph{Lean}, where they could be automatically verified. In this respect, the ETP was more similar to the recently concluded Busy Beaver Challenge\footnote{\url{https://bbchallenge.org/}}, which was a similarly crowdsourced project that computed the fifth Busy Beaver number $BB(5)$ to be $47176870$ through an analysis of about $180$ million Turing machines, with the halting analysis being verified in a variety of computer languages, with the final formal proof written in the proof assistant language \emph{Coq}. One of the aims of the ETP was to explore potential workflows for such collaborative, formally verified mathematical research projects that could serve as a model for future projects of this nature.
 
 Secondary aims of the ETP included the possibility of discovering unusually interesting equational laws, or new experimental observations about such laws, that had not previously been noticed in the literature; and to develop benchmarks to assess the performance of automated theorem provers and other AI tools.