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