The AI for Math Fund, sponsored by Renaissance Philanthropy and XTX Markets, is a grant opportunity committing $9.2 million to research, field-building and development of open-source tools and datasets in the intersection of AI and mathematics. Projects related to AI automation for proof assistants (including HOL) are encouraged to apply.
Links: AI for Math Fund announcement <https://renaissancephilanthropy.org/news-and-insights/renaissance-philanthropy-and-xtx-markets-launch-new-9-million-ai-for-math-fund/> AI for Math Fund website <https://renaissancephilanthropy.org/initiatives/ai-for-math-fund/> Bloomberg article on AI for Math Fund <https://www.bnnbloomberg.ca/business/technology/2024/12/05/billionaire-gerkos-xtx-gives-millions-to-make-ai-better-at-math/> Terence Tao's blog post on AI for Math Fund <https://terrytao.wordpress.com/2024/12/05/ai-for-math-fund/> Please submit a brief application via webform <https://airtable.com/appSh677zJHNiCdW7/pagSeCrgvihcU6dha/form> by *January 10, 2025.* Successful applicants will be invited to submit full proposals.
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info