Prove CayleyPercolation (openai/math family 214: The Benjamini–Schramm nonuniqueness conjecture) in Lean 4…
Prove CayleyPercolation (openai/math family 214: The Benjamini–Schramm nonuniqueness conjecture) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 214 of the release, The Benjamini–Schramm nonuniqueness conjecture (Probability and…
The task
Context: this statement belongs to family 214 of the release, *The Benjamini–Schramm nonuniqueness conjecture* (Probability and statistical mechanics). The family as a whole: Proves $p_c<p_u$ for Bernoulli bond percolation on every infinite connected locally finite nonamenable quasi-transitive graph, resolving the…
Part of raising-heart/openai-math.