Здравствуйте, vsb, Вы писали:

vsb>Смысл хотя бы в том, чтобы проверка и принятие доказательств новых теорем занимала миллисекунды, а не годы, как это иногда бывает.
А не пришлось бы для действительно новых теорем каждый раз прикручивать новые расширения к языку? Отлаживать и тестировать машину вывода, видимо на примере этой самой новой теоремы