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

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