Context: DeepMind released Turing machines for which the termination is equivalent to various conjectures being true/false. The equivalence is certified in Lean, and they also improved the minimum number of states required to encode certain theorems, e.g. Goldbach is now down to 21!!
1 comment
[ 1.0 ms ] story [ 26.8 ms ] threadVery relevant to the discussion people had a few days ago on why busy beaver numbers are interesting https://news.ycombinator.com/item?id=50070741