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

Гипотеза #1: Количество математических доказательств и совокупный объем математических данных будут расти экспоненциально. Это, возможно, не вызывает споров. Модели ИИ, под руководством людей, уже создают огромные объемы математики. Теперь узким местом стало не создание математики, а проверка ее правильности. Aristotle, который использует @leanprover, решает проблему верификации, позволяя каждому доказательству быть проверяемым машиной. По мере улучшения технологий длина и сложность создаваемых доказательств будут продолжать увеличиваться.

Гипотеза #2. Через 10 лет математиков будет значительно больше, чем сегодня. Автоматизируя рутинную работу по проверке и доказательству простых лемм, Aristotle может не только ускорить работу высококвалифицированных профессиональных математиков, но и снизить барьер для других, чтобы они могли внести свой вклад. Среди наших пользователей бета-API есть пенсионеры-программисты, юристы, военнослужащие, студенты и множество других людей, у которых есть математические идеи / изобретательность, но которым нужна помощь с формализмом и кто нуждается в ком-то, чтобы проверить их идеи. Мы должны ожидать, что эти тенденции будут ускоряться.

Гипотеза #3. Люди останутся в центре математических исследований. Это самое важное. Если мы оглянемся на историю, мы всегда изменяли определение математики так, чтобы оно соответствовало тому, что машины не могут автоматизировать. Большая часть работы математика в начале 1800-х годов заключалась в решении уравнений. Но ранние калькуляторы автоматизировали большую часть этой рутинной работы, освобождая математикам время для более творческой / абстрактной работы. В обозримом будущем мы считаем, что ИИ будет таким же. Математики будут тратить меньше времени на проверку правильности и доказательство простых лемм, а такие инструменты, как Аристотель, помогут им сосредоточить свое время на исследовании более глубоких концепций. В конечном итоге, по мере того как Аристотель станет более способным, математики будут управлять Аристотелем, и это будет похоже на то, что у вас есть команда чрезвычайно талантливых и строгих математических сотрудников под рукой, которым вы можете указывать разные направления, и они могут исследовать математические границы. В любом случае, мы уже прошли стадию меловой доски и дивана в математике. Теперь это полностью цифровое, совместное и поддерживаемое ИИ.