Американский математик Томас Хэйлс при сотрудничестве с учеными из корпорации Intel разрабатывает пакет компьютерных программ, которые смогут проверять корректность математических доказательств.
Сегодня математики излагают свои доказательства в описательной форме. Ученые опираются на существующие результаты и опускают шаги рассуждений, которые кажутся им очевидными.
Такая форма наиболее адекватна для восприятия доказательства человеком. Если выписывать все шаги от аксиом до нового результата, доказательство окажется крайне громоздким, и другие математики не смогут его разобрать. Но иногда через много лет оказывается, что доказательство содержит формальные ошибки. Томас Хэйлс предложил выписывать математическое доказательство в чисто формальном виде и поручать его проверку компьютеру.
Он считает, что подобный подход приведет к облегчению труда математика и позволит получать полностью корректные результаты. По оценке ученого, такой пакет программ удастся создать в ближайшие годы.
новости по теме
Бактерии умеют решать математические задачи. В Journal of Biological Engineering опубликовано исследование, согласно которому "живой" компьютер из бактерий E. coli, способен решать сложные математические задачи поиска гамильтонова пути в графе.
Роспотребнадзор снова проверит молдавские вина. Роспотребнадзор еще раз проверит молдавские вина, поставленные в Россию. В зависимости от результатов проверки стороны обсудят возможности возврата молдавских вин на прилавки российских магазинов,
Гаишники проверят стиль вождения Михалкова. Московское управление ГИБДД проверит опубликованную в интернете видеозапись, на которой видно, как автомобиль режиссера Никиты Михалкова выезжает на встречную полосу движения.
Американский математик Томас Хэйлс при сотрудничестве с учеными из корпорации Intel разрабатывает пакет компьютерных программ, которые смогут проверять корректность математических доказательств. 
