1. FormalConjectures
  2. Mathoverflow
  3. «10799»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Optimal monotone families for the discrete isoperimetric inequality

References:

namespace Mathoverflow10799open Finset Real

Start with a set $X={1,2,...,n}$ of $n$ elements and the family $2^X$ of all subsets of $X$. For a real number $p$ between zero and one, we consider a probability distribution $\mu_p$ on $2^X$ where the probability that $i \in S$ is $p$, independently for different $i$'s. Thus for $p=1/2$ we get the uniform probability distribution.

For $S \subseteq {0, \ldots, n-1}$, its probability is $p^{|S|} (1-p)^{n - |S|}$.

noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ := p ^ #S * (1 - p) ^ (n - #S)

For $p = 1/2$, the $p$-biased measure is the uniform distribution: $\mu_{1/2}(S) = (1/2)^n$ for every $S \subseteq [n]$.

All goals completed! 🐙

The $p$-biased measure of a family $\mathcal F \subseteq 2^{[n]}$, i.e. $\mu_p(\mathcal F) = \sum_{S \in \mathcal F} \mu_p(S)$.

noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ := ∑ S ∈ F, μ p S

Given a family $F$, for a subset $S$ of $X$, we write $h(S)$ as the number of subsets $T$ in $X$ such that (1) $T$ differs from $S$ in exactly one element (2) Exactly one set among $S$ and $T$ belongs to $F$.

