The Data Exchange with Ben Lorica
AIがコードを書く時代、誰が正しさを証明するのか
When AI Writes the Code, Who Proves It Works?
Lean の生みの親である Leo de Moura 氏が、AI による自動形式化（auto-formalization）で形式検証が身近になりつつあると語った回。機械検証可能な証明がテストでは得られない「バグがないこと」の保証を与え、人間の役割は仕様やプロパティの記述へ移るという見方を示した。数学・エージェント・物理・金融など応用領域や、信頼の限界（モデルの忠実性、カーネル）も議論された。