← 返回动态 张小珺商业访谈录 2026-04-20 对洪乐潼的四小时访谈: AI for Math、Lean、证明与直觉 摘要 张小珺与洪乐潼系统讨论把数学转成 Lean、形式化证明、数学直觉与 AI for Math 创业。 阅读完整原文 ↗ 证据与核对发现渠道张小珺商业访谈录原始材料www.xiaoyuzhoufm.com材料类型来源网页；材料类型未核实材料范围获取范围未知复核状态未标记人工复核
