SAIR 视频总结 Dashboard

Lean 的创造者 Leonardo de Moura 阐述 Lean 如何把数学变成可机器验证的「数据」，并成为数学研究、软件验证与 AI 的可信基础设施。

Lenore Blum 用一个极简的「意识图灵机（CTM）」形式化模型，从理论计算机科学的角度阐释人类意识的产生机制，并由此论证 AI 意识的出现不可避免。

图灵奖得主 Jeff Ullman 以亲历者视角回顾 AI 从 20 世纪到 21 世纪的范式转变，剖析 prompt 编程对程序员的影响，并吐槽学术界论文泛滥、并分享他用 AI 智能体为期刊寻找审稿人的实践。

高尔斯先用一个几天前的真实案例展示 LLM 已能独立做出博士论文级别的组合数学新结果，再剖析当前 AI 证明在透明度、原创性、教育性和算力效率上的不足，并介绍其剑桥团队正在打造的「有动机证明」平台与数据库。

顶级风投 a16z 的 AI 投资人剖析为何「AI + 科学」创业格外艰难——根源在于物理世界缺乏语言模型那样的普适低维结构与海量数据，并结合投资组合案例总结出五种应对技巧与一套实战融资/组队/算力打法。

SAIR 团队成员介绍其「开放即设计」的科学与 AI 协作平台，通过竞赛、Playground、开放基准与贡献者网络，把科学问题变成可复用的开放研究基础设施，让全球每位科学家都能参与。

强化学习奠基人 Richard Sutton 论证：生成式 AI 只会模仿，无法兼具新颖与优秀，真正的创造与发现必须依靠「变异—评估—选择性保留」这一被监督学习所缺失的机制。

陶哲轩讲述数学这一最保守学科如何借助形式化验证、大规模协作与 AI 开始转型，并以「方程理论项目」和与 DeepMind 的合作为例说明 AI 的正确用法。

用单体（monoid）这一简单玩具模型刻画数学的可压缩性，论证人类数学是形式数学海洋中那个可被层级化压缩的小角落，并据此为自动推理提供指引。

诺奖得主谢克曼以百年蛋白质结构研究史为主线，回顾从测序、晶体学到AlphaFold的演进，讲述AI如何最终破解困扰生物学界一个多世纪的蛋白质折叠难题。

Axiom 创始人 Carina Hong 阐述 AI 数学已从奥数竞赛迈向真正的数学研究，并展示其「形式化+非形式化」混合系统在数论等领域的研究级成果与基准测试困境。

图灵奖得主厄尔曼以亲历者视角回顾上世纪AI的浮夸与失败，指出今日AI的真正价值在于借助算力与海量数据「解决实际问题」，并对软件工程在大模型时代的前途提出开放性追问。

诺奖物理学家以引力波探测 (LIGO) 为例，剖析 AI 在前沿物理实验中的现有用途、根本瓶颈，以及它能否独立做出基础科学发现的深层问题。

五位横跨药物研发、AI 基础模型、组织工程、合成生物制造与医疗投资的专家，讨论 AI 如何加速新药发现、降低制造与医疗成本、扩大患者可及性，并直面医保系统公平性的难题。

五位年轻创业者分别在太空算力、搜索、物理基础模型、AI 推理基础设施和持续学习等不同技术栈层级上构建未来 AI 基础设施，并分享彼此的瓶颈、科学与 AI 的结合点以及给年轻人的建议。

图灵奖得主 David Patterson 与 Databricks/Perplexity 联合创始人 Andy Konwinski 讲述他们如何用慈善资金、以「登月计划」(Moonshots) 和创业式打法重塑科研资助模式，把伯克利高影响力实验室经验推广到顶尖高校，以加速前沿科学落地。

六位来自工业界与学术界的领军者围绕「AI 如何加速科研」展开圆桌，讨论简洁性原则、学术与企业的融合、人才争夺、知识与算力的集中化风险以及安全与开放生态。

五位来自物理、计算机科学与 AI 芯片领域的专家圆桌讨论：当 AI 走进科学，开放与封闭如何取舍——开放是科学的根本，但资金、隐私、安全与算力成本也为封闭留出了空间。

Distributional 创始人 Scott Clark 在 SAIR/Cera AI Kickoff 上谈到，AI 最大的科学价值在于跨学科「翻译」与连接知识，而可观测性与人类设定目标的智慧是驾驭日益自主的 AI 系统的关键。