def boundaryCount (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : ℕ := (Finset.univ.filter fun i : Fin n ↦ Xor (S ∈ F) (symmDiff S {i} ∈ F)).card

Test lemma showing that boundaryCount is equivalent to counting subsets $T$ that differ from $S$ in exactly one element and exactly one of $S, T$ belongs to $F$.

n:ℕF:Finset (Finset (Fin n))S:Finset (Fin n)h_cancel:∀ (A : Finset (Fin n)), symmDiff S (symmDiff S A) = Ah_inj:Function.Injective fun i ↦ symmDiff S {i}T:Finset (Fin n)hcard:#(symmDiff S T) = 1hxor:Xor (S ∈ F) (T ∈ F)i:Fin nhi:symmDiff S T = {i}hT:T = symmDiff S {i}⊢ ∃ a, Xor (S ∈ F) (symmDiff S {a} ∈ F) ∧ symmDiff S {a} = T n:ℕF:Finset (Finset (Fin n))S:Finset (Fin n)h_cancel:∀ (A : Finset (Fin n)), symmDiff S (symmDiff S A) = Ah_inj:Function.Injective fun i ↦ symmDiff S {i}T:Finset (Fin n)hcard:#(symmDiff S T) = 1hxor:Xor (S ∈ F) (T ∈ F)i:Fin nhi:symmDiff S T = {i}hT:T = symmDiff S {i}⊢ Xor (S ∈ F) (symmDiff S {i} ∈ F) rwa [n:ℕF:Finset (Finset (Fin n))S:Finset (Fin n)h_cancel:∀ (A : Finset (Fin n)), symmDiff S (symmDiff S A) = Ah_inj:Function.Injective fun i ↦ symmDiff S {i}T:Finset (Fin n)hcard:#(symmDiff S T) = 1i:Fin nhxor:Xor (S ∈ F) (symmDiff S {i} ∈ F)hi:symmDiff S T = {i}hT:T = symmDiff S {i}⊢ Xor (S ∈ F) (symmDiff S {i} ∈ F)n:ℕF:Finset (Finset (Fin n))S:Finset (Fin n)h_cancel:∀ (A : Finset (Fin n)), symmDiff S (symmDiff S A) = Ah_inj:Function.Injective fun i ↦ symmDiff S {i}T:Finset (Fin n)hcard:#(symmDiff S T) = 1i:Fin nhxor:Xor (S ∈ F) (symmDiff S {i} ∈ F)hi:symmDiff S T = {i}hT:T = symmDiff S {i}⊢ Xor (S ∈ F) (symmDiff S {i} ∈ F) at hxor

The edge-boundary of $F$ is the expectation of $h(S)$ (according to $\mu_p$) over all subsets $S$ of $X$. It is denoted by $I^p(F)$.

noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ := ∑ S : Finset (Fin n), μ p S * boundaryCount n F S

A family $F$ of subsets of $2^X$ is monotone increasing if when $S$ belongs to $F$ and $T$ contains $S$ then $T$ also belongs to $F$. (Monotone increasing families also also called "filtes" and "up-families".) From now on we will restrict our attention to the case of monotone increasing families.

This is Mathlib's IsUpperSet applied to the coercion of $\mathcal F$ to a set, using the fact that ≤ on Finset is ⊆.

abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop := IsUpperSet (↑F : Set (Finset (Fin n)))

We say that a family is optimal for $\mu_p$ if the isoperimetric inequality (IR) is sharp up to a multiplicative constant $1000 \log (1/p)$.

Since the lower bound from (IR) is $$\frac{\mu_p(\mathcal F) \cdot \log(1/\mu_p(\mathcal F))}{p \cdot \log(1/p)},$$ multiplying by $1000 \log(1/p)$ gives the condition $$I^p(\mathcal F) \le \frac{1000}{p} \cdot \mu_p(\mathcal F) \cdot \log \frac{1}{\mu_p(\mathcal F)}.$$

noncomputable def IsOptimal {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : Prop := let m := μFamily p F edgeBoundary n p F ≤ 1000 * Real.log (1 / p) * (m * Real.logb p m / p)

Problem: For every monotone increasing family $F$, given an interval $[s,t]$ of real numbers so that $t/s > 1000 \log n$ we have some $p$ in the interval $[s,t]$ so that $F$ is optimal with respect to $\mu_p$.

This was a "missing lemma" in the work of Kahn and Kalai on threshold behavior of monotone properties. The related Kahn–Kalai conjecture was settled by Park and Pham.

This conjecture is false without the additional assumption $\mu_t(F) = 1/2$. A counterexample was found by Shlomo Perles (April 7, 2026).

@[category research solved, AMS 5 60, formal_proof using formal_conjectures at "https://github.com/mo271/formal-conjectures/blob/408f53dc0856c0882a5e77acd24fc83b978f0bc9/FormalConjectures/Mathoverflow/10799.lean#L252"] theorem mathoverflow_10799 : answer(False) ↔ ∀ (n : ℕ) (_ : 2 ≤ n) (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F) (s t : ℝ) (_ : 0 < s) (_ : s ≤ t) (_ : t < 1) (_ : t / s > 1000 * Real.log n), ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F := ⊢ False ↔ ∀ (n : ℕ), 2 ≤ n → ∀ (F : Finset (Finset (Fin n))), IsMonotoneIncreasing F → ∀ (s t : ℝ), 0 < s → s ≤ t → t < 1 → t / s > 1000 * log ↑n → ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F All goals completed! 🐙

Conjecture 7 from Kahn–Kalai 2006: a fixed-1000 variant of the original conjecture, with the additional assumption that $t$ is the critical probability for $F$, namely $\mu_t(F) = 1/2$.

This variant is false by a counterexample due to Sahar Diskin and Uri Kreitner; see the MathOverflow discussion and the counterexample note. Their construction was adapted to this exact Formal Conjectures statement and formalized in Lean by Kenta Kitamura (KitaKen1).

@[category research solved, AMS 5 60, formal_proof using lean4 at "https://github.com/KitaKen1/kahn-kalai-conjecture-7-counterexample/blob/5446d2f/lean/MO10799CounterexampleFC.lean#L2597-L2604"] theorem mathoverflow_10799.variants.kahn_kalai_conjecture_7 : answer(False) ↔ ∀ (n : ℕ) (_ : 2 ≤ n) (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F) (s t : ℝ) (_ : 0 < s) (_ : s ≤ t) (_ : t < 1) (_ : μFamily t F = 1 / 2) (_ : t / s > 1000 * Real.log n), ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F := ⊢ False ↔ ∀ (n : ℕ), 2 ≤ n → ∀ (F : Finset (Finset (Fin n))), IsMonotoneIncreasing F → ∀ (s t : ℝ), 0 < s → s ≤ t → t < 1 → μFamily t F = 1 / 2 → t / s > 1000 * log ↑n → ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F All goals completed! 🐙

Weaker version proven by Kahn–Kalai: the same conclusion holds when $1000 \log n$ is replaced by $C_\varepsilon , n^\varepsilon$ for every fixed $\varepsilon > 0$.

@[category research solved, AMS 5 60] theorem mathoverflow_10799.variants.weak_kahn_kalai : ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ (n : ℕ) (_ : 2 ≤ n) (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F) (s t : ℝ) (_ : 0 < s) (_ : s ≤ t) (_ : t < 1) (_ : t / s > C * (n : ℝ) ^ ε), ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F := ⊢ ∀ ε > 0, ∃ C > 0, ∀ (n : ℕ), 2 ≤ n → ∀ (F : Finset (Finset (Fin n))), IsMonotoneIncreasing F → ∀ (s t : ℝ), 0 < s → s ≤ t → t < 1 → t / s > C * ↑n ^ ε → ∃ p, s ≤ p ∧ p ≤ t ∧ IsOptimal p F All goals completed! 🐙

Now a famous isoperimetric relation asserts that (IR) $I^p(F) \ge \frac{1}{p} \mu_p(F) \log_p \mu_p(F)$ This relation is true for every family $F$ and every $p$. It is especially famous and simple when $p=1/2$ and $\mu_p(F)=1/2$. In this case, it says that given a set of half the vertices of the discrete cube $2^X$, the number of edges between $F$ and its complement is at least $2^{n-1}$.

Note on translation: We use Real.logb p m to represent the logarithm base $p$ directly. The factor of $p$ in the denominator (equivalent to $1/p$ in front) is consistent with the definition of IsOptimal used in the counterexample proof.

@[category textbook, AMS 5 60] theorem discrete_isoperimetric_inequality (n : ℕ) (p : ℝ) (hp : 0 < p) (hp' : p < 1) (F : Finset (Finset (Fin n))) : let m := μFamily p F edgeBoundary n p F ≥ m * Real.logb p m / p := n:ℕp:ℝhp:0 < php':p < 1F:Finset (Finset (Fin n))⊢ let m := μFamily p F; edgeBoundary n p F ≥ m * logb p m / p All goals completed! 🐙

The $p$-biased measure is a probability distribution: it sums to $1$ over all subsets. This is the binomial identity $(p + (1-p))^n = 1$.

n:ℕp:ℝh:∑ s, p ^ #s * (1 - p) ^ (n - #s) = (p + (1 - p)) ^ n⊢ (p + (1 - p)) ^ n = 1 All goals completed! 🐙

The measure of the full power set is $1$.

@[category test, AMS 5] theorem μFamily_univ (n : ℕ) (p : ℝ) : μFamily p (Finset.univ : Finset (Finset (Fin n))) = 1 := n:ℕp:ℝ⊢ μFamily p univ = 1 n:ℕp:ℝ⊢ ∑ S, μ p S = 1 All goals completed! 🐙

The boundary count is zero for the empty family (no set is in $\mathcal F$).

@[category test, AMS 5] theorem boundaryCount_empty (n : ℕ) (S : Finset (Fin n)) : boundaryCount n ∅ S = 0 := n:ℕS:Finset (Fin n)⊢ boundaryCount n ∅ S = 0 All goals completed! 🐙

The edge boundary is zero for the empty family.

@[category test, AMS 5] theorem edgeBoundary_empty (n : ℕ) (p : ℝ) : edgeBoundary n p ∅ = 0 := n:ℕp:ℝ⊢ edgeBoundary n p ∅ = 0 All goals completed! 🐙

The boundary count is zero for the full family (every set is in $\mathcal F$).

@[category test, AMS 5] theorem boundaryCount_univ (n : ℕ) (S : Finset (Fin n)) : boundaryCount n Finset.univ S = 0 := n:ℕS:Finset (Fin n)⊢ boundaryCount n univ S = 0 All goals completed! 🐙

The edge boundary is zero for the full family.

@[category test, AMS 5] theorem edgeBoundary_univ (n : ℕ) (p : ℝ) : edgeBoundary n p Finset.univ = 0 := n:ℕp:ℝ⊢ edgeBoundary n p univ = 0 All goals completed! 🐙end Mathoverflow10799