Yeah ok when you put it as a bet I think I'll back down ha ha :)

I imagine there will be hold outs who will never switch to formal proofs, though they may simply take on co-authors who are just "formalizers".

I also am probably being over confident with the time scales, I think a process with a tipping point, everyone will use it once everyone starts using it.

However when that tipping point will occur is probably hard to predict. I think it will be soon, but I'm broke and not that sure.