Багато хто з нас інтуїтивно відчуває, що галузь математики зміниться, тож давайте розглянемо ймовірні результати, не вдаючись до гіперболи чи думеризму.

Гіпотеза #1: Кількість математичних доказів і сукупна кількість математичних даних зростуть експоненційно. Це, можливо, не викликає суперечок. Моделі штучного інтелекту під керівництвом людей вже створюють величезні обсяги математики. Тепер вузьке місце перейшло від створення математики до перевірки її коректності. Арістотель, який використовує @leanprover, розв'язує проблему верифікації, дозволяючи кожне доведення бути машинно перевіряним. Зі вдосконаленням технології довжина та складність створених доказів продовжуватимуть зростати.

Гіпотеза #2. За 10 років математиків буде значно більше, ніж сьогодні. Автоматизуючи рутину верифікації та доводячи прості леми, Арістотель не лише прискорює роботу висококваліфікованих професійних математиків, а й знижує бар'єр для входу інших. Серед користувачів наших бета-API — пенсіонер-програмісти, юристи, військовослужбовці, студенти та багато інших людей, які мають математичні ідеї та винахідливість, але потребують допомоги з формалізмом і перевірку їхніх ідей. Слід очікувати, що ці тенденції прискоряться.

Гіпотеза #3. Люди залишаться в центрі математичних досліджень. Це найголовніше. Якщо озирнутися назад — ми завжди змінювали визначення математики на те, що машини не можуть автоматизувати. Велика частина роботи математика на початку 1800-х років полягала у розв'язанні рівнянь. Але ранні калькулятори автоматизували значну частину цієї рутинної роботи, звільнивши математиків для більш творчої та абстрактної роботи. У найближчому майбутньому ми віримо, що ШІ залишиться таким самим. Математики витрачатимуть менше часу на перевірку правильності та доведення простих лем, а інструменти на кшталт Арістотеля допоможуть їм присвятити час глибшому вивченню концепцій. Зрештою, коли Арістотель стане більш здібним, математики будуть керувати ним, і це буде як мати команду надзвичайно талановитих і ретельних математичних співробітників, де ви зможете вказати їм різні напрямки, і вони досліджуватимуть математичні горизонти. У будь-якому разі, ми вже пройшли фазу «дошка і диван» у математиці. Зараз він повністю цифровий, колаборативний і з підтримкою штучного інтелекту.