% V! }( g: e6 Q, b一方面,你们通过 Robinhood Chain 等产品成为 加密生态的建设者;另一方面,你们也算是「外部用户」,通过与 Arbitrum 等合作,感受到整个行业已经建成的东西。 , i; f" O3 r e A8 h: z9 m# S9 I4 n' g U ]: [+ ~! w
我想你肯定也会有一些感受,比如:「大家这个地方做得很差,需要改进。」我们节目的听众里有很多创业者、开发者、建设者。我很想听听 Vlad 的意见:你觉得加密行业在哪些地方做得不够好?有哪些地方应该改进?你希望看到开发者们在哪些方面投入更多?4 E5 f) C# o4 I
8 K& O' u6 t) Y- @8 Y. G! [) kVlad:我其实不太把自己看作是「加密行业的客户」。我认为 Robinhood 是非常活跃的参与者。就市场份额、交易量、收入而言,尤其在美国,我们已经是加密领域最大的公司之一。0 ] C( l% p# A; Z m1 s+ C
) E& I+ _2 r" a- }; [" C
我觉得过去缺失的,是 加密和传统金融体系几乎是两个割裂的世界,中间缺乏连接。稳定币是少数的反例,它们开始起到桥梁作用。但我的态度不是说「你们去修复它」,而是——我们自己就在场内努力改善,利用 Robinhood 的能力和优势,把这个连接点做好。 ( `% t( t0 n/ \8 a7 \: g% V% U- P @) x. a$ p, r D$ k Robert:当然,这里也有时间因素。比如说,你们现在做了 Robinhood Chain 这个 L2,但也许你们几年前就想做了。 . }& G0 Z0 n6 p/ \2 x2 _+ `5 ?4 ~; @, x7 K3 Q+ s
我相信肯定有些事是你会想:「我真希望现在就能做」,但当时技术不够成熟、产品体验太差,或者流动性不足。甚至包括你们现在探索的 私募市场资产,或者 预测市场 的一些尝试。感觉就是,现在时机才刚刚成熟。那你觉得有哪些事,是你想做但还没到时候的?' n& M i" \( h8 c% c" N
- o7 {! \5 W. ]5 U+ K: y7 @ Vlad:我觉得现在有很多讨论围绕 AI Agent:未来这些 AI 会不会用加密货币彼此支付、完成交易?8 J$ ?& l* M4 K& v
1 V- k0 d9 o' ]6 B
但除此之外,还有 现实世界的 AI,比如机器人、医疗设备等等。那这些现实世界的 AI Agent 未来会不会也用加密货币相互支付?那会是什么样子?我认为我们离这两种场景都只有一步之遥,再往前一步,就是 加密真正成为 Agentic Commerce 的工具。 . `* B/ B9 C5 F9 L$ p% h - f" o! g* h4 C: aHaseeb:既然你提到了 AI,就顺便问一下:你还在做一个叫 Harmonic 的公司。如果我理解没错的话,你们正在构建一个基础模型,用 Lean 和定理证明(theorem proving)来验证数学,从而验证模型生成的答案,你作为 Robinhood 的 CEO,怎么还有时间做这件事?你在这家公司里参与到什么程度?为什么会选择做这个方向?7 E* m2 f# g9 W/ S
# P. L$ F9 t+ g5 ?3 I" c Vlad:我是 Harmonic 的董事长。这是一家和 Robinhood 完全独立的公司,我没有日常的运营角色,但我是创始人,也非常关心它。$ [3 A6 l, q0 ~3 \- b
3 M7 n7 V/ B0 r, D6 o6 ?& l几周前,Harmonic 宣布我们的模型 Aristotle 在国际数学奥林匹克竞赛(IMO)上达到了金牌水平。大家可能知道,这是一项极其困难的数学考试。像 GPT-5、Grok 这样的现成大模型,在这种题目上通常连一道完整的题都解不出来,表现非常差。 - ^% a) x& t. _. k# k5 J$ J8 ?3 [$ {/ g: I% H b: d3 d3 ^
问题有两个方面。一是这些题需要「灵光一闪」的创造力,如果找不到那个切入点,就完全解不出;二是它们通常需要 10 步以上的逻辑推理,只要其中一步错了,整个证明就错误,结果也就不对。8 b! x4 c% Y6 [- F. F# I- h
9 |! O2 j$ n! W' h事实上,我们是用形式化方式完成的。你刚才提到 Lean 定理证明器,我们确实用它来生成形式化证明。这意味着结果不需要人类手动验证,只要把它输入 Lean 内核,系统就会逐步检查每一步证明是否正确。 7 Q' z5 j4 \/ {5 I8 M: T7 n6 x+ _: G
接下来你可能会问:这有什么应用场景?我们称之为「数学超级智能(mathematical superintelligence)」。 : M: R1 j/ H* Q+ R+ n' K4 U1 y8 d7 z
它的意义在于,AI 不仅能生成答案,还能在非常高的标准下验证答案的正确性。想想现在 AI 已经在大量生成代码。高级软件工程师的工作,正在从「写代码」转变为「验证 AI 写的代码」。如果是前端 UI,还比较容易验证,你可以肉眼确认是否符合设计规范。但如果是后端系统,或者智能合约,尤其在失败可能导致数亿美元损失的场景下,人类必须严格验证。 ) C2 Y; M+ g. i: V$ C+ [: f* L, V$ z1 R0 C
这就创造了一个 形式化验证的市场。所以我们对这件事很兴奋。我认为它的应用不仅限于数学,还会扩展到所有软件,甚至硬件。 5 B% v- P$ u* [, b9 e* u5 X3 ?9 Y. l. E) C X1 G) W; c# m Haseeb:所以你认为,这是一条更好的路径,能比像 Anthropic 那样的路线更快构建出「软件工程代理」。你觉得:以定理证明和数学作为基础,是实现真正 AGI 的必要前提。 9 N. c& q! n5 q) W! ?, w0 v1 ^- P- U6 c Vlad:我认为这不仅是更好的路径,而且是不可避免的。因为在一个 AI 大量生成内容的世界里,这些产出已经多到人类根本看不完,我们需要一种新的方式来保证它们是正确的。 * b* W _; b+ o0 y9 N' V+ o) z ' `8 h- W) N; ~( F+ ^: Q这里有两点:我们必须确保结果是正确的;它甚至不需要用人类能直接读懂的语言来表达,因为人类已经不会逐行去看了。所以,整个底层逻辑会发生变化。问题变成:我们要怎样才能快速验证 AI 的结果是否符合预期,而不用一行一行去人工核对。3 X+ C: B+ ]# m, y% q& a- `2 a
& ]# S4 e3 O2 L1 W5 c Tarun:我有两个相关的问题。第一个算是对形式化验证的一种美学批评。0 w; F+ U. t: D( a
( E# j& b0 o* y你当年从大学辍学,却深度参与数学研究,可能就是因为被某些证明的美感吸引了。对我来说也是一样——有些定理的证明简洁优雅,让人觉得极其美妙。而数学一直以来都有一种张力:形式化计算和美学直觉之间很难共存。 $ f# V M4 Z; I: D 7 h5 @/ `. s$ ]3 j6 Z$ q ]
Lean 生成的证明,可能会像「四色定理」的计算机证明一样——极其冗长、不美观,相比之下,人类的间接证明更优雅。你怎么看待这种情况?要如何保留数学的美感? . s8 p; e. c6 ]$ b9 F * o' J! H& d6 X# E. r5 CVlad:你看过 Aristotle 在 Lean 中生成的证明吗? 9 U3 m, H% T. R0 E( L/ y, E ; s1 w6 F; B% H; f/ D+ @/ L3 QTarun:我看过一两个,但没看过完整的合集。 + S" c) j# z8 M- N1 b1 l0 R4 l( K+ A. ^7 q Vlad:其实我觉得它们很美。而且,把 Lean 证明转换成自然语言,难度并不大,几乎可以机械化完成。5 ?$ s. C/ Q% o; B. d7 X/ m4 j R! e
- ?4 n1 u3 h& u1 j5 G6 t6 _因为 Lean 的函数和定义都有描述,可以很容易地从高度形式化的细节,转换成更具描述性的英文叙述。我觉得这也是 Lean 相对以往形式化语言更容易使用的地方,这也是它不仅在 AI 领域受到欢迎,也在数学家中流行起来的原因。: }1 P% @% b" X% W6 T
+ t8 I. }# d4 }' @8 J
另一方面,反过来就很难了。把非形式化的证明转化为形式化证明是非常耗费精力的工作。目前在英国帝国理工学院,教授 Kevin Buzzard 正在主导一个大型计划,要把费马大定理完全形式化。这是一个庞大的工程,需要数百名数学家、持续数年,才能手工完成。通过这种对比,你就能看出两者难度的差别。 " X3 e8 X. z' i0 f5 D 1 x# z; I# P8 `Tarun:我最后一个问题是:除了千禧年难题(Millennium Prize Problems),你希望 Aristotle 或它的后继模型去解决什么问题? / t0 G/ l$ m, p# X3 ]& i- B3 q1 E' x# h
千禧年难题太显而易见了,比如黎曼猜想、P=NP 这些,大家都在讨论。但你有没有什么「个人的执念问题」?如果它被解决了,你会觉得「好,这就是我最大的成就」。. G2 [! U: s& X" h6 l6 } h" D5 o5 f, E
6 }* g/ D' K5 z5 f Vlad:好,那就不说黎曼猜想了。6 T. ], S/ A& O6 x" s) g% n
0 Z* N. S9 Z. \Tarun:对,那太显而易见了。! m* h1 M8 `* D
+ M! \. R" h$ f- l M5 z- D Vlad:但其实我还是挺喜欢黎曼猜想的(笑)。如果换一个例子,我觉得做一个「善意版的 HAL 9000」会很酷。我很想打造一个航天器的逻辑核心和控制中心,当然前提是它不会像电影里那样失控、自己起飞。; \2 g( S$ r; N0 y9 n
1 Y+ V$ A; K7 w( B0 @1 e' I Haseeb:呃……你确定这是你想告诉大家的例子吗?+ n! \, v* }7 K2 F6 H
; \/ p5 L. j5 V2 f" CVlad:(笑)对,我的意思是要一个可以形式化验证的航天器控制系统。一个真正「善意的 AI」。我们确实需要一个可靠的控制核心。我觉得最初的目标确实是分开的,但现在开始出现重叠。比如 智能合约验证。 8 t5 f. i: X- u, T' _$ n6 c6 S1 p+ j- g, \3 a
智能合约本质上是运行在 Solidity、Rust 等语言上的一段相对独立的代码。我们必须确保一些基本性质,比如合约不能停摆、不能出现「双重支付」等问题。因为一旦出错,可能导致数亿美元的损失,这已经有过惨痛案例。而目前,智能合约公司几乎只能依赖人工审计——花几十万甚至上百万美元,请外部公司逐行检查代码。% @, r+ o5 |. p2 h) j6 W