  The Frankl's conjecture, formulated in 1979. and still open, states that in
every family of sets closed for unions there is an element contained in at
least half of the sets. FC-families are families for which it is proved that
every union-closed family containing them satisfies the Frankl's condition
(e.g., in every union-closed family that contains a one-element set {a}, the
element a is contained in at least half of the sets, so families of the form
{a} are the simplest FC-families). FC-families play an important role in
attacking the Frankl's conjecture, since they enable significant search space
pruning. We present a formalization of the computer assisted approach for
proving that a family is an FC-family. Proof-by-computation paradigm is used
and the proof assistant Isabelle/HOL is used both to check mathematical
content, and to perform (verified) combinatorial searches on which the proofs
rely. FC-families known in the literature are confirmed, and a new FC-family is
discovered.
