FrenzyMath 通过人机协作 agents 完成 Laver function 结果的 sorry-free Lean 形式化并修正原证明

FrenzyMath 报告完成 Renrui Qi 关于 Laver function 的大型 Lean 形式化：在 I3 公理下，其增长超过相关 fast-growing hierarchy 阈值，从而总性不能在 PA 中证明。项目使用基于 Opus 4.8 的专用 agents 与持续人工引导，公开仓库约 36k 行；文章称目标结果及依赖 sorry-free、通过 comparator，并且形式化过程发现并反馈了原稿中的若干可修正问题。