[non_aligned]

The research into BB numbers is purely academic and unlikely to be more than that, unless some other part of mathematics turns out to be wrong. Our current understanding is that the numbers are essentially guaranteed to be useless.

This particular proof is doubly-academic in the sense that the value was already known, this is just a way to make it easier to independently verify the result.

It's a part of a broader movement to provide machine proofs for other stuff (e.g., Fermat's last theorem), which may be beneficial in some ways (e.g., identifying issues, making parts of proofs more "reusable").

[cwillu]

I'm going to push back on “the value was already known”; my understanding is that the candidate value was known, but while there was a single machine with behaviour that was not yet characterized, it quite easily could have been the real champion.

[non_aligned]

Ah yeah, I stand corrected. I didn't realize this is a paper by the original team that found the number a while back, I thought it's an independent formalization in 2025.