原创 AIforMathFund zzllrr小乐
近日，AI for Math Fund数学人工智能基金成立，这是由美国文艺复兴慈善（Renaissance Philanthropy） 和 XTX Markets（英国量化交易巨头XTX）发起的一项新的资助项目。该基金将投入920 万美元支持新AI人工智能工具的开发，这些工具将作为推进数学发展的长期基石。基金面向全球个人和团队开放，个人资助最多可达100万美元，用于长达 24 个月的开源项目和研究工作。
一、项目背景简介
挑战与机遇
形式验证——所谓的“自动定理证明”——允许计算机严格验证证明的正确性，或者更广泛地“证明”任何计算机程序的正确性。不幸的是，除了形式验证研究人员之外，很少有人使用这些工具，因为它们非常麻烦且劳动密集型。基于人工智能的自动化工具正在改变这种情况，这些工具越来越多地使数学家可以使用正式的验证框架，从而实现新形式的大规模数学协作。一旦自动化、可用的形式验证工具成为现实，我们将有能力自动生成和验证数学上严格的命题，从而实现数学知识的巨大扩展，同时使人工智能和软件更加可靠。
产业实验室和学术研究人员在数学人工智能领域取得了越来越多令人兴奋的成果。然而，使整个领域受益的开源项目却受到产业和传统学术资助者的资助不足。尽管美国国家科学基金会在人工智能和数学交叉领域有一个规模不大的项目（每年600万美元），但增加支持可以加快数学发现的速度和影响。
慈善事业可以通过支持以下项目来产生巨大的反事实影响：(1) 在一切按部就班的情况下不太可能发生；(2) 有潜力推动整个领域的发展。其中包括：开发开源的、生产级质量的工具；增加训练人工智能模型所需的数据集的规模、多样性和质量；提高工具的易用性，以便它们被数学家采用。
战略
越来越多的研究人员，包括一些世界领先的数学家，相信未来的数学将在人工智能工具的帮助下被发现和研究。数学人工智能基金致力于创造对数学家有价值的人工智能技术，并扩大其在全球数学界的应用。
通过RFP申报单和公开征集申请，人工智能数学基金将支持四个方面的项目：开源工具、变革性数据集、突破和领域建设。
项目可以由来自学术机构、商业组织或独立项目的申请人领导，只要所有工作都是开源的并公开共享，并且与任何营利性公司的常规活动分开。典型的申请人应在形式验证、人工智能和相关领域拥有良好的成就记录。
1. 生产级软件工具
数学人工智能基金将支持在人工智能和数学交叉领域开发开源、高品质软件工具的项目，例如：
基于人工智能的自动形式化工具，将自然语言数学转化为证明助手的形式主义
基于人工智能的自动信息化工具，将机器辅助证明转化为可解释的自然语言数学
将证明助手与计算机代数系统CAS、微积分和偏微分方程连接起来的基础设施
面向数学家的大规模人工智能增强分布式协作平台
2. 数据集
数学人工智能基金将支持生成用于训练人工智能模型的开源数据集的项目，例如：
证明助手中的形式化定理和证明的数据集
数据集将推动人工智能定理证明应用于程序验证和安全代码生成
（自然语言）数学问题、定理、证明、论证等的数据集。
3. 领域建设
数学人工智能基金将支持发展数学人工智能领域的项目，例如：
教科书
课程
对证明助手以及与 AI 工具集成的接口/API 的文档和支持
4.突破性的想法
数学人工智能基金将支持一些将人工智能应用于基础数学和应用的高风险、高回报的想法，例如：
预期难度估计（证明的子问题）
形式化类型理论证明的新颖数学含义
证明助手中证明复杂度的形式化
二、人工智能数学基金详情
基金项目官网
基金使用详情
个人资助：最多100 万美元，用于长达24个月的开源项目和研究工作
向全球个人和团队开放
请阅读申报单和申报说明了解更多信息。
申请截止日期
申请资格
申请人应在形式验证、人工智能、证明助理或数学方面拥有深厚的背景和可追踪的成就记录
拟议项目推动数学人工智能领域及其应用的潜力
传统融资机制忽视的拟议项目
地理限制
申请向美国和世界各地的居民开放，但以下地区的居民除外：
克里米亚
所谓的顿涅茨克人民共和国 (DNR)
所谓的卢甘斯克人民共和国 (LNR)
古巴
伊朗
叙利亚
朝鲜
或任何受到美国出口管制或美国、英国或欧盟制裁的人。
申请流程
选定的申请人提交完整的提案。
如果您的申请通过了第一轮筛选，您将被邀请提交更详细的书面提案，以供我们的顾问进一步评估。
如果您提议的项目是在一家营利性公司内进行的，则需要额外的文件要求，说明该工作是一个开源、免费、面向公众的项目，而在正常业务过程中不会进行该项目。
选定的申请人将接受面试，提案将得到深入讨论。
顾问列表
所有申请将由我们的顾问进行审核，顾问包括著名数学家和科技行业资深人士，以及数学人工智能领域的专家。
知识产权和数据共享
基金支持的项目生成的所有代码都必须在开源许可证（例如 MIT、GNU GPL 等）下发布。
基金支持的项目生成的所有数据集必须在开放访问存储库中共享，并附有适当的文档。
特定的开源许可证和存储库将在项目开始之前与文艺复兴慈善基金会达成一致。
间接花费
我们要求所有获奖者，除非在奖励协议条款中另有约定，否则不得使用奖励资金来支付任何间接花费，并且在任何情况下都不得将间接花费分配给奖励，除非明确同意以书面形式写入协议，允许裁决用于间接费用。换句话说，除非明确同意，否则获奖者不应将任何间接花费纳入资助预算。
如果根据奖励协议的条款允许间接花费分配，则应适用以下规则，除非适用的奖励协议中另有明确规定：
间接花费不得超过奖励总额的10%；
分配比率必须事先得到项目经理或其他办公室的批准；并且
间接费用分配必须作为项目预算的一项
联系方式
项目团队
汤姆·卡利尔（Tom Kalil），文艺复兴慈善事业CEO首席执行官
汤姆曾在两任总统（奥巴马和克林顿）的白宫任职，并与他的团队和参议院合作，赋予每个联邦机构支持高达 5000 万美元奖励的权力。汤姆还设计并启动了数十项白宫科技计划，其中包括克林顿总统宣布的耗资 400 亿美元的美国国家纳米技术计划；奥巴马总统宣布的大脑计划；克林顿总统和戈尔副总统宣布的下一代互联网倡议；以及先进材料、机器人、小型卫星、数据科学和教育科技方面的举措。
汤姆还担任 Schmidt Futures 的首席创新官，这是 Eric 和 Wendy Schmidt 的慈善项目。在施密特期货公司，汤姆支持成立了 Convergent Research，该组织致力于孵化和推出重点研究组织，这些组织是有时限的非营利组织，旨在加速科学进步。汤姆·卡利尔担任 Convergent Research 主席。汤姆还担任 Future House 的董事会成员，这是一家致力于为实验室构建人工智能助理的非营利组织。
莎拉·康斯坦丁（Sarah Constantin），文艺复兴慈善事业研究员
莎拉是文艺复兴慈善基金会的研究员。此前，她曾担任 Nanotronics 的企业发展总监，负责管理与推出第一个基于人工智能的实时工业过程控制系统相关的战略合作伙伴关系和计划。在此之前，她创立了Longevity研究所，这是一家非营利性研究机构，资助衰老生物学的寿命研究。在此之前，她在各种应用中从事机器学习和数据科学工作，包括自动驾驶汽车 (Starsky Robotics）、药物发现（Recursion Pharma）和网络安全（Palantir）。她拥有耶鲁大学数学博士学位和普林斯顿大学学士学位。
参考资料
原标题：《小乐数学科普：每人最高可获100万美元资助的AI for Math Fund数学人工智能基金成立——陶哲轩等人担任顾问》