Код креативности. Как искусственный интеллект учится писать, рисовать и думать

reserve n, p for Nat;

theorem Euclid: ex p st p is prime & p > n proof

set k = n! + 1;

n! > 0 by NEWTON:23;

then n! >= 0 + 1 by NAT1:38; then k >= 1 + 1 by

REAL1:55;

then consider p such that

A1: p is prime & p divides k by INT2:48; A2: p <> 0 & p > 1

by A1, INT2: def 5; take p;

thus p is prime by A1;

assume p <= n;

then p divides n! by A2, NATLAT:16;

then p divides 1 by A1, NAT1:57;

hence contradiction by A2, NAT1:54;

end;

theorem p: p is prime is infinite

from Unbounded(Euclid).

Совершенно невразумительно даже для меня, профессионального математика! Это ни в коей мере не соответствует тому, как рассказывал бы эту историю любой человек. В некотором смысле тут возникает проблема языкового барьера.

Если можно создать алгоритмы, переводящие с испанского на английский, нельзя ли найти способ перевода с компьютерного языка на тот язык, которым излагают доказательства люди? Исследовать этот вопрос взялись два кембриджских математика, Тимоти Гауэрс и Мохан Ганесалингам. Гауэрс впервые приобрел широкую известность в 1998 году, когда он получил Филдсовскую премию, и в том же году стал профессором кафедры имени Роуза Болла.

Ганесалингам сначала шел по похожему пути: он изучал математику в кембриджском Тринити-колледже. Однако, после того как он был выбран лучшим на своем курсе («старшим ранглером») и получил одну из высших студенческих наград, он решил сменить род занятий и, к удивлению всего своего факультета, получил магистерскую степень по англосаксонскому английскому. Получив награду за лучшие результаты на кембриджском факультете английской филологии, он поступил в аспирантуру по информатике, в которой занимался анализом математического языка с точки зрения формальной лингвистики. Вскоре этому сочетанию математики и лингвистики нашлось практическое применение. Гауэрс и Ганесалингам познакомились в Тринити-колледже и вскоре поняли, что их обоих интересует вопрос о непроницаемости компьютерного языка. Они решили объединить свои усилия, чтобы создать инструмент для разработки компьютерных доказательств, которые смогут читать люди.