图灵奖得主、Alphabet董事长John Hennessy从计算架构、AI for Science、科研资助与人才培养等角度，畅谈AI正如何加速科学发现，以及人类科学家在其中不可替代的角色。

图灵奖得主 Jeff Ullman 在 π Day 接受访谈，从工业革命与编程史的视角探讨 AI 如何重塑科学、就业与人类社会，并对 AGI 的近期可行性表达审慎乐观。

陶哲轩与艺术史学者塔尼娅·克洛登围绕两人合著的论文《AI 时代的数学方法与人类思维》，探讨 AI 对数学与人文的冲击、人机协作的价值，以及他们提出的‘智能的哥白尼式转变’。

菲尔兹奖得主陶哲轩在与儿子的对谈中讲述他如何在数学研究中可靠地使用AI，并提出「AI是高产但不可饮用的污水消防水龙头、数学验证则是净水滤芯」的核心比喻。

ICONIQ 普通合伙人 Murali Joshi 以炉边对谈方式，分享他们如何长期陪伴并投资 Anthropic、Datadog、Snowflake 等公司，以及对创始人识别、护城河、AI 与科学/安全/算力前沿的判断。

Tom Kalil 解析「AI赋能科学」的真正瓶颈在于缺少公共物品（数据集与评测基准），并阐述为何慈善资本能填补政府与风投都不愿触碰的资金空白。

Hugging Face 后训练团队负责人 Lewis Tunstall 从理论物理转入 AI 的经历出发，讲述后训练（post-training）、强化学习与蒸馏的最新趋势，以及开源模式对 AI for Science 的关键价值。

图灵奖夫妇 Lenore 与 Manuel Blum 在圆周率日回顾各自的数学求学之路，并详细讲解他们合作提出的『意识图灵机（CTM）』理论及『有意识的 AI 是必然的』这一论断。

UCLA 应用数学家贝尔托齐讲述如何把流体力学、表面张力等基础数学思想迁移到机器学习，倡导可解释、尊重物理规律的 AI，并强调架起 AI 与科学之间的桥梁。

a16z 基础设施投资合伙人 Jason Cui 解读 AI 与科学相互促进的历史性时刻，以及风投在 AI for Science 中关注的基础技术、平台层与计算流体力学等机会。

诺奖得主谢克曼回顾从童年显微镜到酵母分泌研究的科学之路，并谈论开放获取出版的危机与AI(尤其AlphaFold)给生物学带来的根本性变革。

AWS 研究者 Erran Li 谈如何用可验证奖励、形式化验证与基础模型，构建可靠、能与科学家协作闭环的科学 AI 智能体。

微软研究院医疗AI负责人潘海方在SAIR启动会上指出，技术只是催化剂，真正落地需要跨学科社区、重塑工作流与社会契约，并以「雄心宏大、起步极小」的飞轮策略推进AI for Science，迈向打破数据孤岛的「学习型健康系统」。

沃顿优化学者达梅克·戴维斯回顾自己从纯数学到机器学习的研究历程，并指出上下文长度、可验证性与不同领域的「真理标准」是当下 AI 面临的核心瓶颈。

2017年诺贝尔物理学奖得主、LIGO引力波探测领军者巴里·巴里什在SAIR大会上讲述精密科学的价值，并探讨如何让AI跨学科迁移人类的解题能力以推动科学研究。

菲尔兹奖得主 Michael Freedman 用「压缩」这一概念解释人类数学的本质，并通过分析 Lean 数学库 MathLib、建立幺半群（monoid）模型，论证人类数学是形式数学中可被压缩的那一小块多项式增长子集，进而探讨人类数学家应如何与 AI 协作。

在「AI×科学」播客首期中，陶哲轩与投资人陈楚（Chuck In）及主持人 Peter 围绕 AI 在科研中的真实定位展开对话，主张把 AI 当作可验证、可问责的辅助工具，而非替代科学家或被神化的「全能智能」。

菲尔兹奖得主 Michael Freedman 在 π 日访谈中，结合自身经历探讨 AI 如何改变数学研究方式、人机协作的新角色，以及对原创性思维和数学本质的思考。

