OpenAI 辅助提出稀疏 0–1 矩阵射影平面行列式界，提供 98 模块 Lean 封闭证明工件

John Tripodo 于 10 月 22 日提交稀疏二元矩阵行列式研究：对密度参数 r=3,…,14 提出明确的 affine-exponential 行列式上界，在总 1 元素数 e≤rn 下取得射影平面 incidence matrices 对应的指数率并刻画取等情形，不要求逐行/列度数均匀。该研究披露 OpenAI 工具深度参与证明工程和精确计算，伴有有限实标量证书、无界度数尾项控制与 98 模块冻结 Lean 工件。作者明确说明没有外部专门数学审查，也不声称最近一次 fresh Lean compilation 已完成；不能把工件存在直接升级成 Radar 的独立复现结果。