[Перевод] Насколько близко компьютеры подошли к автоматическому построению математических рассуждений?

Лучшие публикации за сутки.

Инструментарий искусственного интеллекта определяет форму автоматических доказывателей теорем нового поколения, а вместе с этим – и взаимоотношения математики и машин

Говорят, что в 1970-е годы ныне почивший математик Пол Джозеф Коэн, единственный лауреат Филдсовской премии за работы по математической логике, сделал огульное предсказание, которое до сих пор продолжает как восторгать, так и раздражать математиков: «когда-нибудь в будущем математиков заменят компьютеры». Коэн, известный дерзостью методов в работе с теорией множеств, предсказал, что можно автоматизировать всю математику, включая и написание доказательств.

Доказательство – это пошаговая логическая аргументация, подтверждающая истинность гипотезы или математического предположения. После появления доказательства гипотеза становится теоремой. Оно как подтверждает правильность утверждения, так и объясняет, почему оно верно. Но доказательство – штука странная. Оно абстрактно, и не привязано к материальному опыту. «Они представляют собой результат безумного контакта между вымышленным, не физическим миром, и существами, появившимися в результате биологической эволюции», — сказал когнитивист Саймон Дедео из университета Карнеги-Меллона, изучающий математическую определённость через анализ структур доказательств. «К этому нас эволюция не готовила».
Читать дальше →

Добавить комментарий

Ваш адрес email не будет опубликован.