English
Total sum over non-uniform parts (weighted by sizes) is strictly less than ε times a quadratic expression in |A| and |P.parts|, under A nonempty and G uniform at ε.
Русский
Сумма по неоднородным частям (взвешенная по размерам) строго меньше ε на квадратичную функцию от |A| и |P.parts|, при A непустом и G однородном при ε.
LaTeX
$$sum_nonUniforms_lt' (hA : A.Nonempty) (hε : 0 < ε) (hP : P.IsEquipartition) (hG : P.IsUniform G ε) : ∑ i ∈ P.nonUniforms G ε, (#i.1 * #i.2 : 𝕜) < ε * (#A + #P.parts) ^ 2$$
Lean4
/-- **Conway's 99-graph problem** (from https://oeis.org/A248380/a248380.pdf)
can be reformulated as the existence of a strongly regular graph with params (99, 14, 1, 2).
This is an open problem, and has no known proof of existence. -/
axiom conway_99 : ∃ α : Type*, ∃ (g : SimpleGraph α), IsSRGWith G 99 14 1 2
