# Uniform influence and sharp thresholds for graph and hypergraph properties

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A Sharp Threshold Bound for Monotone Graph Properties](../../preprints/A-Sharp-Threshold-Bound-for-Monotone-Graph-Properties-September-25-2026/paper.pdf)

## Scope

The Friedgut–Kalai sharp-threshold conjecture concerns how quickly a nontrivial increasing graph property appears in the independent-edge random graph. For every $n\ge2$, every such property invariant under vertex relabeling, and $0<\varepsilon<1/2$, the formalization proves that the edge-probability interval between probabilities $\varepsilon$ and $1-\varepsilon$ has width at most $2^{19}\log(1/(2\varepsilon))/(\log n)^2$. The constant is uniform over the graph property, $n$, and $\varepsilon$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Sharp threshold width for monotone graph properties | [SharpThreshold.lean](../ComparatorChallenges/SharpThreshold.lean) |