{"id":"bfd8306b-2e20-4cfd-b063-3b55a145b182","arxiv_id":"2504.13454","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"Every ideal family of sets is average rare: the average vertex degree is at most half the number of hyperedges, with a formal Lean 4 proof.","lead":"This paper proves that every 'ideal' set family, a downward-closed collection containing the full ground set, satisfies the average rarity condition, meaning its elements appear in at most half the sets on average. The authors back the proof with a Lean 4 formalization, making it a machine-checked result in an area connected to Frankl's union-closed sets conjecture.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The induction proof of Theorem 4.1 is mathematically sound; the load-bearing caveat is that the advertised Lean 4 certificate is not independently verifiable from the preprint because the displayed code is incomplete and the repository has no pinned commit or build log.","rationale":"The reader's mathematical weakest-assumption analysis concerned whether deletion and contraction preserve ideal families; after checking the definitions, those lemmas are sound, so I do not regard that as a live flaw. The reader's rationale also flagged the unverifiable formalization, and that is the concern I consider load-bearing for the paper's advertised Lean 4 contribution. Since the human proof of Theorem 4.1 appears correct and the formalization issue is exactly what motivated the CONDITIONAL verdict, my stress-test pass does not change the reader's verdict. I would keep the condition: the theorem is accepted, but the machine-checked formalization should be made reproducible with a pinned commit and build log before the formal-proof claim is taken as fully evidenced.","tokens_in":12369,"tokens_out":10734,"duration_ms":98712,"concrete_test":"Clone https://github.com/kashiwabarakenji/frankl_lean at a pinned commit, build it with a documented Lean 4 toolchain via `lake build`, and in the file containing `ideal_average_rarity` run `#print axioms ideal_average_rarity` to confirm the result does not depend on `sorry`, `admit`, or unsafe axioms; if the command lists only classical axioms such as `Classical.choice` or `propext`, the formalization claim is confirmed.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I checked the core mathematical argument and did not find a flaw. Lemma 2.3 and Lemma 2.4 hold under the paper's 'downward-closed except U' definition: deletion adds U\\{v} only after ensuring all proper subsets are already present, and contraction is ideal exactly when {v} is a hyperedge, which Lemma 4.1 supplies in the degree-at-least-two case. The induction algebra in Section 4 also checks out, including the two subcases for whether U\\{v} is a hyperedge. Lemma 2.2 is slightly under-specified, but if the ground set U is mapped to the global maximal non-ground hyperedge M and v is chosen outside M, the claimed injection is valid; the potential collision with a non-ground hyperedge M∪{v} would contradict the maximality of M. Thus no mathematical obstruction to Theorem 4.1 is apparent. The genuine load-bearing concern is about the formalization claim made in the title and abstract. Section 5 explicitly says the Lean code is a 'concept proof' rather than executable code, contains a `sorry` for `geq2`, and refers to a GitHub repository without a commit hash, toolchain version, or build log. As a result, a reader cannot currently confirm that `ideal_average_rarity` is a fully checked Lean theorem with no remaining `sorry` or `admit`. This does not weaken the human proof, but it means the advertised machine-checked contribution is unverified from the preprint alone.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":12663,"tokens_out":6682,"duration_ms":61296,"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":[{"comment":"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.","section":"Section 5, Listing 3 and Section 1.3"}],"minor_comments":[{"comment":"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":"Section 2.2, Lemma 2.2"},{"comment":"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":"Section 2.3, Lemma 2.4"},{"comment":"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":"Section 4, paragraph before the case deg_F(v) ≥ 2"},{"comment":"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":"Section 5, Listings 1 and 2"},{"comment":"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":"Section 5, Listings 4 and 5"},{"comment":"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":"Section 1.3 and Section 5"},{"comment":"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.","section":"Section 5, repository URL"}],"recommendation":"major_revision","confidential_remarks":"The mathematical core of the paper is sound, and the induction proof of Theorem 4.1 is correct as far as I can verify. The main risk is not the mathematics but the overclaiming of a verified Lean 4 formalization: the displayed code is explicitly incomplete and contains a `sorry`, and the repository is not pinned. If the authors can provide a complete, buildable Lean 4 project with the main theorem checked and no `sorry`, the formalization claim becomes credible. Otherwise, the title, abstract, and Section 1.3 should be revised to present the Lean 4 material as a proof sketch rather than a verified certificate. The result itself is a modest but valid contribution to the averaging literature on Frankl's conjecture."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat'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.\n\nThe 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.\n\nWho 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.","headline":"A correct small theorem with a solid human proof; the Lean 4 formalization is claimed but not independently verifiable from the preprint as written.","tokens_in":13186,"tokens_out":3119,"would_cite":true,"duration_ms":27924,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["05D05","05C65","03B35"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["union-closed sets conjecture","intersection-closed families","average rarity","ideal families","normalized degree sum","deletion and contraction minors","formal proof","Frankl's conjecture"],"falsifier":"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.","tokens_in":12162,"feed_emoji":"⚖️","tokens_out":11302,"duration_ms":93580,"temperature":0.7,"pith_summary":"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.","feed_headline":"Every ideal family passes the averaging test for Frankl's conjecture","feed_subtitle":"The paper proves their normalized degree sum is always non-positive, so each has a rare vertex.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines the deletion, contraction, and trace minor operations and establishes that they preserve intersection-closed families; the ideal-family minor lemmas are built on these operations.","marker":"[12]"},{"why":"The public repository containing the complete formal proof that is the verification artifact for the paper's claim that the theorem is machine-checked.","marker":"[13]"},{"why":"Supplies the interactive theorem prover used to verify the formal proof.","marker":"[20]"},{"why":"Sets out the averaging approach to Frankl's conjecture that motivates the normalized degree sum and average rarity condition.","marker":"[7]"}],"fun_headline_variants":["Lean 4 proof: every ideal family is average rare","Formalized: all ideal families pass the averaging test","Average rarity proven for all ideal families, machine-checked","Ideal families always have a rare vertex, now proven stronger","Machine-verified: ideal families satisfy average rarity"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Lean 4 proof: every ideal family is average rare","Formalized: all ideal families pass the averaging test","Average rarity proven for all ideal families, machine-checked","Ideal families always have a rare vertex, now proven stronger","Machine-verified: ideal families satisfy average rarity"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001266,"raw_usage":{"total_tokens":5222,"prompt_tokens":1022,"completion_tokens":4200,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":638,"completion_tokens_details":{"reasoning_tokens":4120}},"tokens_in":638,"tokens_out":4200,"duration_ms":24281,"temperature":1.0,"reasoning_tokens":4120,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T12:08:41.894272+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Hachimori and K","cited_arxiv_id":null,"evidence_quote":"Defines the deletion, contraction, and trace minor operations and establishes that they preserve intersection-closed families; the ideal-family minor lemmas are built on these operations."},{"cited_title":"Kashiwabara, Formal proof of a problem of ideal famil ies by Lean 4, GitHub","cited_arxiv_id":null,"evidence_quote":"The public repository containing the complete formal proof that is the verification artifact for the paper's claim that the theorem is machine-checked."},{"cited_title":"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","cited_arxiv_id":null,"evidence_quote":"Supplies the interactive theorem prover used to verify the formal proof."},{"cited_title":"Cz´ edli, M","cited_arxiv_id":null,"evidence_quote":"Sets out the averaging approach to Frankl's conjecture that motivates the normalized degree sum and average rarity condition."}],"review_version":1}