A Formalisation of a Special Case of the Union-Closed Conjecture in Isabelle/HOL
En palabras de los autores
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.
Resultado principalLimitación que admiten los autores
Apareció: lunes, 21 de septiembre. arXiv. Preprint, todavía sin revisión por pares.
Comentario de los autores: Submitted to J Automated Reasoning