Без заголовка

на самом деле даже из первого пункта уже много можно извлечь: 1) нанимаем гениального архитектора сетей, который придумывает мудрую архитектуру 2) реализуем сеть 3) скармливаем сети все coq-файлы, которые удается найти в интернете 4) закорачиваем фидбек пруфчекера на вход сети, чтобы она училась выдавать только корректные теории 5) формулируем открытую проблему в виде теоремы и подаем сети для продолжения (понятия не имею, как это сделать) 6) любая корректная теория, выданная сетью, будет корректным формальным доказательством сформулированной проблемы, не важно насколько распухшим, нечитаемым и использующим непостижимые нечеловеческие тактики доказательств оно будет