jeff87654/busy-beaver

Busy beaver machines with axiom-free Coq proofs: BB(7) σ > 3↑²⁰3, BB(8) > f_ω³(12), BB(9) > f_ω⁷(12), BB(10) f_(ω+1), BB(12) f_(ω+1)², BB(13)/BB(14) f_(ω+2), BB(4,3). Plus Turing machines that halt iff ZF/ZFC (253 states), ZFC + universes (296) or PA (238) is inconsistent, and one (449) that halts iff PA proves Goldbach's conjecture.

68 best points · 75 comments · 1 Hacker News post · 15 GitHub stars · View on GitHub

Hacker News discussions

• BB(10) > Graham's Number (68 points, 75 comments, by surprisetalk, 2026-10-13)