Interview with MPIM Director Peter Scholze.
(P.Scholzeの懸念) 14分すぎ頃から

what role do you think
proof assistants such as
Lean will play in the future?

https://m.youtube.com/watch?v=_gAe77G_aHw&ra=m