30 октября 2015 · Комментарий

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

Имя не сохранено · Оригинал в ЖЖ ↗ · Ссылка на запись

А вот интересно, никто не додумался загрузить в какую-нибудь сетку все теории, написанные на каком-нибудь языка формальной математики (Coq/Agda/Isabelle), запускать проверятель определений и доказательств на выданном сеткой и скармливать результат запуска ей на вход в качестве обратной связи, получится автоматический учитель.