{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T18:57:45Z","timestamp":1781031465285,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":97,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T00:00:00Z","timestamp":1780963200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,6,9]]},"DOI":"10.1145\/3798129.3806376","type":"proceedings-article","created":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:53:56Z","timestamp":1781027636000},"page":"565-574","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Determination of the Fifth Busy Beaver Value"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-7117-0375","authenticated-orcid":false,"given":"Justin","family":"Blanchard","sequence":"first","affiliation":[{"name":"Independent, Brooklyn, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5216-1503","authenticated-orcid":false,"given":"Daniel","family":"Briggs","sequence":"additional","affiliation":[{"name":"Independent, Northampton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9910-0911","authenticated-orcid":false,"given":"Konrad","family":"Deka","sequence":"additional","affiliation":[{"name":"Jagiellonian University, Krak\u00f3w, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3164-4921","authenticated-orcid":false,"given":"Nathan","family":"Fenner","sequence":"additional","affiliation":[{"name":"Independent, San Francisco, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8676-9819","authenticated-orcid":false,"given":"Yannick","family":"Forster","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3385-776X","authenticated-orcid":false,"given":"Georgi","family":"Georgiev (Skelet)","sequence":"additional","affiliation":[{"name":"Sofia University, Sofia, Bulgaria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-2665-0223","authenticated-orcid":false,"given":"Matthew L.","family":"House","sequence":"additional","affiliation":[{"name":"University of Georgia, Athens, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-1308-9492","authenticated-orcid":false,"given":"Maja","family":"K\u0105dzio\u0142ka","sequence":"additional","affiliation":[{"name":"University of Warsaw, Warsaw, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-6622-5849","authenticated-orcid":false,"given":"Pavel","family":"Kropitz","sequence":"additional","affiliation":[{"name":"Independent, \u017dilina, Slovakia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7163-5570","authenticated-orcid":false,"given":"Shawn","family":"Ligocki","sequence":"additional","affiliation":[{"name":"Independent, Providence, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3843-4303","authenticated-orcid":false,"family":"mxdys","sequence":"additional","affiliation":[{"name":"Independent, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-6824-8966","authenticated-orcid":false,"given":"Mateusz","family":"Na\u015bciszewski","sequence":"additional","affiliation":[{"name":"Independent, Krak\u00f3w, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2649-3718","authenticated-orcid":false,"given":"Tristan","family":"St\u00e9rin","sequence":"additional","affiliation":[{"name":"PRGM DEV, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0267-9398","authenticated-orcid":false,"given":"Chris","family":"Xu","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3150-6571","authenticated-orcid":false,"given":"Jason","family":"Yuen","sequence":"additional","affiliation":[{"name":"University of Waterloo, Markham, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3580-8806","authenticated-orcid":false,"given":"Th\u00e9o","family":"Zimmermann","sequence":"additional","affiliation":[{"name":"LTCI - T\u00e9l\u00e9com Paris - Institut Polytechnique de Paris, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3427361.3427369"},{"key":"e_1_3_2_1_2_1","volume-title":"Mateusz Na\u015bciszewski,  savask, Tristan St\u00e9rin, Chris Xu, Jason Yuen, and Th\u00e9o Zimmermann.","author":"Collaboration The","year":"2026","unstructured":"The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev (Skelet), Matthew L. House, Rachel Hunter, Iijil, Maja K\u0105dzio\u0142ka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Na\u015bciszewski, savask, Tristan St\u00e9rin, Chris Xu, Jason Yuen, and Th\u00e9o Zimmermann. 2026. Determination of the fifth Busy Beaver value. arxiv:2509.12337. arxiv:2509.12337 v2"},{"key":"e_1_3_2_1_3_1","unstructured":"bbchallenge wiki. 2025. Champions. Wiki:. https:\/\/wiki.bbchallenge.org\/wiki\/Champions Accessed: 2025-08-10"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"A. M. Ben-Amram B. A. Julstrom and U. Zwick. 1996. A note on busy beavers and other creatures. Mathematical systems theory 29 4 (1996) 01 July-August 375\u2013386. issn:1433-0490 https:\/\/doi.org\/10.1007\/BF01192693 10.1007\/BF01192693","DOI":"10.1007\/BF01192693"},{"key":"e_1_3_2_1_5_1","unstructured":"Justin Blanchard. 2022. Finite Automata Reduction (FAR). https:\/\/github.com\/bbchallenge\/bbchallenge-deciders\/tree\/main\/decider-finite-automata-reduction"},{"key":"e_1_3_2_1_6_1","volume-title":"The Busy Beaver Challenge. Hacker News item. https:\/\/news.ycombinator.com\/item?id=34689081 Online","year":"2023","unstructured":"bmc7505. 2023. The Busy Beaver Challenge. Hacker News item. https:\/\/news.ycombinator.com\/item?id=34689081 Online; posted on Feb 7, 2023;"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_26"},{"key":"e_1_3_2_1_8_1","volume-title":"Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci","author":"Bolan Matthew","unstructured":"Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andr\u00e9s Goens, Aaron Hill, Harald Husum, Hern\u00e1n Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, J\u00e9r\u00e9my Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. Dec. The Equational Theories Project. https:\/\/github.com\/teorth\/equational_theories"},{"key":"e_1_3_2_1_9_1","volume-title":"Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci","author":"Bolan Matthew","year":"2025","unstructured":"Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andr\u00e9s Goens, Aaron Hill, Harald Husum, Hern\u00e1n Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, J\u00e9r\u00e9my Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. 2025. The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. arxiv:2512.07087. arxiv:2512.07087"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014565"},{"key":"e_1_3_2_1_11_1","volume-title":"Solutions of restricted cases of the halting problem applied to the determination of particular values of a non-computable function. Ph. D. Dissertation","author":"Brady Allen H.","unstructured":"Allen H. Brady. 1964. Solutions of restricted cases of the halting problem applied to the determination of particular values of a non-computable function. Ph. D. Dissertation. Oregon State University."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0025-5718-1983-0689479-6"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198537748.003.0009"},{"key":"e_1_3_2_1_14_1","unstructured":"Dan Briggs. 2010. Turing. https:\/\/github.com\/danbriggs\/Turing"},{"key":"e_1_3_2_1_15_1","volume-title":"Turing Machine. Quanta Magazine, 2 Jul, https:\/\/www.quantamagazine.org\/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702\/ Online","author":"Brubaker Ben","year":"2024","unstructured":"Ben Brubaker. 2024. Amateur Mathematicians Find Fifth \u201cBusy Beaver\u201d Turing Machine. Quanta Magazine, 2 Jul, https:\/\/www.quantamagazine.org\/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702\/ Online; published July\u00a02,\u00a02024;"},{"key":"e_1_3_2_1_16_1","unstructured":"Code Golf Addict. 2016. list27.txt. \u2260wline. https:\/\/gist.github.com\/anonymous\/a64213f391339236c2fe31f8749a0df6"},{"key":"e_1_3_2_1_17_1","unstructured":"Johan Commelin and the Lean community. 2022. Completion of the Liquid Tensor Experiment. Accessed: 2025-10-18"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Johan Commelin and Adam Topaz. 2023. Abstraction boundaries and spec driven development in pure mathematics. arxiv:arXiv:2309.14870.","DOI":"10.1090\/bull\/1831"},{"key":"e_1_3_2_1_19_1","volume-title":"Informal Proceedings of the Workshop on Logical Frameworks.","author":"Coquand Thierry","year":"1999","unstructured":"Thierry Coquand, Jean Gallier, and Le Cedex. 1999. A Proof of Strong Normalization For the Theory of Constructions Using a Kripke-Like Interpretation. In Informal Proceedings of the Workshop on Logical Frameworks."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0165-0114(91)90130-I"},{"key":"e_1_3_2_1_21_1","volume-title":"Felix E. Browder (Ed.) (Proceedings of Symposia in Pure Mathematics","volume":"378","author":"Davis Martin","year":"1976","unstructured":"Martin Davis, Yuri Matiyasevich, and Julia Robinson. 1976. Hilbert\u2019s Tenth Problem: Diophantine Equations \u2013 Positive Aspects of a Negative Solution. In Mathematical Developments Arising from Hilbert Problems, Felix E. Browder (Ed.) (Proceedings of Symposia in Pure Mathematics, Vol. 28). American Mathematical Society, 323\u2013378."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_23_1","volume-title":"Formal Conjectures: A collection of formalized statements of conjectures in Lean. GitHub repository. URL: https:\/\/github.com\/google-deepmind\/formal-conjectures","author":"DeepMind","year":"2025","unstructured":"DeepMind (Google). 2025. Formal Conjectures: A collection of formalized statements of conjectures in Lean. GitHub repository. URL: https:\/\/github.com\/google-deepmind\/formal-conjectures"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0017089508004655"},{"key":"e_1_3_2_1_25_1","unstructured":"Frans Faase. 2022. Symbolic TM. https:\/\/github.com\/FransFaase\/SymbolicTM"},{"key":"e_1_3_2_1_26_1","unstructured":"Nathan Fenner. 2022. bbchallenge Dafny deciders. https:\/\/github.com\/Nathan-Fenner\/bbchallenge-dafny-deciders"},{"key":"e_1_3_2_1_27_1","unstructured":"Nathan Fenner. 2022. bbchallenge-regexy-decider. https:\/\/github.com\/Nathan-Fenner\/bbchallenge-regexy-decider"},{"key":"e_1_3_2_1_28_1","unstructured":"Nathan Fenner. 2023. n-GRAM CPS Decider. https:\/\/github.com\/Nathan-Fenner\/bb-simple-n-gram-cps"},{"key":"e_1_3_2_1_29_1","unstructured":"Georgi Georgiev. 2003. Busy Beaver nonregular machines for class TM(5). https:\/\/skelet.ludost.net\/bb\/nreg.html Accessed: 2025-04-03"},{"key":"e_1_3_2_1_30_1","unstructured":"Georgi Georgiev. 2003. Busy Beaver prover - bbfind. https:\/\/skelet.ludost.net\/bb\/ Accessed: 2024-11-25"},{"key":"e_1_3_2_1_31_1","first-page":"1382","article-title":"Formal proof\u2013the four-color theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier. 2008. Formal proof\u2013the four-color theorem. Notices of the AMS, 55, 11 (2008), 1382\u20131393.","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_1_32_1","unstructured":"Georges Gonthier. 2023. A computer-checked proof of the Four Color Theorem."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_34_1","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier Georges","year":"2010","unstructured":"Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. Journal of formalized reasoning, 3, 2 (2010), 95\u2013152.","journal-title":"Journal of formalized reasoning"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1038\/461879a"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/583852.581501"},{"key":"e_1_3_2_1_37_1","unstructured":"Tony Guilfoyle. 2023. FAR C++ reproduction. https:\/\/github.com\/TonyGuil\/bbchallenge\/tree\/main\/FAR"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Thomas Hales Mark Adams Gertrud Bauer Tat Dat Dang John Harrison \u0141e Truong Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Tat Thang Nguyen Quang Truong Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason Rute Alexey Solovyev Thi Hoai An Ta Nam Trung Tran Thi Diep Trieu Josef Urban Ky Vu and Roland Zumkeller. 2017. A FORMAL PROOF of the Kepler CONJECTURE. Forum of Mathematics Pi 5 (2017) issn:2050-5086 https:\/\/doi.org\/10.1017\/fmp.2017.1 10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 12th Computing: The Australasian Theroy Symposium -","volume":"51","author":"Harland James","year":"2006","unstructured":"James Harland. 2006. The Busy Beaver, the Placid Platypus and other Crazy Creatures. In Proceedings of the 12th Computing: The Australasian Theroy Symposium - Volume 51 (CATS \u201906). Australian Computer Society, Inc., AUS. 79\u201386. isbn:1920682333"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.3888\/tmj.11.2-8"},{"key":"e_1_3_2_1_41_1","unstructured":"hipparcos. 2025. turing_machine. https:\/\/github.com\/jhuang97\/turing_machine"},{"key":"e_1_3_2_1_42_1","unstructured":"Iijil. 2022. Bruteforce-CTL. https:\/\/github.com\/Iijil1\/Bruteforce-CTL"},{"key":"e_1_3_2_1_43_1","unstructured":"Iijil. 2023. Finned 3 is irregular. https:\/\/discuss.bbchallenge.org\/t\/10756090-is-irregular\/137"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Iijil1. 2025. Iijil1\/MITMWFAR: v1.0.0. https:\/\/doi.org\/10.5281\/zenodo.14914502 10.5281\/zenodo.14914502","DOI":"10.5281\/zenodo.14914502"},{"key":"e_1_3_2_1_45_1","unstructured":"Owen Kellett. 2005. A multi-faceted attack on the busy beaver problem. https:\/\/homepages.hass.rpi.edu\/heuveb\/research\/BB\/downloads\/OwenThesis.pdf"},{"key":"e_1_3_2_1_46_1","unstructured":"Reinhard Kleindl. 2025. Durchbruch beim mathematischen Problem des \u201eflei\u00dfigen Bibers\u201c. Der Standard 6 Jan. https:\/\/www.derstandard.de\/story\/3000000249211\/durchbruch-beim-mathematischen-problem-des-fleissigen-bibers"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.194.4271.1235"},{"key":"e_1_3_2_1_48_1","unstructured":"Pavel Kropitz. 2023. bbc. https:\/\/github.com\/univerz\/bbc\/tree\/no1"},{"key":"e_1_3_2_1_49_1","unstructured":"Maja K\u0105dzio\u0142ka. 2023. busycoq. https:\/\/github.com\/meithecatte\/busycoq\/blob\/master\/verify\/Skelet1.v"},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of the Third Conference on Computabiliy in Europe, CiE \u201907","author":"Lafitte G","year":"2007","unstructured":"G Lafitte and C Papazian. 2007. The fabric of small Turing machines. In Computation and Logic in the Real World, Proceedings of the Third Conference on Computabiliy in Europe, CiE \u201907. Springer-Verlag, Berlin, Heidelberg. 219\u2013227. isbn:9783540730002"},{"key":"e_1_3_2_1_51_1","first-page":"3","article-title":"The 3x + 1 Problem and Its Generalizations","volume":"92","author":"Lagarias Jeffrey C.","year":"1985","unstructured":"Jeffrey C. Lagarias. 1985. The 3x + 1 Problem and Its Generalizations. The American Mathematical Monthly, 92, 1 (1985), 3\u201323. issn:00029890, 19300972 http:\/\/www.jstor.org\/stable\/2322189","journal-title":"The American Mathematical Monthly"},{"key":"e_1_3_2_1_52_1","volume-title":"\u201ccastor affair\u00e9","author":"Larousserie David","year":"2024","unstructured":"David Larousserie. 2024. Math\u00e9matiques\u00a0: le d\u00e9fi du \u201ccastor affair\u00e9\u201d r\u00e9solu. Le Monde, 17 July, https:\/\/www.lemonde.fr\/sciences\/article\/2024\/07\/17\/mathematiques-le-defi-du-castor-affaire-resolu_6251337_1650684.html"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Yijun Leng. 2025. lengyijun\/goldbach_tm: 25-state Turing machine. https:\/\/doi.org\/10.5281\/zenodo.14635917 10.5281\/zenodo.14635917","DOI":"10.5281\/zenodo.14635917"},{"key":"e_1_3_2_1_55_1","unstructured":"Shawn Ligocki. 2022. CTL Filter. Accessed: 2023-03-20"},{"key":"e_1_3_2_1_56_1","unstructured":"Shawn Ligocki. 2022. Mother of Giants. Accessed: 2025-08-10"},{"key":"e_1_3_2_1_57_1","unstructured":"Shawn Ligocki. 2023. BB(3 3) is Hard (Bigfoot). Accessed: 2025-08-10"},{"key":"e_1_3_2_1_58_1","unstructured":"Shawn Ligocki. 2023. Shift Overflow Counters. Accessed: 2025-04-04"},{"key":"e_1_3_2_1_59_1","unstructured":"Shawn Ligocki. 2023. Skelet #1 is infinite ... we think. Accessed: 2024-02-11"},{"key":"e_1_3_2_1_60_1","unstructured":"Shawn Ligocki. 2023. Skelet #1: What I Know. Accessed: 2025-04-07"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"crossref","unstructured":"Shawn Ligocki. 2023. Skelet #10: Double Fibonacci Counter. Accessed: 2025-04-07","DOI":"10.1055\/s-0045-1811508"},{"key":"e_1_3_2_1_62_1","unstructured":"Shawn Ligocki. 2024. BB(2 5) is Hard (Hydra). Accessed: 2025-08-10"},{"key":"e_1_3_2_1_63_1","unstructured":"Shawn Ligocki. 2024. BB(3 4) > Ack(14). https:\/\/www.sligocki.com\/2024\/05\/22\/bb-3-4-a14.html Accessed: 2025-08-10"},{"key":"e_1_3_2_1_64_1","unstructured":"Shawn Ligocki. 2024. BB(6) is Hard (Antihydra). Accessed: 2025-08-10"},{"key":"e_1_3_2_1_65_1","volume-title":"Computer studies of Turing machine problems. Ph. D. Dissertation","author":"Lin Shen","unstructured":"Shen Lin. 1963. Computer studies of Turing machine problems. Ph. D. Dissertation. Ohio State University, Graduate School."},{"key":"e_1_3_2_1_66_1","first-page":"247","article-title":"Attacking the Busy Beaver 5","volume":"40","author":"Marxen H.","year":"1990","unstructured":"H. Marxen and J\u00fcrgen Buntrock. 1990. Attacking the Busy Beaver 5. Bull. EATCS, 40 (1990), 247\u2013251.","journal-title":"Bull. EATCS"},{"key":"e_1_3_2_1_67_1","unstructured":"Pascal Michel. [n. d.]. The Busy Beaver Competitions. Website:. https:\/\/bbchallenge.org\/ pascal.michel\/ha.html Accessed 04-08-2025"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.05.008"},{"key":"e_1_3_2_1_69_1","unstructured":"Pascal Michel. 2022. The Busy Beaver Competition: a historical survey. arxiv:0906.3749. arxiv:0906.3749v7"},{"key":"e_1_3_2_1_70_1","unstructured":"Quanta Magazine. 2025. Amateurs Solve a Famous Computer Science Problem On Discord. YouTube video. https:\/\/www.youtube.com\/watch?v=rmx3FBPzDuk Uploaded by Quanta Magazine on YouTube;"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1962.tb00480.x"},{"key":"e_1_3_2_1_72_1","volume-title":"Proceedings of the Symposium on Mathematical Theory of Automata","author":"Rad\u00f3 Tibor","year":"1963","unstructured":"Tibor Rad\u00f3. 1963. On a simple source for non-computable functions. In Proceedings of the Symposium on Mathematical Theory of Automata (New York). Polytechnic Press of the polytechnic Institute of Brooklyn."},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","unstructured":"Redacted. 2022. bbchallenge.org https:\/\/doi.org\/10.5281\/zenodo.14955828","DOI":"10.5281\/zenodo.14955828"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","unstructured":"Redacted. 2025. Coq-BB5 release v1.0.0. https:\/\/doi.org\/10.5281\/zenodo.17061968 10.5281\/zenodo.17061968","DOI":"10.5281\/zenodo.17061968"},{"key":"e_1_3_2_1_75_1","unstructured":"Rohan Ridenour. 2024. \u201cUse decz for ZFC (636 states)\u201d. GitHub commit. Commit 6fc33bef6ba8885d26aed94c83e88bdabbedb0f1; https:\/\/github.com\/CatsAreFluffy\/metamath-turing-machines\/commit\/6fc33bef6ba8885d26aed94c83e88bdabbedb0f1"},{"key":"e_1_3_2_1_76_1","volume-title":"The Undecidability of BB(748)","author":"Riebel Johannes","unstructured":"Johannes Riebel. 2023. The Undecidability of BB(748). University of Augsburg. https:\/\/www.ingo-blechschmidt.eu\/assets\/bachelor-thesis-undecidability-bb748.pdf"},{"key":"e_1_3_2_1_77_1","unstructured":"Kyle Ross Owen Kellett Bram van Heuveln and Selmer Bringsjord. 2005. A New-Millenium Attack on the Busy Beaver Problem. https:\/\/homepages.hass.rpi.edu\/heuveb\/research\/BB\/downloads\/superpaper.pdf"},{"key":"e_1_3_2_1_78_1","unstructured":"savask. 2023. Analysis of Skelet\u2019s machine 17. https:\/\/chrisxudoesmath.com\/papers\/skelet17_savasks_analysis.pdf Accessed: 2025-04-07"},{"key":"e_1_3_2_1_79_1","unstructured":"savask. 2024. RepWL Haskell implementation. https:\/\/github.com\/savask\/turing\/blob\/main\/Repeat.hs"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"crossref","unstructured":"Tristan St\u00e9rin and Damien Woods. 2024. Hardness of\u00a0Busy Beaver Value BB(15). In Reachability Problems Laura Kov\u00e1cs and Ana Sokolova (Eds.). Springer Nature Switzerland Cham. 120\u2013137. isbn:978-3-031-72621-7","DOI":"10.1007\/978-3-031-72621-7_9"},{"key":"e_1_3_2_1_81_1","unstructured":"Tristan St\u00e9rin. 2023. FAR Python reproduction. https:\/\/github.com\/bbchallenge\/bbchallenge-deciders\/tree\/main\/decider-finite-automata-reduction-reproduction"},{"key":"e_1_3_2_1_82_1","unstructured":"Tristan St\u00e9rin. 2024. RepWL Python implementation. https:\/\/github.com\/bbchallenge\/bbchallenge-deciders\/tree\/main\/decider-repeated-word-list-reproduction"},{"key":"e_1_3_2_1_83_1","unstructured":"Terrence Tao. 2024. A pilot project in universal algebra to explore new ways to collaborate and use machine assistance? Blog:. https:\/\/terrytao.wordpress.com\/2024\/09\/25\/ Accessed: 2025-05-11"},{"key":"e_1_3_2_1_84_1","volume-title":"NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS\u201924","author":"Teodorescu Laetitia","year":"2024","unstructured":"Laetitia Teodorescu, Guillaume Baudart, Emilio Jes\u00fas Gallego Arias, and Marc Lelarge. 2024. NLIR: Natural Language Intermediate Representation for Mechanized Theorem Proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS\u201924. https:\/\/openreview.net\/forum?id=QzOc0tpdef"},{"key":"e_1_3_2_1_85_1","unstructured":"The bbchallenge Collaboration Justin Blanchard Konrad Deka Nathan Fenner Tony Guilfoyle Iijil Maja K\u0105dzio\u0142ka Pavel Kropitz Shawn Ligocki Pascal Michel Mateusz Na\u015bciszewski and Tristan St\u00e9rin. 2025. Turing machines deciders part I. arxiv:2504.20563. arxiv:2504.20563"},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant v8.20. https:\/\/doi.org\/10.5281\/zenodo.14542673 10.5281\/zenodo.14542673","DOI":"10.5281\/zenodo.14542673"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-023-06747-5"},{"key":"e_1_3_2_1_88_1","volume-title":"Busy Beaver for lambda calculus BB\u03bb. https:\/\/oeis.org\/A333479 Entry A333479 in The On-Line Encyclopedia of Integer Sequences","author":"Tromp John","unstructured":"John Tromp. 2020. Busy Beaver for lambda calculus BB\u03bb. https:\/\/oeis.org\/A333479 Entry A333479 in The On-Line Encyclopedia of Integer Sequences"},{"key":"e_1_3_2_1_89_1","unstructured":"Andrew Wade. 2025. \u201cAlignment shenanigans (ZFC \u2192 549)\u201d. GitHub commit. Commit 5d676aec074a94f598959cb3b7733a8f7781762f; https:\/\/github.com\/andrew-j-wade\/metamath-turing-machines\/commit\/5d676aec074a94f598959cb3b7733a8f7781762f"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01973619","article-title":"A classification of the ordinal recursive functions","volume":"13","author":"Wainer S. S.","year":"1970","unstructured":"S. S. Wainer. 1970. A classification of the ordinal recursive functions. Archiv f\u00fcr Mathematische Logik und Grundlagenforschung, 13, 1-2 (1970), 136\u2013153.","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"e_1_3_2_1_91_1","volume-title":"The Free Encyclopedia","unstructured":"Wikipedia. 2025. Cycle detection \u2014 Wikipedia, The Free Encyclopedia. http:\/\/en.wikipedia.org\/w\/index.php?title=Cycle%20detection&oldid=1265904359 Aaccessed: 2025-01-30"},{"key":"e_1_3_2_1_92_1","volume-title":"The Free Encyclopedia","unstructured":"Wikipedia. 2025. Zeckendorf\u2019s theorem \u2014 Wikipedia, The Free Encyclopedia. http:\/\/en.wikipedia.org\/w\/index.php?title=Zeckendorf\u2019s%20theorem&oldid=1242695626 Accessed 2025-04-07"},{"key":"e_1_3_2_1_93_1","unstructured":"Zijian Wu Suozhi Huang Zhejian Zhou Huaiyuan Ying Jiayu Wang Dahua Lin and Kai Chen. 2024. InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems. arxiv:2410.15700. arxiv:2410.15700"},{"key":"e_1_3_2_1_94_1","unstructured":"Chris Xu. 2024. Skelet #17 and the fifth Busy Beaver number. arxiv:2407.02426. arxiv:2407.02426"},{"key":"e_1_3_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.25088\/complexsystems.25.4.297"},{"key":"e_1_3_2_1_96_1","unstructured":"Daniel Yuan and Justin Blanchard. 2024. Skelet 17 is irregular. https:\/\/cosearch.bbchallenge.org\/contribution\/rgr5sxom"},{"key":"e_1_3_2_1_97_1","unstructured":"Scott Aaronson Yuri Matiyasevich Stefan O\u2019Rear. 2016. metamath - Riemann Hypothesis. \u2260wline. https:\/\/github.com\/sorear\/metamath-turing-machines\/blob\/master\/riemann-matiyasevich-aaronson.nql"}],"event":{"name":"STOC '26: 58th Annual ACM Symposium on Theory of Computing","location":"Salt Lake City UT USA","acronym":"STOC '26","sponsor":["SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 58th Annual ACM Symposium on Theory of Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3798129.3806376","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T18:03:28Z","timestamp":1781028208000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3798129.3806376"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,9]]},"references-count":97,"alternative-id":["10.1145\/3798129.3806376","10.1145\/3798129"],"URL":"https:\/\/doi.org\/10.1145\/3798129.3806376","relation":{},"subject":[],"published":{"date-parts":[[2026,6,9]]},"assertion":[{"value":"2026-06-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}