On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4

Kenji Kashiwabara; Masahiro Hachimori

REVIEW 1 major objections 7 minor 28 references

On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4

T0 review · 1 major / 7 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper proves that every ideal family is average rare: its normalized degree sum is always non-positive, so it contains a vertex that appears in at most half the sets.

desk verdict A correct small theorem with a solid human proof; the Lean 4 formalization is claimed but not independently verifiable from the preprint as written. read the letter →

arxiv 2504.13454 v1 pith:EN45G7WO submitted 2025-04-18 math.CO

Masahiro Hachimori , Kenji Kashiwabara This is my paper · ORCID

classification math.CO MSC 05D0505C6503B35

keywords union-closedsetsconjectureintersection-closedfamiliesaveragerarityidealnormalizeddegreesumdeletionandcontractionminorsformalproofFrankl's

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Frankl's union-closed sets conjecture can be reformulated for intersection-closed families: any family that contains the ground set $U$ and the empty set and is closed under intersections should have a rare vertex, one that lies in at most half the sets. This paper proves a stronger averaging statement for a restricted class called ideal families, which are intersection-closed families that contain $\emptyset$ and $U$ and are downward-closed for every set except $U$ itself. The main theorem shows that the normalized degree sum $\mathrm{NDS}(\mathcal{F}) = 2\,\mathrm{TSH}(\mathcal{F}) - |U|\,|\mathcal{F}|$ is non-positive for every ideal family, where $\mathrm{TSH}(\mathcal{F})$ is the sum of the sizes of all sets in $\mathcal{F}$; this is exactly the condition that the average vertex appears in at most half the sets. Because average rarity implies the existence of a rare vertex, this gives a new infinite class of families that cannot serve as counterexamples to Frankl's conjecture. The proof is an induction on the ground set using deletion and contraction minors, and the whole argument is formally verified by an interactive theorem prover.

What carries the argument

The carrying object is the normalized degree sum $\mathrm{NDS}(\mathcal{F}) = 2\,\mathrm{TSH}(\mathcal{F}) - |U|\,|\mathcal{F}|$, because non-positivity is precisely average rarity. The proof runs on two minor operations: deletion $\mathcal{F}.\mathrm{del}'\,v$, which keeps only sets not containing $v$ and adds the new ground set $U\setminus\{v\}$, and contraction $\mathcal{F}.\mathrm{cont}\,v$, which removes $v$ from every set containing it. Lemmas 2.3 and 2.4 show that both operations preserve ideal families, so the induction hypothesis applies to the smaller ground sets. The proof then splits into the four cases where $\{v\}$ and $U\setminus\{v\}$ are or are not hyperedges; in each case the same decomposition identities for $\mathrm{NDS}$ connect the whole family to its two minors, and the rare-vertex inequality $2\deg_{\mathcal{F}}(v)-|\mathcal{F}|\le 0$ supplies the final bound.

What would settle it

Compute the normalized degree sum of every ideal family on a finite ground set with at most, say, five vertices by exhaustive enumeration; any family with $\mathrm{NDS}>0$ would refute Theorem 4.1 immediately. Alternatively, find an ideal family for which $\{v\}$ is a hyperedge but the contraction $\mathcal{F}.\mathrm{cont}\,v$ fails to contain the empty set, since that would break Lemma 2.4 and the induction step.

Watch

Extended reading notes

Core claim

The central claim, Theorem 4.1, is that for every nonempty finite ground set $U$ and every ideal family $\mathcal{F}$ on $U$, the inequality $\mathrm{NDS}(\mathcal{F}) = 2\,\mathrm{TSH}(\mathcal{F}) - |U|\,|\mathcal{F}| \le 0$ holds. Since $\mathrm{TSH}(\mathcal{F}) = \sum_{v\in U} \deg_{\mathcal{F}}(v)$ by double counting, this says the average of the vertex degrees is at most half the number of sets, i.e., the family is average rare. This strengthens Lemma 2.2, which only asserts that every ideal family has a rare vertex. The induction chooses a rare vertex $v$, considers the deletion $\mathcal{F}.\mathrm{del}'\,v$ and contraction $\mathcal{F}.\mathrm{cont}\,v$, and uses Lemmas 2.3 and 2.4 to keep both as ideal families on the smaller ground set. In each of the four cases determined by whether $\{v\}$ and $U\setminus\{v\}$ are hyperedges, the normalized degree sum of $\mathcal{F}$ is written as the sum of the normalized degree sums of the minors plus a remainder bounded by the rarity inequality $2\deg_{\mathcal{F}}(v)-|\mathcal{F}|\le 0$. The entire proof is machine-checked in an interactive theorem prover.

