私見だが
早く Leanによる形式化の詳細を公開して
みんなで議論して、早く前進させた方が良いと思う

ある方法がだめでも
おうおうにして
別の手段があるものです