Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre grafos titulado Properties of random graphs – subgraph containment.
Sus autor es Lars Hupel (de la Univ. Politécnica de Munich).
Su resumen es
Random graphs have been introduced by Erdös and Rényi in [1]. They describe a probability space where, for a fixed number of vertices, each possible edge is present with a certain probability independent from other edges, but with the same probability for each edge. They study what properties emerge when increasing the number of vertices, or as they call it, “the evolution of such a random graph”. The theorem which we will prove here is a slightly different version from that in the first section of that paper.
Here, we are interested in the probability that a random graph contains a certain pattern, for example a cycle or a clique. A very high edge probability gives rise to perhaps too many edges, which is usually undesired since it degrades the performance of many algorithms, whereas a low edge probability might result in a disconnected graph. The central theorem determines a threshold probability such that a higher edge probability will asymptotically almost surely produce a random graph with the desired subgraph.
The proof is outlined in [2, §11.4] and [3, §3]. The work is based on the comprehensive formalization of probability theory in Isabelle/HOL and on a previous definition of graphs in a work by Noschinski [4]. There, Noschinski formalized the proof that graphs with arbitrarily large girth and chromatic number exist. While the proof in this paper uses a different approach, the definition of a probability space on edges turned out to be quite useful.
El trabajo se ha publicado en Archive of Formal Proofs
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.