
@TaliaRinger's article: https://www.ams.org/journals/notices/202409/noti3032/noti3032.html
Users are excited about Lean Prover's growing role in mathematics because it enables open collaboration like Terry Tao accepting GitHub pull requests and shows the outsized impact of informal coffee chats on research.

@TaliaRinger's article: https://www.ams.org/journals/notices/202409/noti3032/noti3032.html

Sometimes those informal coffee chats are more impactful than any publication you could write, any theorem you could prove, any tool you could build. But the informal moments get lost in history while the rest are preserved. They're cool and worth remembering

@KSHartnett @TaliaRinger Terry Tao accepting pull requests from anyone on GitHub. That sentence would have been incomprehensible a decade ago. The tool changes not just what we can prove but how we organize ourselves to prove it.