某中心学者、卡耐基梅隆大学计算机科学教授Marijn Heule与柏林工业大学同事Manfred Scheucher合作，利用自动推理技术解决了匈牙利-澳大利亚数学家Esther Szekeres近100年前提出的几何难题。

该问题被传奇数学家Paul Erdős称为"幸福结局问题"，要求确定平面上不共线的若干点中，能保证存在n个点构成不包含其他点的凸多边形的最小点数。Heule团队证明30个点足以保证存在空凸六边形。

研究团队采用SAT求解器（一种能判断长逻辑约束链可满足性的自动推理工具）生成证明。为应对数百TB规模的证明数据，Heule与某机构自动推理团队开发了新型流式证明检查基础设施，将验证开销从原来的100-200%降低至10%左右。这项创新可应用于软件安全验证、硬件验证等领域。

研究过程中，团队突破性地将六边形分解为三角形进行验证，发现只需检查每个六边形的"内三角形"即可推导整体结论。SAT求解器不仅完成证明，还反馈了可优化的问题表述方式，最终生成的超长证明通过新型验证系统快速确认了有效性。

该成果展示了自动推理技术在解决复杂数学问题中的强大能力，其开发的流式验证架构将显著提升各类形式化验证任务的效率。