TorchLean 升级：可在 Lean 里编写带形状检查与证明的张量程序
burny_tech · x · 2026-10-15
TorchLean 作者 Robert Joseph George 发布更新，介绍该项目从机器学习验证工具扩展为 Lean 内的通用张量编程与执行框架。
- 张量 API 扩展：新增形状安全操作、einsum（通用张量缩并）以及 rearrange/expand/reduce 等维度操作，可直接在 Lean 中表达矩阵乘法、多头注意力等复杂计算，形状在 elaboration 阶段即被检查。
- 已验证的 lowering 路径：einsum 实现可生成融合的基于索引的计算，并有 Lean 证明连接其数学规范，包括算术运算顺序。
- GPU 编译与自定义函数：支持将受支持的 Lean 函数编译到 GPU 执行，通过张量 API 调用；自动微分基于“tape”记录反向传播所需操作。
- 核心问题：lowered 程序是否仍计算作者写下的函数——这在 Lean 中可以被精确陈述并证明，让“写计算、求值、证明”成为同一项目的组成部分。
「编程与Agent」频道最新
- 开发者让 Codex 同时接管 Mac 与 iPhone Air,自主做游戏性能剖析优化 — Dimillian · 2026-10-15
- 群聊成 Agent 控制面板:Zenzap 让团队在聊天里审批和指挥多个 AI Agent — rohanpaul_ai · 2026-10-15
- React Bits 2.0 发布：216 个动画组件与全新设计工具全面开源 — shadcn · 2026-10-15
- 一图对照 Kiro/Claude Code/Codex/Cursor 功能命名速查表 — DigitalColmer · 2026-10-15
- 一周攒点子、并行 10 个 agent 做原型：一人软件工厂工作流 — Stefania_druga · 2026-10-15
- 华为等提出 SwarmRSI：科学 agent 集群实现递归自我改进 — Qianru Meng · 2026-10-15