AI在IMO竞赛的表现 - 字节跳动Seed团队的形式化数学推理专用模型Seed Prover在IMO竞赛中解决了6道题目中的4道以及一道题的部分证明，成绩为30分，达到银牌分数[4] - 该成绩获得IMO官方认证，展示了AI在复杂数学问题解决方面的能力[4] 人类选手Warren Bei的卓越表现 - Warren Bei以满分42/42的成绩成为2025年IMO五位满分选手之一，这一成绩在全球范围内极其罕见[5][6] - 作为加拿大队唯一的满分选手，Warren Bei的排名为全球并列第1名[7] - 他在过去五年IMO比赛中获得三金两银，展示了持续卓越的数学能力[9][15] Warren Bei的学术背景与成就 - Warren Bei不仅在数学领域表现出色，还在2023年国际信息学奥林匹克(IOI)中获得银牌[9] - 他于2025年获得麻省理工学院(MIT)提前录取，这是对其学术潜力的认可[10][11] - 他在2021年以初中生身份获得加拿大数学奥林匹克(CMO)冠军，成为史上最年轻获奖者之一[16] - 2023-2025年期间，他连续四次获得CMO冠军，包括2025年以35分制中的27分夺冠[17] Warren Bei的学术理念与方法 - 他强调数学竞赛的乐趣在于解决问题的过程而非奖项本身[18] - 他认为困难是暂时的，关键在于依靠直觉生成想法并持续尝试[19] - 他建议年轻选手寻找解法背后的深层洞察，而非追求表面答案[21]

FormalMATH基准测试 - 香港中文大学、西湖大学、MAP、浙江大学、马克斯·普朗克智能系统研究所等机构联合推出FormalMATH形式化数学推理基准测试，包含5560道经过严格验证的数学题，覆盖从奥数到大学水平的代数、微积分、数论等领域[1] - FormalMATH基准测试首次系统性评估当前LLM驱动的定理证明器的真实水平，结果显示表现最佳的模型Kimina-Prover成功率仅为16.46%[3] - FormalMATH包含5560个经过Lean4编译器验证的数学命题，涵盖12个子领域，规模是经典基准MiniF2F的22.8倍[5] 构建创新 - 研究团队提出"三阶段过滤"框架解决传统形式化数据依赖专家手动标注的瓶颈：多LLM协同翻译、自动化验证、否定反证过滤，该流程在人工审核前保留了72.09%的高质量命题[7][9] - 团队召集12名人类奥赛金牌级别的专家花费22天检测自然语言数学命题与Lean4形式化命题之间的语义一致性[9] LLM表现分析 - 主流LLM证明器在FormalMATH全量数据集上表现远低于预期，最佳模型Kimina-Prover成功率16.46%，次优模型STP成功率13.87%[10][15] - 现有模型在代数等领域表现较好，但在微积分等其他领域表现接近随机猜测，显示出明显领域偏差[11][12] - LLM证明器频繁滥用自动化策略，导致冗余假设(34%)、不完整证明(62%)、自动化策略误用(65.0%)、无法正确应对不等式(13.0%)等典型错误[16] 技术瓶颈与突破方向 - 自然语言引导可能反拖后腿，例如DeepSeek-V1.5-RL模型在普通CoT提示时表现优于引入人为自然语言引导的情况[17] - 未来提升LLM形式化推理能力需从三方面突破：强化多步规划、跨领域泛化、人机协同验证[19] 开源与行业影响 - FormalMATH基准测试的代码、训练数据及评估模型已向公众开放，研究团队呼吁学术界与工业界共同推进形式化数学推理技术发展[20][21]

DeepSeek-Prover-V2-671B模型发布 - 公司发布专注于形式化数学推理的开源大型语言模型DeepSeek-Prover-V2-671B，参数量达6710亿 [1] - 该模型结合LLM泛化能力与形式化工具（如Lean），首次实现自然语言描述到机器可验证证明的大规模端到端转化 [2] - 形式化数学被视为AI"终极挑战"，突破可能将数学研究效率提升数倍，并打开金融建模、芯片验证、密码学等高价值商业场景 [2] 大模型开发者活动 - DeepSeek前成员辛华剑将参与"大模型开发者与AI基金合伙人跨洋对谈"，分享《大语言模型时代的形式化数学革命》 [2] - 辛华剑为DeepSeek-Prover系列模型开发主导者，现任爱丁堡大学AI博士生及字节跳动研究实习生，专注大模型在数学定理证明的创新应用 [2][4] - 锦秋基金合伙人臧天宇将同期分享2025年AI创投趋势 [3][4] 活动主办方背景 - 锦秋基金专注AI领域投资，在管基金为12年长期基金，59%项目为首次投资，采取多轮追加策略，已投资北美活跃AI基金 [6] - 剑桥中国人工智能协会(CCAIA)致力于链接中国AI产业与海外学界，采用轻量化社群模式促进中英资源流动 [7] - 清华大学学生通用人工智能研究会(THUAGI)以培养下一代通用AI人才为目标，依托清华AI研究院资源 [9] - 清华大学学生创业协会成立于1997年，为全国最早高校创业协会之一，28年来聚焦创业生态培育 [10] 活动流程 - 英国时间15:00/中国时间22:00开始辛华剑主题演讲，随后臧天宇分享AI创投趋势 [8] - 活动含圆桌对谈及观众提问环节，国内通过腾讯会议直播，需通过锦秋基金公众号报名 [5][6][8]