我們在 Lean 中正式化了 FRI 的健全性，使用了 @HarmonicMath 和 Claude Code。 - 由 @nico_mnbl 和合作者進行的 FRI 分析 - 由 @pirapira 轉換為 Lean 證明 🔥

小知識：這是出於對 Math, Inc 公布的 FRI 證明的好奇心而開始的，正式化了簡潔證明和線性代數： ...這很好，但與我們預期的 FRI 安全實際界限相差甚遠！