Американский математик Томас Хэйлс (Thomas Hales, University of Pittsburgh) при сотрудничестве с учеными из корпорации Intel разрабатывает пакет компьютерных программ, которые смогут проверять корректность математических доказательств. Сегодня математики излагают свои доказательства в описательной форме. Ученые опираются на существующие результаты и опускают шаги рассуждений, которые кажутся им очевидными. Такая форма наиболее адекватна для восприятия доказательства человеком. Если выписывать все шаги от аксиом до нового результата, доказательство окажется крайне громоздким, и другие математики не смогут его разобрать. Но иногда через много лет оказывается, что доказательство содержит формальные ошибки. Томас Хэйлс предложил выписывать математическое доказательство в чисто формальном виде и поручать его проверку компьютеру. Он считает, что подобный подход приведет к облегчению труда математика и позволит получать полностью корректные результаты. По оценке ученого, такой пакет программ удастся создать в ближайшие годы.