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

Давайте я на всякий случай переформулирую свое предложение, дабы устранить всякие недоразумения. У нас есть совокупность людей, которая генерирует теории на языке Coq (выбираем его, потому что у меня создалось впечатление, что больше всего теорий написанно именно на этом языке). Таким образом, мы имеем некий мегаинтеллект, продуцирующий теории на Coq, которые ему по каким-то причинам интересны. Мы берем сеть, которая делает то же, что и этот мегаинтеллект -- генерирует интересные теории на Coq. Далее. Некоторые из них пройдут проверку, если их засунуть в Coq, а а на некоторых он будет выдавать сообщение об ошибке. Мы запускаем ферму, на ней запускаем выдающую теории сеть, ее выход подаем на проверятель, и в зависимости от исхода проверки поощряем или наказываем сеть. В результате сеть изменяет себя таким образом, что процент ее теорий, который проходит проверку, становится все больше и больше. Тут выход сети становится интересен -- в плане свежих идей, до которых не дает добраться сложившаяся культура. Но можно пойти еще дальше -- заставить сеть генерить теории, начинающиеся с данного префикса -- в который мы засовываем формулировку открытой проблемы. Все ее выходы с данным префиксом, прошедшие проверку проверятелем, будут решениями открытой проблемы.