Beaucoup d'entre nous ressentent intuitivement que le domaine des mathématiques va changer, alors déballons les résultats probables, sans recourir à l'hyperbole ou au catastrophisme.

Hypothèse n°1 : Le nombre de preuves mathématiques et la quantité totale de données mathématiques vont s'accroître de manière exponentielle. Celle-ci est peut-être peu controversée. Les modèles d'IA, sous la direction des humains, créent déjà d'énormes quantités de mathématiques. Maintenant, le goulot d'étranglement est passé de la création de mathématiques à la vérification de leur exactitude. Aristote, qui utilise @leanprover, résout le problème de vérification en permettant à chaque preuve d'être vérifiable par machine. À mesure que la technologie s'améliore, la longueur et la complexité des preuves créées continueront d'augmenter.

Hypothèse n°2. Il y aura dramatiquement plus de mathématiciens dans 10 ans qu'il n'y en a aujourd'hui. En automatisant la corvée de vérification et en prouvant des lemmes simples, Aristote peut non seulement accélérer le travail de mathématiciens professionnels hautement sophistiqués, mais aussi abaisser la barrière à l'entrée pour que d'autres puissent contribuer. Parmi nos utilisateurs de l'API bêta, on trouve des ingénieurs logiciels à la retraite, des avocats, des membres de l'armée, des étudiants et plein d'autres personnes qui ont des idées / ingéniosité mathématiques mais qui ont besoin d'aide avec le formalisme et ont besoin de quelqu'un pour vérifier leurs idées. Nous devrions nous attendre à ce que ces tendances s'accélèrent.

Hypothèse n°3. Les humains resteront au centre de la recherche en mathématiques. C'est le point crucial. Si nous regardons en arrière à travers l'histoire -- nous avons toujours changé la définition des mathématiques pour qu'elle corresponde à ce que les machines ne peuvent pas automatiser. Une grande partie du travail d'un mathématicien au début des années 1800 consistait à résoudre des équations. Mais les premières calculatrices ont automatisé une grande partie de ce travail de routine, libérant ainsi les mathématiciens pour qu'ils puissent faire un travail plus créatif / abstrait. Pour un avenir prévisible, nous croyons que l'IA sera la même chose. Les mathématiciens passeront moins de temps à vérifier la justesse et à prouver des lemmes simples, et des outils comme Aristote les aideront à consacrer leur temps à explorer des concepts plus profonds. Finalement, à mesure qu'Aristote devient plus capable, les mathématiciens dirigeront Aristote et ce sera comme avoir une équipe de collaborateurs mathématiques extrêmement talentueux et rigoureux à votre disposition, où vous pouvez les orienter dans différentes directions et ils peuvent explorer les frontières mathématiques. Quoi qu'il en soit, nous avons dépassé la phase du tableau noir et du canapé en mathématiques. C'est maintenant entièrement numérique, collaboratif et habilité par l'IA.