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










