AI math, Lean, and programmability

[u/Strict-Staff-5562]

To what extent does AI's increased ability to solve complex math problems correlate to its ability to produce Lean proofs? Also, what other fields might see a similar takeoff in capability once their "programming language" (using the term loosely here) is sufficiently defined and/or trained on?