Баззард точно не Риэль и не жулик, а аспирант Тейлора и крепкий профессионал с премией Уайтхеда в активе (хотя и не звезда). Естественно, ему было интересно научить LEAN определению перфектоида, он же арифметической геометрией занимался (и при чем тут "главное в мире"). Если я правильно помню, геометрии Аракелова он тоже LEAN учил.

Польза от proof assistant я уже написал, какая может быть: научить студента, чем доказательство отличается от галлюцинаций, которые он за доказательства обычно принимает на первом курсе (или на первом году обучения в матшколе). Сейчас (или даже не "сейчас", а сколько-то лет назад: посмотреть на LEAN у меня руки все не доходят) оно для таких целей неприменимо, из-за безумного количества утомительных деталей, которые нужно объяснять тупому устройству.

Если же эту боль удастся/удалось преодолеть (чтобы тупое устройство само заклеивало тупые детали), это решит часть утомительной проблемы, о которой пишет Михаил в комментарии по теории Галуа: не знаю, что там пишут ему, но по крайней мере, у них не получится никак запихнуть в assistant жульническое вычисление группы Галуа кругового поля в обход неприводимости многочлена.

Ну и для научения матлогике тоже нелишнее (наверное; я из матлогики знаю только нумерацию Г. и немножко форсинга).