Дослідники з Массачусетського технологічного інституту (MIT) здобули значний грант від Renaissance Philanthropy та XTX Markets для розробки систем штучного інтелекту, що сприятимуть математичним відкриттям. Ця ініціатива об'єднує активи баз даних LMFDB та mathlib з метою автоматизації теорем та полегшення їх перевірки.

Інтеграція баз даних для математичних інновацій
Проект під керівництвом дослідників Ро та Сазерленда з MIT має на меті об'єднати LMFDB, великий онлайн-ресурс сучасної теорії чисел, з mathlib — бібліотекою для формальної перевірки математичних теорем. Це з'єднання надасть математичній спільноті та AI системам доступ до вже наявних даних, полегшуючи розв'язання складних задач та формалізацію нових теорем.
Сьогодні автоматизовані системи доведення теорем стикаються з проблемами, такими як обмеженість формалізованих знань і висока вартість формалізації складних результатів. Новий підхід передбачає використання вже існуючих обчислювальних результатів, що зекономить час та ресурси, зменшуючи потребу у повторних обчисленнях.
Майбутнє математичних досліджень
У рамках проекту команди MIT планують розвивати інструменти для доступу до LMFDB з mathlib, що дозволить AI асистентам швидше ідентифікувати цілі для формалізації. Це не тільки розширить можливості математичних досліджень, але й зменшить розрив між теоретичними знаннями і практичною реалізацією.
Проект відкриває нові горизонти для математиків та дослідників, надаючи їм інструменти для роботи над складними задачами з меншими витратами зусиль. Зацікавлені студенти MIT мають можливість приєднатися до команди, щоб долучитися до формування майбутнього математичних досліджень.