Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Transitive Union-Closed Families

view this post on Zulip Email Gateway (Feb 01 2025 at 13:29):

From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,

Angeliki Koutsoukou-Argyraki and Larry Paulson have formalized a recent advancement on Frankl’s conjecture.

Transitive Union-Closed Families

by Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

We formalise a proof by Aaronson, Ellis and Leader showing that the Union-Closed Conjecture holds for the union-closed family generated by the cyclic translates of any fixed set.

https://www.isa-afp.org/entries/Transitive_Union_Closed_Families.html

Enjoy!

Last updated: Mar 09 2025 at 12:28 UTC