新智元报道
新智元报道
一图看透全球大模型！新智元十周年钜献，2025 ASI前沿趋势报告37页首发
近日，陶哲轩表示，自己所担任顾问的AI数学基金，刚刚公布第一批获得资助的项目：去年12月，陶哲轩表示同意加入AI数学基金（AI for Math Fund）顾问委员会。该基金由Renaissance Philanthropy（文艺复兴慈善基金会）与XTX Markets联合发起，旨在支持新型AI工具的开发，为推动数学长期发展奠定基础。
1800万美元为数学突破提供「AI加速器」该基金首轮资助的29个项目，涵盖斯坦福、剑桥、牛津等全球多所顶尖高校和研究机构的数学家与研究人员，致力于构建能够在多个关键任务中促进数学研究发现的AI系统，比如：
每个项目的资助金额最高可达100万美元。AI数学基金于2024年12月启动后，收到了全球280份高质量提案。由于这些提案质量非常高，9月17日，XTX Markets决定将最初承诺出资的900万美元，翻倍至1800万美元。XTX Markets慈善事业负责人Simon Coyle表示：
部分获得资助的项目名单如下：Sketchpad（爱丁堡大学）：开发将数学证明自动转换为结构化数据的系统，引入新的图结构表示方式，把证明拆分为独立语句，以提升AI在形式化数学中的实用性与精度。形式化现代定理（帝国理工学院）：构建公开数据集，收录来自《数学年刊》等期刊的定理形式化陈述，扩充形式化数学库，为自动形式化、错误识别、辅助证明等任务提供评测基准。LeanTutor（加州大学伯克利分校）：开发可自动形式化本科生数学证明并判定其正确性的工具，提供个性化学习反馈，结合教育研究、机器学习与形式方法，构建学生与AI共同探索数学的平台。文艺复兴慈善基金会召集了专家评审委员会负责评审提案并发放资助，其CEO Tom Kalil称，自己坚信这些项目所开发的工具将具有真正的变革意义：
XTX Markets创始人兼CEO Alex Gerko近期表示，将在「AI 数学」方向提供重要的慈善支持。他向Lean FRO（Focused Research Organization，由Convergent Research支持）捐赠500万美元，用于提升Lean系统的自然语言能力与形式/非形式数学的接口。同时，他还向Mathlib项目捐赠500万美元，以支持其在Lean中对基础数学知识形式化的持续发展。
「AI数学基金」的发起者「AI数学基金」旨在通过支持数学发展方面至关重要的项目，来加快数学发现的进程与影响力。优先支持以下两大方向的项目：在常规体制下，难以推进的研究；有潜力带动整个领域发展的创新举措：如开发开源工具，扩大与优化AI模型训练所需的数据集，提升工具易用性，帮助更多数学家采用AI工具开展研究等。文艺复兴慈善基金会文艺复兴慈善基金会是一家非营利组织，致力于通过激发慈善家、科学家与创新者的雄心，引领21世纪新一轮的「文艺复兴」。成立首年内，该基金会推动超过2.14亿美元的科学、技术与创新类慈善资金，启动了10多个覆盖AI、教育、气候、健康与科研基础设施的项目。XTX MarketsXTX Markets是一家全球领先的算法交易公司，它运用最前沿的机器学习技术，为股票、固定收益、货币、大宗商品及加密资产等50,000多种金融工具提供价格预测。XTX Markets通过交易所与替代交易平台进行交易，公司日交易量超过2,500亿美元，业务遍及35个国家，在伦敦、新加坡、纽约、巴黎、布里斯托、孟买和埃里温设有办公室，员工超过250人。XTX Markets拥有业内领先的计算资源，配备了超过25,000 块GPU，拥有650PB的可用存储空间。公司还在芬兰建设大型数据中心，以满足未来不断增长的算力需求。自2020年以来，XTX Markets向全球各类慈善组织和非营利机构捐赠超过2.5亿英镑，成为英国乃至全球重要的慈善捐助者。XTX Markets还特别重视数学教育与研究，已向英国的慈善和教育机构提供逾5000万英镑资助，重点支持更多来自低收入家庭的学生，进入数学相关的高等教育及高技能职业领域。
文章原文
