Tired of going to Scott "Other" Aaronson's blog to find out what's currently known about the busy beaver game? I maintain a community website that has summaries for the known numbers in Busy Beaver research, the Busy Beaver Gauge.
I started this site last year because I was worried that Other Scott was excluding some research and not doing a great job of sharing links and history. For example, when it comes to Turing machines implementing the Goldbach conjecture, Other Scott gives O'Rear's 2016 result but not the other two confirmed improvements in the same year, nor the recent 2024 work by Leng.
Concretely, here's what I offer that Other Scott doesn't:
- A clear definition of which problems are useful to study
- Other languages besides Turing machines: binary lambda calculus and brainfuck
- A plan for how to expand the Gauge as a living book: more problems, more languages and machines
- The content itself is available on GitHub for contributions and reuse under CC-BY-NC-SA
- All tables are machine-computed when possible to reduce the risk of handwritten typos in (large) numbers
- Fearless interlinking with community wikis and exporting of knowledge rather than a complexity-zoo-style silo
- Acknowledgement that e.g. Firoozbakht is part of the mathematical community
I accept PRs, although most folks ping me on IRC (korvo on Libera Chat, try #esolangs) and I'm fairly decent at keeping up on the news once it escapes Discord. Also, you (yes, you!) can probably learn how to write programs that attempt to solve these problems, and I'll credit you if your attempt is short or novel.
Other Scott has clarified his position on citational standards in a comment on his blog:
In contrast, the Gauge's standard is that a claim needs reproducible computable artifacts as supporting evidence, with inline comments serving as sufficient documentation for those already well-versed in the topic, and any supporting papers or blog posts are merely a nicety for explaining the topic and construction to the mathematical community and laity at large. If a claim is not sufficiently strong then we should introduce more computational evidence to settle the question at hand.
For example, Leng 2024 gives a construction in Lean 4. If this is not strong enough then the Gauge could be configured to compile a Nix-friendly Lean 4 and expend some compute in CI to verify the proof, so that the book only builds if Leng's proof is valid. Further critique would focus on what Leng actually proved in terms of their Lean 4 code. Other Scott isn't convinced by this, so it's not part of the story that they will tell.