在「AI for Science」启动活动现场，连续创业者 Amos Stern 讲述自己的网络安全创业经历，并呼吁要有像 CERC 这样的机构以长期视角、负责任地推动 AI 民主化、造福全社会。

数学家、前港科大与 KAUST 校长陈繁昌在圆周率日访谈中，剖析当前 AI 的能力与根本局限，强调人类判断力、创造力与跨学科人文素养在科学发现中不可替代。

Reid Hoffman 在一场 SAIR 科学活动的炉边对话中，阐述 AI 如何把每个知识工作者变成「智能体管理者」，并分享其 AI 药物发现公司 Manas、对 AI 加速科学与公众情绪的看法。

NVIDIA 与 UC Berkeley 的焦剑涛在采访中谈 AI 如何降低科研门槛、世界模型与校准不确定性如何加速模拟与科学发现，以及通才模型与专才模型的共存未来。

在圆周率日，Lean 之父 Leonardo de Moura 接受学生 Maddie 访谈，深入浅出地讲解形式化证明工具 Lean、AI 如何与之结合，以及 AI 将如何改变数学发现与未来职业。

OpenAI 研究员布贝克阐述构建 AGI 的终极目的在于加速科学，并以数学领域 GPT-5 已成为真正合作者为例，展望自动化实验室等下一个前沿。

陶哲轩在 SAIR 启动前夕受访，解释他联合创立这个 AI for Science 基金会的初衷，并深入剖析当前 AI（尤其是大语言模型）在数学与科学中的潜力、可靠性短板与正确使用方式。

一段产品演示视频，分步讲解 SAIR 平台「贡献者网络」如何让研究者公开、复用并引用彼此的「速查表（cheat sheet）」，形成可追溯的协作知识图谱。

一段近3分钟的官方上手教程，演示如何创建 SAIR（基于 Zindi 竞赛平台）API 密钥并完成首次 API 调用，把竞赛工作流接入自己的脚本、训练任务和 CI 流水线。

这是一段 SAIR Playground（练习场）操作教程，演示如何在不影响排行榜的前提下，迭代测试与打磨用于「数学蒸馏挑战赛」的 cheat sheet（备忘单/解题策略）。

一段约 2 分半的官方教程，演示如何在 SAIR「数学蒸馏挑战赛——等式理论（Equational Theories）」第二阶段的 Playground 中创建、运行和调试求解器（solver），并说明正式比赛的两条赛道与提交规则。

一段操作教程，逐步演示如何在 SAIR 模运算挑战赛(Modular Arithmetic Challenge)的 Playground 页面提交并评估你的模型。

陶哲轩远程介绍 SAIR 正在举办的数学竞赛——以「蒸馏挑战」和「模算术挑战」为代表，旨在为 AI 时代的数学建立新的「交通基础设施」，让开源模型逼近前沿模型水平。

陶哲轩在圆周率日(3月14日)送上简短寄语，提醒人们日常科技背后无处不在却被忽视的数学，并号召大家在这一天留意并庆祝数学。

图灵奖得主、RISC 架构奠基人 John Hennessy 在 SAIR π Day 特辑中畅谈数学与计算机的深层联系，以及 AI 作为科研工具的潜力与局限。

在 π Day 当天，菲尔兹奖得主 Tim Gowers 接受访谈，回顾自己走上数学之路的历程，并就 AI 时代学生该如何学数学、协作方式将如何演变给出建议。

SAIR 基金会的开篇短片，阐释当下 AI 在科研中的真实定位：擅长重组已知信息、承担重复性杂活，且必须以可验证为前提，做人与 AI 的协作伙伴关系。

陶哲轩代表 SAIR 基金会发布首届竞赛——「数学蒸馏挑战赛」，邀请参赛者撰写一页「小抄」(cheat sheet)，把 2200 万道代数判断题的解题知识提炼出来，用以大幅提升弱模型的准确率。

一支汇集多位科学家观点的宣传短片，阐述 AI 正在变革科研、SAIR 致力于搭建连接研究者与产业的全球社区，并宣布其首届「蒸馏挑战」竞赛。

陶哲轩在简短的开场致辞中，欢迎大家参加 SAIR 基金会首批活动之一的「AI for Science 2026 启动大会」，并预告将汇聚数学与科学领域的顶尖嘉宾，探讨如何用 AI 加速科研。