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!!

Very relevant to the discussion people had a few days ago on why busy beaver numbers are interesting https://news.ycombinator.com/item?id=50070741