Matematikçi Terry Tao, geleneksel derin problemlerin yanı sıra, geniş bir matematik topluluğuyla daha geniş ilgi alanlarına sahip problemler üzerinde çalışmanın tamamlayıcı bir yol olduğuna inanıyor. Modern teknolojilerin ve yapay zekanın bu tür iş akışlarına daha uygun olduğunu düşünen Tao, daha önce "Polymath projeleri" ve işbirlikçi formalizasyon projeleri gibi girişimlere öncülük etmişti. 2024 yılında başlattığı Equational Theories Project (ETP) ile Lean formalizasyonunun titizliğini otomatik teorem ispatlayıcılar (eski usul yapay zeka) ile birleştirerek evrensel cebirdeki 22 milyondan fazla doğru-yanlış problemini resmi doğrulama ile çözmeyi başardı.
Bu ruhla devam eden Terry Tao ve Damek Davis, SAIR Vakfı'nın ev sahipliğinde deneysel bir rekabetçi meydan okuma başlatıyor. Honda, Murakami ve Zhang'ın yakın tarihli bir makalesinden esinlenen bu "Matematik Damıtma Yarışması"nın temel amacı, ETP tarafından elde edilen 22 milyon evrensel cebir doğru-yanlış sonucunun ne ölçüde kısa, insan tarafından okunabilir bir "kopya kağıdına" damıtılabileceğini ölçmek. Bu fikir, bir lisans matematik öğrencisinin bir sınavda kullanmasına izin verilen tek sayfalık bir özet oluşturmasına benziyor.
ETP'nin çözdüğü tipik bir problem, ikili bir işlemin belirli bir denklemi sağlayıp sağlamadığını sorgulamak gibi evrensel cebir problemlerini içeriyor. Bu tür problemler cebirsel manipülasyonla veya karşı örnek bularak çözülebilir ve bazı durumlarda karar verilemez nitelikte olabilir. İnsanlar, otomatik teorem ispatlayıcılar veya gelişmiş yapay zeka sistemleri bu problemleri çözebilirken, bu yapay zeka modelleri pahalıdır ve cevaplarının nereden geldiğine dair fazla içgörü sunmazlar. Daha küçük ve ucuz açık kaynak modeller ise rastgele şanstan daha iyi performans gösterememektedir. Bu yarışma, bu büyük veri setinden anlamlı ve özetlenebilir bilgiyi çıkarmayı hedefliyor.
Bu proje, yapay zeka destekli matematiksel keşiflerin sonuçlarını insan tarafından anlaşılabilir, özlü bilgilere dönüştürme potansiyelini ve zorluklarını ortaya koyuyor.