large formal math dataset by Numina

Stream: Machine Learning for Theorem Proving

[fzyzcjy]

News seen just now: Numina (funded by XTX Markets) will create a large formal math dataset consisting of 1 million questions and answers.

Source: https://mathstodon.xyz/@tao/113669121621914558 (linked to https://www.businesswire.com/news/home/20241217062574/en/Project-Numina-Receives-%E2%82%AC3m-Research-Grant-From-XTX-Markets)

[Jason Rute]

Also discussed here: #general > Numina 3mil XTX grant to make 1 million formal problems

[fzyzcjy]

Thanks for the link!

[fzyzcjy]

So... should I remove this thread to avoid duplication, or leave it here for people who subscribed ML4TP but not General channel to know the news?

[Jason Rute]

I think leave it up. Threads in #general get buried quickly. You probably are not the first interested party who missed it.

[Jason Rute]

Also, there is this thread about the large prize pool (which I assume is yet to be rewarded). #general > AI for Math fund