/ C) A# R7 i9 ]Tarun:但也会有一些股份,是创始人非常在意的。 * N" Z% i! r O. Q& Y6 v8 H3 n& w& S7 w. s( Z3 P4 [( | Haseeb:对,有些股份公司确实很在意。我想 Robinhood 也不太可能真的拿到那部分。 # S8 n6 N$ i" i. b K R: t/ H; `4 u' O- g) m- x
我更感兴趣的问题,其实是你刚才点到的——Robinhood 的故事一直带有某种「普罗米修斯」的色彩:把原本高高在上的火种带下来,让散户可以接触任何金融资产、任何股票、任何他们本来不允许碰的金融工具。现在他们能碰到了。 ' t8 N- x) D- z2 {3 h# \3 M8 f1 g$ L. O) M9 V3 y
这个叙事我能理解,也很契合加密世界的精神。但与此同时,它也模糊了「私营公司」和「上市公司」之间的界限。毕竟,建立这么一整套制度,本质上就是为了划清两者的分野。2 ?/ a t3 y( ~5 ?* ~* M% O
6 {9 w& D. t& \. Y) f
如果公司是私营的,那监管就可以相对放松,允许它们更自由运作;但如果公司是上市公司,那一切都必须公开透明,所有面向散户的披露要求都要满足。3 m4 i% M7 f8 H. Y
# X0 ?: `+ F0 s- q6 h0 Z所以,当散户能同时接触到公募和私募的股票时,哪怕只是部分有吸引力的私企,这从社会层面看,是否会削弱「公募 vs. 私募」制度存在的意义?: _5 I& ]1 T6 X& ~. P; e1 d' l! h
1 `- V. u( Q/ V
在你想象的那个世界里,你认为这套制度应该被改造成什么样 ) b. Y! C' I6 f5 O8 n1 `' F% x5 I. V3 X: e Vlad:我并不认为这会削弱制度的意义。我不觉得有人曾经认真设计过一个体系,让美国 80% 的普通人主动地无法参与到这些价值增值的机会里。这更像是一个历史演进中的偶然结果。最初的确是基于投资者保护——让公司能更容易地运作和起步,而不需要承担过多披露要求,这是合理的。 8 V( s, a, g. L; N ) a y" q" `. M& v5 B但过去几十年里,情况发生了变化。上市变得越来越难,流程和要求越来越繁琐;与此同时,私募市场对公司来说反而更容易进入,有更多 VC、PE 提供资金。) M1 _ ]! W2 I0 \
* a" n D0 @( N$ i6 ]7 s' ?1 t- S
这两者结合在一起,导致很多公司不愿意上市,或者等到上市时已经是极高的估值。受害的,其实就是散户投资者,他们被挡在这些增值机会之外。所以我认为,完全可以在解决部分监管担忧的同时,让散户也能参与到这些优秀公司的早期机会里。 " Z4 k- c& P& h/ Y- X) `1 } 7 _* V: M; v. y, I( d5 Q5 WTarun:实际上,你说的情况让我想到加密世界里一个挺有意思的现象。在我看来,这就像是私募和公募市场之间一场不可避免的拉锯战——谁能先拿到更早期的份额。# f3 ]4 e; }& w7 X" U8 e
. E$ q3 n5 V! S3 J. ^+ h# j% z
在加密领域,这种情况反复出现。比如在牛市里,很多私募轮都会部分开放给散户,出现了一些平台,比如 Echo 或 Legion,公司先完成私募融资,然后再把一部分额度拆分成 AngelList SPV 的形式卖给散户。$ N" e! z7 H z# ~+ E
0 [5 e% i/ `) Z7 n: s9 u4 f但这种模式往往扩张得比公司的实际增长还快,结果就是一旦热度过头,项目又会迅速反向,彻底转为私有化,停止向散户开放。加密的特别之处在于,它的周期速度极快,相当于你能在一个小时内看到二十次公募市场的循环。- ^" o' o! B" r8 W5 \$ a( c
7 m& A+ Q' [9 ^" P7 x举个例子,如果你在链上完成一次代币化股票交易,或者我们在托管股票代币、私募代币时,你该把它算进加密业务,还是算进 TradFi 业务? / A6 B3 q& V1 b0 o& J$ H7 z# B( q: h: t3 m) \) N; a' r" V ~0 L# O
这种分类其实会遇到很多边界问题。就像「科技行业」这个概念正在变得越来越不相关——如今几乎没有公司可以说自己不是科技公司,因为所有公司都依赖技术。同样地,随着时间推移,这种「加密 vs. TradFi」的区分也会变得没那么重要。 # Z6 j1 z2 E8 |+ C# I5 q P2 z 9 A' U8 a, i. d0 y7 D作为 Robinhood 的用户,你可能会越来越多地在使用加密技术,但它不会是体验的「显性部分」。6 ~8 E d- m1 e
" ~ y8 w: v U+ k" [5 e
当然,如果你买的是比特币,那很清楚,你买的是加密资产;但如果你买的是代币化资产,加密在这里更多是一种基础设施和传输机制,而最终你拿到的是那个你真正想要的金融工具。 # B3 |5 H7 I9 E8 F; u4 {$ f' S- Y+ s' t- Z Tarun:其实这还和前面的问题有关:Robinhood 从股票起家再加上加密,而 Coinbase 则是从加密出发想扩展到股票。两家公司之间另一个差别在于 机构/基础设施层面。 9 h; v& E. z _ 1 d0 t, O" x' v& B比如,在托管、质押以及支持机构客户的基础设施方面,Coinbase 更倾向于「全栈掌控」。而在公募市场里,你很难拥有整个全栈。但在加密领域,有点奇怪的是,一个单一实体其实可以为终端用户提供完整的全栈。 s/ N. R9 K+ h& h6 V" h # w3 B/ g; @; [! T! ^5 [你们怎么看待这个?随着 Robinhood 想要同时服务加密和非加密的「全市场」,你们会不会逐步自己掌握更多基础设施?因为我觉得这是一个很大的转变。比如如果代币化股票的交易量远超你们现有的传统股票交易,那 Robinhood 会不会也要变成「全栈型」的?2 a# J: W8 D C6 Z7 T3 X
* ^8 E+ }( z+ z1 A Vlad:我把 Robinhood 的发展分成三个阶段来看:短期、中期和长期。8 C ^5 }5 Y- I& P0 S0 n
6 F& Q A R8 q, i
短期:目标是成为所有活跃交易者的第一平台,覆盖我们提供的所有资产类别——加密货币、股票、期权、期货等等。 6 m5 ?! ]: M$ ~6 d; l7 B8 p3 _. {# X6 G
中期:这是我们正在打造的阶段,成为客户的 No.1 金融超级应用。你的全部财富放在 Robinhood,所有交易都通过 Robinhood 完成。前两个阶段基本都是以零售为核心,我们认为这部分业务不需要完全纵向整合到机构层面。 % T4 G0 \+ w" U- w+ ?' E7 B; X" W) i7 ?: j% {, T; l8 e
长期:在我们不断建设这些能力的过程中(比如 24 小时交易、极低的保证金利率、资产代币化),这些功能本身就会对企业和机构客户有吸引力。毕竟,机构投资者同样希望能 24 小时交易,希望能在一个地方同时接触加密和传统资产,也希望得到最低的保证金利率。7 T& v' f$ W+ D3 S
6 G7 V/ [1 ^5 D+ j$ m这些功能会自然孕育出 B2B 和机构业务 的机会。展望 10 年,我认为 Robinhood 的 海外业务规模可能会超过美国本土,机构业务规模也可能超过零售业务。这让我非常兴奋,因为我们现在还只是刚刚开始。我能看到至少几条路径,可以让 Robinhood 的业务增长 10 倍,而且我们可以同时推进多条路径。3 w8 U/ E* W7 W( N4 ~& ?
: ~% j* w! O/ _5 e3 d" V Haseeb:所以现在 Robinhood 的角色很特别: 2 |+ V& D! e/ `+ p0 y1 J/ \' @) u5 u$ t! e! a
一方面,你们通过 Robinhood Chain 等产品成为 加密生态的建设者;另一方面,你们也算是「外部用户」,通过与 Arbitrum 等合作,感受到整个行业已经建成的东西。 1 L3 W2 o7 W y# a 2 ~7 m! N! d5 L9 t* T" r我想你肯定也会有一些感受,比如:「大家这个地方做得很差,需要改进。」我们节目的听众里有很多创业者、开发者、建设者。我很想听听 Vlad 的意见:你觉得加密行业在哪些地方做得不够好?有哪些地方应该改进?你希望看到开发者们在哪些方面投入更多? 4 a y5 `; J: L2 g k7 B. w. X Vlad:我其实不太把自己看作是「加密行业的客户」。我认为 Robinhood 是非常活跃的参与者。就市场份额、交易量、收入而言,尤其在美国,我们已经是加密领域最大的公司之一。 . ^8 s" S7 \- O0 a / D, c6 J6 O t6 S* I' h我觉得过去缺失的,是 加密和传统金融体系几乎是两个割裂的世界,中间缺乏连接。稳定币是少数的反例,它们开始起到桥梁作用。但我的态度不是说「你们去修复它」,而是——我们自己就在场内努力改善,利用 Robinhood 的能力和优势,把这个连接点做好。 - y: I0 E8 O3 _0 _) q9 w & v2 j- i# e# vRobert:当然,这里也有时间因素。比如说,你们现在做了 Robinhood Chain 这个 L2,但也许你们几年前就想做了。 ) k- N7 }" G1 S% B$ V4 T3 H0 h# n
我相信肯定有些事是你会想:「我真希望现在就能做」,但当时技术不够成熟、产品体验太差,或者流动性不足。甚至包括你们现在探索的 私募市场资产,或者 预测市场 的一些尝试。感觉就是,现在时机才刚刚成熟。那你觉得有哪些事,是你想做但还没到时候的?8 D, O- o }( U( r: [ h
9 Y2 N' ?! ~1 G6 E R. V% f Vlad:我觉得现在有很多讨论围绕 AI Agent:未来这些 AI 会不会用加密货币彼此支付、完成交易?# S5 g+ ^* }( A1 K0 m0 {
% l8 b' a4 e; N+ Q- j2 B0 b但除此之外,还有 现实世界的 AI,比如机器人、医疗设备等等。那这些现实世界的 AI Agent 未来会不会也用加密货币相互支付?那会是什么样子?我认为我们离这两种场景都只有一步之遥,再往前一步,就是 加密真正成为 Agentic Commerce 的工具。 ) n% Y( F4 v9 ~- `8 e2 @ % X4 X( E) r' p4 h4 hHaseeb:既然你提到了 AI,就顺便问一下:你还在做一个叫 Harmonic 的公司。如果我理解没错的话,你们正在构建一个基础模型,用 Lean 和定理证明(theorem proving)来验证数学,从而验证模型生成的答案,你作为 Robinhood 的 CEO,怎么还有时间做这件事?你在这家公司里参与到什么程度?为什么会选择做这个方向? " S; Q7 p) [) N2 u7 \" c5 K9 g! V+ i0 z }. n5 Y) g, J. C b Vlad:我是 Harmonic 的董事长。这是一家和 Robinhood 完全独立的公司,我没有日常的运营角色,但我是创始人,也非常关心它。% L9 b4 d( v- ^: i3 `0 t, E; E
- Q' T% B4 T3 m
几周前,Harmonic 宣布我们的模型 Aristotle 在国际数学奥林匹克竞赛(IMO)上达到了金牌水平。大家可能知道,这是一项极其困难的数学考试。像 GPT-5、Grok 这样的现成大模型,在这种题目上通常连一道完整的题都解不出来,表现非常差。 / E: {* N$ w! e ~, p+ K4 M 0 k3 H$ O: i0 B0 L' P6 F问题有两个方面。一是这些题需要「灵光一闪」的创造力,如果找不到那个切入点,就完全解不出;二是它们通常需要 10 步以上的逻辑推理,只要其中一步错了,整个证明就错误,结果也就不对。5 P" I& `3 P. [2 \4 C( R# d
' l) P* o6 K+ v
所以要同时具备创造力和逻辑严谨性。而且在这种场景下,AI 的「幻觉」问题会层层叠加。因此,这次结果是对我们技术的一个很好的验证。! |( @% I% t1 L* e" i' \7 B
2 B( c: b8 }! N0 a事实上,我们是用形式化方式完成的。你刚才提到 Lean 定理证明器,我们确实用它来生成形式化证明。这意味着结果不需要人类手动验证,只要把它输入 Lean 内核,系统就会逐步检查每一步证明是否正确。* B3 j0 r. \+ g c. n! f% d( K
1 O! v7 }6 M$ t" k% D* s
接下来你可能会问:这有什么应用场景?我们称之为「数学超级智能(mathematical superintelligence)」。) r# [' z% {) f) i; u, B% o
, [0 ^, n5 U& i, F2 t* `( S! ^它的意义在于,AI 不仅能生成答案,还能在非常高的标准下验证答案的正确性。想想现在 AI 已经在大量生成代码。高级软件工程师的工作,正在从「写代码」转变为「验证 AI 写的代码」。如果是前端 UI,还比较容易验证,你可以肉眼确认是否符合设计规范。但如果是后端系统,或者智能合约,尤其在失败可能导致数亿美元损失的场景下,人类必须严格验证。 ( p) c# [' }( u- H6 e; _! a1 m/ R2 W- O0 D7 `, a8 h
这就创造了一个 形式化验证的市场。所以我们对这件事很兴奋。我认为它的应用不仅限于数学,还会扩展到所有软件,甚至硬件。 2 G- o" b) C2 m# C, E4 t9 S( C/ x8 _1 I& }' {4 a Haseeb:所以你认为,这是一条更好的路径,能比像 Anthropic 那样的路线更快构建出「软件工程代理」。你觉得:以定理证明和数学作为基础,是实现真正 AGI 的必要前提。2 q! h' p9 M8 t$ |3 w. Q7 H0 {
. X! y6 j* X& d) U Z9 dVlad:我认为这不仅是更好的路径,而且是不可避免的。因为在一个 AI 大量生成内容的世界里,这些产出已经多到人类根本看不完,我们需要一种新的方式来保证它们是正确的。1 ?2 H' I: v1 V
+ t2 i( T- K1 H! i5 o这里有两点:我们必须确保结果是正确的;它甚至不需要用人类能直接读懂的语言来表达,因为人类已经不会逐行去看了。所以,整个底层逻辑会发生变化。问题变成:我们要怎样才能快速验证 AI 的结果是否符合预期,而不用一行一行去人工核对。 5 z* x2 d! _9 |: L$ x* o( Z u& b9 Z1 x Tarun:我有两个相关的问题。第一个算是对形式化验证的一种美学批评。 % ~8 e# C1 I: w % q1 _8 X( J4 q2 i z你当年从大学辍学,却深度参与数学研究,可能就是因为被某些证明的美感吸引了。对我来说也是一样——有些定理的证明简洁优雅,让人觉得极其美妙。而数学一直以来都有一种张力:形式化计算和美学直觉之间很难共存。 ( n+ ~" [' X: Y @3 m: W " @6 v) p0 F) ~, lLean 生成的证明,可能会像「四色定理」的计算机证明一样——极其冗长、不美观,相比之下,人类的间接证明更优雅。你怎么看待这种情况?要如何保留数学的美感? 4 e8 B6 `# b4 B' a. W& z8 u , G: j6 E3 x8 s FVlad:你看过 Aristotle 在 Lean 中生成的证明吗?6 r- l# |# j8 }8 ` s
8 v3 v& _; M; Z7 sTarun:我看过一两个,但没看过完整的合集。 9 I7 k/ n' f7 s, t3 w* V- O# c8 L) `% T1 ^ Vlad:其实我觉得它们很美。而且,把 Lean 证明转换成自然语言,难度并不大,几乎可以机械化完成。 : P- A3 Y, z5 A" W% N$ v6 D- @& w3 [" Z) V
因为 Lean 的函数和定义都有描述,可以很容易地从高度形式化的细节,转换成更具描述性的英文叙述。我觉得这也是 Lean 相对以往形式化语言更容易使用的地方,这也是它不仅在 AI 领域受到欢迎,也在数学家中流行起来的原因。 B& K( N0 }% Q, \ ) q Z! ]( p% C' e4 d另一方面,反过来就很难了。把非形式化的证明转化为形式化证明是非常耗费精力的工作。目前在英国帝国理工学院,教授 Kevin Buzzard 正在主导一个大型计划,要把费马大定理完全形式化。这是一个庞大的工程,需要数百名数学家、持续数年,才能手工完成。通过这种对比,你就能看出两者难度的差别。* @8 E; b5 X0 j1 r" f
, K. C( P, w. v' {; F% WTarun:我最后一个问题是:除了千禧年难题(Millennium Prize Problems),你希望 Aristotle 或它的后继模型去解决什么问题? i V6 J: j- y. L% K. D! R2 |, q9 t; {) W N7 X
千禧年难题太显而易见了,比如黎曼猜想、P=NP 这些,大家都在讨论。但你有没有什么「个人的执念问题」?如果它被解决了,你会觉得「好,这就是我最大的成就」。* K4 s# |# ^+ D5 }+ b
. B- p3 t' A. g+ X" d& i) bVlad:好,那就不说黎曼猜想了。 & E6 O K% j$ m7 Z) R: F3 t! _$ T8 B+ h( a2 C/ M9 n; v Tarun:对,那太显而易见了。 6 Y( y% b% [8 G$ ^' [5 J: n$ g6 q Vlad:但其实我还是挺喜欢黎曼猜想的(笑)。如果换一个例子,我觉得做一个「善意版的 HAL 9000」会很酷。我很想打造一个航天器的逻辑核心和控制中心,当然前提是它不会像电影里那样失控、自己起飞。 / F0 J7 g2 I I) Z0 j& b" X$ u x6 Y0 ]1 S2 PHaseeb:呃……你确定这是你想告诉大家的例子吗? " @! l, B. Y r $ l8 {1 s" F4 G1 d. ?* c$ UVlad:(笑)对,我的意思是要一个可以形式化验证的航天器控制系统。一个真正「善意的 AI」。我们确实需要一个可靠的控制核心。我觉得最初的目标确实是分开的,但现在开始出现重叠。比如 智能合约验证。 : S" D6 p- m+ z7 e 6 E. w/ I8 O: D; y: U4 p7 z智能合约本质上是运行在 Solidity、Rust 等语言上的一段相对独立的代码。我们必须确保一些基本性质,比如合约不能停摆、不能出现「双重支付」等问题。因为一旦出错,可能导致数亿美元的损失,这已经有过惨痛案例。而目前,智能合约公司几乎只能依赖人工审计——花几十万甚至上百万美元,请外部公司逐行检查代码。8 _ B% `5 ]" Y
9 v, g4 Z7 I) [
所以在加密领域,我觉得一旦形式化验证变得可行,它会非常有力量。还有很多其他场景,比如需要复杂数学计算的地方——保证金计算、期权定价等等。这些都是错误成本极高的软件。因此我认为,金融服务业,以及医疗、汽车、航天、机器人等行业,其实都非常适合用形式化验证。* J+ E$ i5 c/ s( [1 v2 `' f) ~