Muitos de nós sentimos intuitivamente que o campo da matemática vai mudar, então vamos analisar os resultados prováveis, sem recorrer a hipérboles ou pessimismo.

Hipótese #1: O número de provas matemáticas e a quantidade agregada de dados matemáticos vão se expandir exponencialmente. Essa talvez não seja controversa. Modelos de IA, sob a direção humana, já estão criando grandes quantidades de matemática. Agora, o gargalo passou de criar matemática para verificar sua correção. Aristóteles, que usa @leanprover, resolve o problema de verificação ao permitir que cada prova seja verificável por máquinas. À medida que a tecnologia avança, o comprimento e a complexidade das provas criadas continuarão a aumentar.

Hipótese #2. Haverá dramaticamente mais matemáticos em 10 anos do que hoje. Ao automatizar a monotonia da verificação e provar lemas simples, Aristóteles pode não apenas acelerar o trabalho de matemáticos profissionais altamente sofisticados, mas também diminuir a barreira de entrada para que outros contribuam. Entre nossos usuários beta da API estão engenheiros de software aposentados, advogados, militares, estudantes e muitas outras pessoas que têm ideias/engenhosidade matemática, mas precisam de ajuda com o formalismo e alguém para verificar suas ideias. Devemos esperar que essas tendências se acelerem.

Hipótese #3. Os humanos permanecerão no centro da pesquisa matemática. Essa é a grande questão. Se olharmos para trás ao longo da história — sempre mudamos a definição de matemática para ser aquilo que as máquinas não podem automatizar. Uma grande parte do trabalho de um matemático no início dos anos 1800 era resolver equações. Mas as primeiras calculadoras automatizaram grande parte desse trabalho rotineiro, liberando matemáticos para fazerem trabalhos mais criativos e abstratos. No futuro próximo, acreditamos que a IA será a mesma. Matemáticos gastarão menos tempo verificando a correção e provando lemas simples, e ferramentas como Aristóteles os ajudarão a dedicar seu tempo a explorar conceitos mais profundos. Eventualmente, à medida que Aristóteles se torna mais capaz, os matemáticos estarão conduzindo Aristóteles e será como ter uma equipe de colaboradores matemáticos extremamente talentosos e rigorosos à sua disposição, onde você pode apontá-los para diferentes direções e eles podem explorar as fronteiras matemáticas. De qualquer forma, já passamos da fase de quadro-negro e sofá da matemática. Agora é totalmente digital, colaborativo e habilitado por IA.