A Formalisation of a Special Case of the Union-Closed Conjecture in Isabelle/HOL
arXiv:2609.20876
Abstract
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.
Submitted to J Automated Reasoning