"на очень высокопрофессиональном уровне" - в этой области не трудятся ли где-либо студенты / аспиранты в плане формализации на Lean? Хороший язык, кстати - я зашёл на отчётный семинар в местном университете (UW), там уже несколько лет действует группа со сменяющимся составом (студентов, постградов), формализуют нетривиальные теоремы. Наткнувшись на первые места расползания - в процессе формализации доказательства - можно получить весомый аргумент, что доказательство отсутствует. Далее, насколько я понимаю, есть группа лиц, уверенных в состоятельности доказательства (один из них вроде в Питере, я поищу общих знакомых, обсудить). Для этих лиц такая аргументация может оказаться убедительной (если с самим автором доказательства общаться смысла нет).