Lean plus AI is a winning combo: Lean is super precise but "narrow", AI is broad but lacks precision.

Before AI it was super tedious to formally express your software models in Lean, with AI this is super easy. See formal verification of consensus core in Ultima Cluster: https://github.com/PeterKnego/ultima_cluster/blob/main/docs/...