Журнал Компьютерра -759   ::   Компьютерра

В последние

годы программы проверки доказательств стали достаточно мощными, чтобы справляться со сложными теоремами. К сожалению,

формальная запись доказательства пока получается примерно в четыре раза длиннее обычной и требует примерно неделю

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

этим заниматься. Тем более что славы проверка известных теорем не приносит. Впрочем, программы совершенствуются, и,

возможно, в недалеком будущем запись формального доказательства станет не намного труднее записи обычного. А редакции

математических журналов не станут рассматривать статьи без приложения формальных записей сформулированных в них

теорем.

Сегодня имеется около двух десятков пакетов для проверки доказательств, пять из которых особенно

популярны. С их помощью в общей сложности проверено восемь десятков теорем - капля в море математики. Но пока эта

деятельность лишь удел небольших групп специалистов, и не все математики одобряют эту работу. Тем не менее авторы

обзоров призывают специалистов и энтузиастов присоединяться к процессу формализации доказательств, чтобы сделать

математику еще более надежной основой науки. ГА

Новый суд по старому вопросу



В конце

октября медиахолдинг ВГТРК подал несколько исков, связанных с защитой своих авторских прав. Ответчиками по ним являются

крупнейшая российская интернет-компания Mail.