I am not really sure. The models can be bootstrapped to become much better at both natural language generation and verification for sure and my hypothesis is that the current days models would have been just as good at math without Lean.