я про него ничего не знаю,
но на mathjobrumors.com после любого
упоминания Баззарда юзеры ритуально посылают его нахуй
собственно, я только в этом качестве о нем и слышал,
типа "гафурка значит нахуй"

видимо, очень известный математик

>формализованную библиотеку всего накопленного
>математического знания,

это очень полезно, конечно,
вот например stacks project
https://stacks.math.columbia.edu/
написано хуже некуда, но многие учебники
такие же плохие, а так полезно, и при желании
вбивается в любой формальный фреймворк

в принципе, из этого формального фреймворка (когда он будет)
можно много полезного впоследствии вытащить, типа проверочных
механизмов, а то когда люди кидаются говном насчет "это доказательство
верное", "это доказательство неверное", пусть будет какой-то способ
решения ситуации, кроме спасительной эвтаназии всех участников