Conjectures 平台 miner 解出悬置 40 余年的 Erdős 问题 579，结果经 Lean 验证

数学众包平台 Conjectures.io 宣布，其 miner 找到了至少自 1983 年以来悬而未决的 Erdős 问题 579 的解，该结果否证了原猜想。结果显示图可以在避免八面体图 K₂,₂,₂ 的同时保持稠密，且其最大独立集占全部顶点的比例趋于消失。完整结果已在该平台通过 Lean 形式化验证。