A Formalisation of a Special Case of the Union-Closed Conjecture in Isabelle/HOL
In the authors' words
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.
Main resultLimitation the authors admit
Appeared: Monday, September 21. arXiv. Preprint, not yet peer-reviewed.
Authors' comment: Submitted to J Automated Reasoning