Load-bearing premise

The load-bearing premise is that an ideal family's definition—downward-closed for every set except the ground set—guarantees the deletion and contraction minors are again ideal families; if the usual downward-closed definition were used, the contraction minor could lose the empty set, and the induction, which also needs the ground set to be finite, would break.

Editorial extensions

If this is right

Every ideal family is average rare, hence contains a rare vertex; ideal families therefore form a class of intersection-closed families that are all compatible with Frankl's conjecture.
The normalized degree sum of the full power set is exactly $0$, so the bound $\mathrm{NDS}\le 0$ is tight and ideal families can sit exactly on the average-rare boundary.
The explicit decomposition $\mathrm{NDS}(\mathcal{F}) = \mathrm{NDS}(\mathcal{F}.\mathrm{del}'\,v) + \mathrm{NDS}(\mathcal{F}.\mathrm{cont}\,v) + 2\deg_{\mathcal{F}}(v) - |\mathcal{F}|$ (with a correction when $U\setminus\{v\}$ is absent) gives a reusable induction identity for other classes of intersection-closed families that admit such minors.
The machine-checked formalization means the proof can be reused as a verified lemma in further formal work on Frankl's conjecture.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

We expect the same induction template to generalize: any intersection-closed class that always has a rare vertex and is closed under deletion and contraction on smaller ground sets should also be average rare, because the NDS decomposition only uses those two ingredients. Testing this on classes such as families with bounded rank or semimodular lattice families would be a direct extension.
The theorem shows that average rarity is not a property that needs to be proved globally from scratch for every family; a single rare vertex plus closure under minors can force the whole family to be average rare. This suggests a possible route to proving Frankl's conjecture by finding a broad class with these closure properties rather than by entropy or injection methods.
One implicit limitation is that the proof's deletion/contraction lemmas rely on the unusual definition that the ground set is exempt from downward closure. If one weakened the definition to ordinary downward-closed families containing $U$, the contraction minor could lose the empty set and the induction would fail, so the boundary of the method is exactly this class.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Two things to know. The theorem is correct and the induction proof is sound; the paper's advertised Lean 4 certificate is not something you can verify from the arXiv page, because the text itself admits the displayed code is a concept proof with a `sorry`, and the GitHub link has no pinned commit or build log.

What's new: the class of ideal families — downward-closed except the ground set, plus U — is a reasonable new subclass of intersection-closed families. Theorem 4.1, that every ideal family has NDS(F) ≤ 0 (equivalently, satisfies average rarity), is a genuine strengthening of the rare-vertex lemma. The proof by induction on |U| using deletion and contraction minors is self-contained; I checked the algebra in both subcases and it holds. Lemma 2.2's injection is sketchy but repairable, and the paper is honest that the rare-vertex property is probably known — the contribution is the average-rarity result plus its formal proof attempt.

The soft spots are mostly presentational. Section 5 is the real issue: it describes the Lean code as 'a conceptual overview rather than executable Lean 4 code' and includes `sorry` for `geq2` in the main theorem sketch. The abstract and introduction, by contrast, claim the proof 'has been rigorously validated using the Lean 4 system.' Those two statements don't match. A reader cannot currently confirm from the preprint that `ideal_average_rarity` is a fully checked Lean theorem with no remaining sorries. That doesn't undermine the human proof, but it means the machine-checked contribution is unverified as advertised. Fix: pin a commit, give the toolchain, and either remove the sorries or state plainly that the formalization is incomplete. Also, Lemma 2.2 could use one more sentence to define the injection's second case; the stress-test note's repair works.

Who this is for: people working on the averaging approach to Frankl's conjecture, and anyone interested in Lean formalization of elementary combinatorics. It's a small result, not a breakthrough, but it is correct and honestly framed (most of the time). I'd send it to a serious referee; the math deserves an outlet, and the formalization claim needs to be forced into alignment with what actually exists.

Referee Report

1 major / 7 minor

Summary. The paper defines a class of finite set families called ideal families: families F ⊆ 2^U containing both the empty set and the ground set U and downward-closed for every proper subset. The central result, Theorem 4.1, states that every ideal family on a nonempty finite ground set has non-positive normalized degree sum, NDS(F) = 2·TSH(F) − |U|·|F| ≤ 0, which is equivalent to the average rarity condition. The proof is by induction on |U|, using a rare-vertex lemma to choose a vertex v, then analyzing deletion and contraction minors of the ideal family. The paper also claims a Lean 4 formalization of the proof, presented in Section 5, with code available in a GitHub repository.

Significance. If correct, the result identifies a new, verifiably average-rare class within intersection-closed families, a stronger property than the rare-vertex condition required by Frankl's conjecture. The human proof is short, self-contained, and appears mathematically sound on its own terms; no fitted parameters or external assumptions are used. The claimed machine-checked Lean 4 proof is a potentially valuable reproducibility contribution, but as submitted the displayed code is explicitly only a 'conceptual overview' and contains an admitted `sorry`, so the formalization claim is not yet substantiated. The mathematical result is modest but meaningful for the averaging approach to Frankl's conjecture, and the proof is accessible to a broad combinatorics audience.

major comments (1)

[Section 5, Listing 3 and Section 1.3] The title, abstract, and Section 1.3 state that the proof is 'formalized and verified using the Lean 4 theorem prover,' but the manuscript does not support this claim. Listing 3 is explicitly described as 'a conceptual overview rather than executable Lean 4 code,' and it contains 'have geq2 : F.ground.card ≥ 2 := by sorry', an admitted omission. Listings 4 and 5 are lemma statements ending with ':=' and no proof term, so they are not syntactically complete Lean code. The referenced GitHub repository is not pinned to a commit and no toolchain version or build log is provided. As a result, a reader cannot verify that the theorem `ideal_average_rarity` is fully checked by Lean 4 with no remaining `sorry` or `admit`. This is a load-bearing issue for the formalization contribution; the human proof stands independently, but the advertised machine-checked certificate must either be supplied in complete, executable form with a stable repository link, or the claims in the title and abstract must be tempered.

minor comments (7)

[Section 2.2, Lemma 2.2] The proof of Lemma 2.2 is under-specified: the mapping for the ground set U should fix one maximal non-ground hyperedge M with v ∉ M, and the injectivity argument must explicitly rule out the collision case M ∪ {v} ∈ F using the maximality of M. As written, 'a maximal hyperedge' is ambiguous, since several incomparable maximal hyperedges may exist.
[Section 2.3, Lemma 2.4] The proof of Lemma 2.4 says only that the contraction minor contains the empty set; it should also verify the downward-closed-except-ground-set condition for F.cont v. This is straightforward but should be stated.
[Section 4, paragraph before the case deg_F(v) ≥ 2] The text says 'F. del′ v and F. cont v are ideal families by Lemmas 2.3 and 2.6', but the contraction minor F.cont v is Lemma 2.4, not Lemma 2.6 (the trace minor). Please correct the reference.
[Section 5, Listings 1 and 2] The displayed Lean code is incomplete: the definition of `F.degree` is not shown, and the theorem `frankl_conjecture` refers to `has_empty`, `has_univ`, and `is_closed_under_intersection` that are not defined in Listing 1 or in the surrounding text. Please include these definitions or state clearly that the listing is illustrative pseudocode.
[Section 5, Listings 4 and 5] Listings 4 and 5 contain no proof terms after the ':='; if they are intended as lemma statements rather than complete proofs, this should be stated explicitly in the caption or surrounding text. As printed, they are not valid Lean 4 code.
[Section 1.3 and Section 5] The statements 'Barring exceptional circumstances, it is reasonable to trust in the validity of the proofs' and the claim that all proofs have been 'rigorously validated using the Lean 4 system' are too strong relative to the displayed code, which includes `sorry` and is described as a concept proof. Please soften these claims to match what is actually presented.
[Section 5, repository URL] The repository URL in the text after Listing 5 is incomplete: it reads 'https://github.com/kashiwabarakenji/' while the reference [13] gives 'https://github.com/kashiwabarakenji/frankl_lean/'. Please align these and include a specific commit identifier or version.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 4.1 is proved by induction from the definition of ideal families, with no fitted parameters, renamed inputs, or load-bearing self-citations.

full rationale

The derivation chain is self-contained. Theorem 4.1 is proved by induction on |U|, using Lemma 2.2 (existence of a rare vertex) as a strictly weaker ingredient, not as the conclusion; the proof explicitly notes that this is a strengthening. The minor preservation lemmas (2.3 and 2.4) are proved directly from Definition 2.5, and the induction algebra relating NDS(F) to NDS of deletion and contraction minors is given by explicit equations rather than by definitional equivalence. The cited prior work [12] is used only to note that minors preserve intersection-closedness, which is not load-bearing for the main argument. No parameter is fitted and no quantity is renamed as a prediction. The only flagged weakness is in Section 5: the displayed Lean code is described as a 'concept proof rather than executable Lean 4 code' and contains a `sorry` for `geq2`, with the repository not pinned by a commit hash or build log in the preprint. This affects independent machine verification of the formalization claim, but it does not indicate circularity in the human proof. Overall, the mathematical derivation is independent and non-circular.

Assumptions & free parameters 0 free parameters · 3 assumptions · 1 invented entities

The proof introduces no free parameters. It relies on standard finiteness and arithmetic, and on the soundness of the Lean 4 kernel for the formalization claim. The new notion 'ideal family' is a definition, not a postulated entity with empirical content.

assumptions (3)

domain assumption The ground set U is finite and nonempty.
Stated in Section 2.1. Used for the induction on |U|, for the existence of a maximal hyperedge in Lemma 2.2, and for finite cardinal arithmetic in NDS.
standard math Standard facts about finite sets, double counting, and arithmetic over integers and naturals.
Used throughout, e.g., TSH double counting and the algebraic manipulations in Theorem 4.1's proof.
domain assumption The Lean 4 theorem prover's kernel is sound and the repository code compiles against a recent version.
The paper claims formal verification, but the preprint does not include the complete verified code or a commit hash; trust in the formalization relies on the tool and the repository contents.

invented entities (1)

Ideal family
purpose: A class of set families, downward-closed except the ground set, for which the paper proves the average rarity condition.
This is a new named mathematical object introduced in Section 2.2. It is a definition, not an empirically testable entity; its value is mathematical structure, not falsifiable prediction.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4." pith.science (2026). https://pith.science/paper/EN45G7WO

@misc{pith2026250413454,
  author       = {Pith},
  title        = {Pith review of: On the Averaging Problem of Ideal Families Related to Frankl's Conjecture with Formal Proof by Lean 4},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EN45G7WO}},
  note         = {Machine review of arXiv:2504.13454}
}

read the original abstract

Frankl's conjecture, also known as the union-closed sets conjecture, can be equivalently expressed in terms of intersection-closed set families by considering the complements of sets. It posits that any family of sets closed under intersections, and containing both the ground set and the empty set, must have a ``rare vertex'' -- a vertex belonging to at most half of the members of the family. The concept of \emph{average rarity} describes a set family where the average degree of all the elements is at most half of the number of its members. Average rarity is a stronger property that implies the existence of a rare vertex. This paper focuses on ideal families, which are set families that are downward-closed (except the ground set) and include the ground set. We present a proof that the normalized degree sum of any ideal family is non-positive, which is equivalent to saying that every ideal family satisfies the average rarity condition. This proof is formalized and verified using the Lean 4 theorem prover.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

28 extracted references · 22 canonical work pages

[1]

Abe, Strong semimodular lattices and Frankl’s conjec ture, Algebra Universalis

T. Abe, Strong semimodular lattices and Frankl’s conjec ture, Algebra Universalis. 44 (2000), 379–382

work page 2000
[2]

Alweiss, B

R. Alweiss, B. Huang, M. Sellke, Improved lower bound for Frankl’s union-closed sets conjecture (2022). arXiv:2211.11731 https://arxiv.org/abs/2211.11731

arXiv 2022
[3]

Boˇ snjak and P

I. Boˇ snjak and P. Markovi´ c, The 11-element case of Frankl’s conjecture, Electronic Journal of Combinatorics 15 (2008), R88

work page 2008
[4]

Bruhn and O

H. Bruhn and O. Schaudt, The journey of the Union-Closed S ets Conjecture, Graphs and Combinatorics 31 (2015), 2043–2074

work page 2015
[5]

Cambie, Better bounds for the union-closed sets conje cture using the entropy approach (2022)

S. Cambie, Better bounds for the union-closed sets conje cture using the entropy approach (2022). arXiv:2212.12500 https://arxiv.org/abs/2212.12500

arXiv 2022
[6]

Chase, S

Z. Chase, S. Lovett, Approximate union closed conjectur e (2022). arXiv:2211.11689 https://arxiv.org/abs/2211.11689

arXiv 2022
[7]

Cz´ edli, M

G. Cz´ edli, M. Mar´ oti and E.T. Schmidt, On the scope of averaging for Frankl’s Conjecture, Order 26 (2009), 31–48

work page 2009
[8]

Frankl, On the Union-Closed Sets Conjecture, Unpubli shed manuscript, 1979

P. Frankl, On the Union-Closed Sets Conjecture, Unpubli shed manuscript, 1979. 14

work page 1979

Show all 28 references

[9]

Gilmer, A constant lower bound for the Union-Closed Se ts Conjecture (2022)

J. Gilmer, A constant lower bound for the Union-Closed Se ts Conjecture (2022). arXiv:2202.10087 https://arxiv.org/abs/2202.10087

2022 arXiv
[10]

https://github.com/features/copilot

GitHub, GitHub Copilot. https://github.com/features/copilot
[11]

Gusakov, Formalizing the excluded minor characteri zation of binary ma- troids in the Lean theorem prover, Master Thesis, Universit y of Waterloo, 2024

A. Gusakov, Formalizing the excluded minor characteri zation of binary ma- troids in the Lean theorem prover, Master Thesis, Universit y of Waterloo, 2024. https://uwspace.uwaterloo.ca/items/d35d17be-485d-4f 60-8696-4dce7ae907bb

2024
[12]

Hachimori and K

M. Hachimori and K. Kashiwabara, Several minimality co ncepts related to Frankl’s con- jecture, Graphs and Combinatorics 40 (2024), article 130

2024
[13]

Kashiwabara, Formal proof of a problem of ideal famil ies by Lean 4, GitHub

K. Kashiwabara, Formal proof of a problem of ideal famil ies by Lean 4, GitHub. https://github.com/kashiwabarakenji/frankl_lean/
[14]

Lean Copilot: Assisting formal pro of development in Lean,

Lean Copilot Team, “Lean Copilot: Assisting formal pro of development in Lean,” Avail- able at: https://github.com/lean-dojo/LeanCopilot
[15]

LeanSearch, https://leansearch.net
[16]

Liu, Improving the lower bound for the union-closed s ets conjecture via conditionally IID coupling, 58th Annual Conference on Information Scienc es and Systems (CISS), IEEE, 2024

J. Liu, Improving the lower bound for the union-closed s ets conjecture via conditionally IID coupling, 58th Annual Conference on Information Scienc es and Systems (CISS), IEEE, 2024

2024
[17]

Mari´ c, M

F. Mari´ c, M. ˇZivkovi´ c, and B. Vuckovi´ c, Formalizing Frankl’s conjecture: FC-families (2012). arXiv:1207.3604 https://arxiv.org/abs/1207.3604

2012 arXiv
[18]

M. J. Moghaddas Mehr, A note on the Union-closed Sets Con jecture (2023) arXiv:2309.01704 https://arxiv.org/abs/2309.01704

2023 arXiv
[19]

Morris, FC-families and improved bounds for Frankl’ s conjecture, European Journal of Combinatorics 27 (2006), 269–282

R. Morris, FC-families and improved bounds for Frankl’ s conjecture, European Journal of Combinatorics 27 (2006), 269–282

2006
[20]

de Moura et al., The Lean 4 theorem prover and programm ing language, Proceedings of the 13th International Conference on Interactive Theore m Proving (ITP 2022), 2021

L. de Moura et al., The Lean 4 theorem prover and programm ing language, Proceedings of the 13th International Conference on Interactive Theore m Proving (ITP 2022), 2021. https://lean-lang.org/papers/lean4.pdf

2022
[21]

Nagel, Notes on the Union Closed Sets Conjecture (202 2)

N. Nagel, Notes on the Union Closed Sets Conjecture (202 2). arXiv:2208.03803 https://arxiv.org/abs/2208.03803

arXiv
[22]

ChatGPT, https://openai.com

OpenAI. ChatGPT, https://openai.com
[23]

Pebody, Extension of a method of Gilmer (2022)

L. Pebody, Extension of a method of Gilmer (2022). arXiv :2211.13139 https://arxiv.org/abs/2211.13139

2022 arXiv
[24]

Poonen, Union-closed families, Journal of Combinat orial Theory, Series A 59 (1992), 253–268

B. Poonen, Union-closed families, Journal of Combinat orial Theory, Series A 59 (1992), 253–268

1992
[25]

Reinhold, Frankl’s conjecture is true for lower semi modular lattices, Graphs and Com- binatorics, 16 (2000), 115–116

J. Reinhold, Frankl’s conjecture is true for lower semi modular lattices, Graphs and Com- binatorics, 16 (2000), 115–116

2000
[26]

Roberts and J

I. Roberts and J. Simpson, A note on the Union-Closed Set s Conjecture, Australasian Journal of Combinatorics 47 (2010), 265–267. 15

2010
[27]

Sawin, An improved lower bound for the union-closed s et conjecture (2022)

W. Sawin, An improved lower bound for the union-closed s et conjecture (2022). arXiv:2211.11504. https://arxiv.org/pdf/2211.11504

2022 arXiv
[28]

Yu, Dimension-free bounds for the union-closed sets conjecture

L. Yu, Dimension-free bounds for the union-closed sets conjecture. Entropy 25 (2023), 767. Funding Statement The authors have no relevant ﬁnancial or non-ﬁnancial inter ests to disclose. Data Availability Statement All formalized proofs and related Lean 4 source code used in t...

2023

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.

[1] [1]

Abe, Strong semimodular lattices and Frankl’s conjec ture, Algebra Universalis

T. Abe, Strong semimodular lattices and Frankl’s conjec ture, Algebra Universalis. 44 (2000), 379–382

work page 2000

[2] [2]

Alweiss, B

R. Alweiss, B. Huang, M. Sellke, Improved lower bound for Frankl’s union-closed sets conjecture (2022). arXiv:2211.11731 https://arxiv.org/abs/2211.11731

arXiv 2022

[3] [3]

Boˇ snjak and P

I. Boˇ snjak and P. Markovi´ c, The 11-element case of Frankl’s conjecture, Electronic Journal of Combinatorics 15 (2008), R88

work page 2008

[4] [4]

Bruhn and O

H. Bruhn and O. Schaudt, The journey of the Union-Closed S ets Conjecture, Graphs and Combinatorics 31 (2015), 2043–2074

work page 2015

[5] [5]

Cambie, Better bounds for the union-closed sets conje cture using the entropy approach (2022)

S. Cambie, Better bounds for the union-closed sets conje cture using the entropy approach (2022). arXiv:2212.12500 https://arxiv.org/abs/2212.12500

arXiv 2022

[6] [6]

Chase, S

Z. Chase, S. Lovett, Approximate union closed conjectur e (2022). arXiv:2211.11689 https://arxiv.org/abs/2211.11689

arXiv 2022

[7] [7]

Cz´ edli, M

G. Cz´ edli, M. Mar´ oti and E.T. Schmidt, On the scope of averaging for Frankl’s Conjecture, Order 26 (2009), 31–48

work page 2009

[8] [8]

Frankl, On the Union-Closed Sets Conjecture, Unpubli shed manuscript, 1979

P. Frankl, On the Union-Closed Sets Conjecture, Unpubli shed manuscript, 1979. 14

work page 1979