发表机构
Royal Holloway, University of London; University of Cambridge（伦敦大学皇家霍洛威学院; 剑桥大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究在 Isabelle/HOL 中形式化了并闭猜想特例的 2021 年证明，通过概述证明并展示代码片段，展示了数学推理在形式语言中的清晰表达。
AI 中文摘要
Aaronson、Ellis 和 Leader 于 2021 年对并闭猜想的一个特例给出了证明，该证明已在证明助手 Isabelle/HOL 中形式化。我们的讨论包括概述他们的证明，并展示 Isabelle 版本证明的片段，以说明数学推理在形式语言中能被清晰呈现的程度。
英文摘要
A 2021 proof of a special case of the Union-Closed Conjecture, by Aaronson, Ellis and Leader, has been formalised in the proof assistant Isabelle/HOL. Our discussion involves sketching their proof and displaying snippets from the Isabelle version of the proof, illustrating the extent to which mathematical reasoning can be rendered clearly in a formal language.
CommentsSubmitted to J Automated Reasoning
