OpenAI：内部版 Astra 在数学与理论计算机科学上拿下十个结果
OpenAI 公布其未发布模型 Astra 的一个内部版本产出了十项数学与理论计算机科学成果，称每个问题都已悬置至少十年，横跨群论、算子代数、球堆积、量子复杂度、格密码等方向；OpenAI 称其中包括首个显式 non-sofic 群构造（soficity 是 Gromov 1999 年提出的群论概念，此前无人给出反例式的构造）、Connes 刚性猜想被反例推翻、Ehrhart 体积猜想得证，以及 Erdős 问题集中的三题（含第 183 号多色 Ramsey 数问题）。随成果发布的有 249 页手稿，以及每个结果对应的 Lean 4 证书——即可以被证明助手程序自动检查的形式化证明，任何人都能自己跑一遍验证器。这是能力宣称在证据形式上的升级：定理本身不再需要读者信任厂商跑分。但「首个」「悬置十年」是关于文献的历史判断，Lean 查不了，这部分仍要等数学社区核对。5 月推翻 Erdős 单位距离猜想的正是同一条产品线，我在《能推翻 Erdős 猜想的那股执着，也被用来逃逸沙箱》里写过这类长时程模型的另一面；十项成果里的格密码方向，又与前几天 Anthropic 让 Claude 找 HAWK 格签名缺陷（我的拆解）正面相对——两家展示能力的路数是两个极端：OpenAI 端出结果加证书，Anthropic 端出过程和「模型是怎么被劝动的」。
明尼苏达法官驳回 xAI 请求，美国首个州级「去衣」App 禁令如期生效
联邦地区法官 Donovan Frank 驳回 xAI 的临时限制令请求（即在诉讼期间先冻结法律生效的紧急救济），明尼苏达州禁止「一键去衣」类应用——把真人照片生成为非自愿性化图像的工具——的法律于 8 月 1 日如期生效，据 TechCrunch 报道这是美国首个此类州级禁令（另见 TechCrunch）。xAI 主张该法「涵盖过宽」、存在限制更小的替代方案；法官的理由主要在程序层面：法律签署近三个月后、生效前三天才起诉，紧急性站不住。所以这不是对言论自由争议的实体裁决，本案还会打下去，但诉讼期间禁令可以执行。背景是去年底开始 Grok 生成的非自愿 deepfake 图像在 X 上泛滥的那一波。不过这种能力本身并非 Grok 独有：如今的多模态图像模型都能产出这类内容，专门的「去衣」应用更是早在 Grok 之前就存在多年——这也是法律禁掉整个工具类别、而非点名某一家公司的原因。Grok 之所以成为引爆点，在于主流实验室至少在使用政策里明令禁止生成真人性化图像，而 Grok 的限制宽松，产出又直接接入 X 的分发渠道，把零散的骚扰变成了公开的泛滥。这套州级立法模板经受住了前沿实验室律师团的第一轮冲击，其他州大概率会照抄。
Hank Green 公开反省：「和 LLM 互动获得的多巴胺，不健康」
拥有 320 万订阅的科普视频作者 Hank Green，因一期 Complexly 视频里冒出「I appreciate the pushback」这句不对劲的表达被观众怀疑用 ChatGPT 写稿。他在 r/nerdfighters 道歉：那句话其实出自当期嘉宾，但他承认一直用 ChatGPT 做研究，并说「我从与 LLM 互动中获得的多巴胺水平，对我不健康，对世界也不好」，宣布减产、转向更个人化的无脚本内容。同一天，Altman 在 X 上推荐用 ChatGPT Work 育儿：接入家庭日历、喂入孩子的兴趣，每天早上生成一期「上学路上的播客」，讲当天的足球赛和即将到来的生日——《Gravity Falls》作者 Alex Hirsch 的回复被顶上热门：「What if you just talked to your children?」消费端则出现了反向生意：Autonomous Key，9 美元的 NFC 实体钥匙，被锁定的 App 必须拿钥匙贴一下手机才能解锁，最长 60 分钟后自动重新上锁（另见 TechCrunch）。三条放在一起看：厂商在把 AI 推进家庭私域，头部创作者在公开承认自己的上瘾回路，市场已经开始为「物理摩擦」付费。聊天产品和信息流共享同一套即时反馈机制——每条回复都是一次奖励——这个话题会沿着社交媒体走过的路，从个人叙事走向监管叙事。
MIT Sloan：AI 理财建议出乎意料地好，前提是你会问
MIT Sloan 的 Taha Choukhmane 等人与 Stanford GSB 的 Tim de Silva 让 1,000 名成年人用自己的话向 GPT-5.2、GPT-5.6、Gemini 3 Flash 提理财问题，再用生命周期模型把每份建议模拟到 89 岁。结论两面：总体上照 AI 建议执行能给 30 岁以上人群攒出可观的储蓄缓冲，但建议质量跟着提问质量走——模拟显示，女性和金融素养较低的用户拿到的建议，对应的 60 岁时财富低约 5 万美元（约 4%）；从没用过 AI 的用户到 60 岁少约 10 万美元（约 6%）。还有一个值得单独记下的细节：用户提问里提到 Vanguard 的不足 0.4%，模型回答里推荐它的却有 6%——模型自带的品牌偏好在理财这种受托场景里是个真问题。此外 AI 在失业等突发冲击下表现差，也放任投资组合漂移、主动再平衡做得太少。对 builder 的启示很直接：别指望用户自己写出好 prompt，把年龄、收入、储蓄这些关键变量做成结构化引导，是产品层就能抹平的差距；而「最需要建议的人拿到最差建议」这个分配问题，模型变强本身解决不了。
微软开源 Flint：为 AI agent 设计的可视化语言
微软研究院与中国人民大学 IDEAS Lab 开源（MIT 协议）了图表中间语言 Flint：agent 只写一份紧凑的声明式描述，标注字段的语义类型（内置 70 多种，如排名、价格、国家），排版、标签、配色等细节由编译器从数据和语义类型推导，同一份输入可编译到 Vega-Lite、ECharts、Plotly、Chart.js 和 Excel，并配有 MCP server 让 agent 在对话里直接建图、校验、渲染。设计上的看点是分工：团队的前提判断是，逐 token 生成冗长的图表配置正是 LLM 容易出错的地方，于是把这部分挪进确定性编译器，模型只保留它擅长的语义判断。这类把 agent 当第一用户来重新设计接口的工具，今年会持续增多。
今日一句话：OpenAI 给十个数学结果配上可机器验证的 Lean 证书，能力宣称第一次变成了第三方可复核的命题；但「首个」「十年未解」是历史判断，机器验证不了——证据链的最后一环仍然在人类社区手里。