We describe a formal correctness proof of RANKING, an online algorithm for online bipartite matching. An outcome of our formalisation is that it shows that there is a gap in all combinatorial proofs of the algorithm. Filling that gap constituted the majority of the effort which went into this work. This is despite the algorithm being one of the most studied algorithms and a central result in theoretical computer science. This gap is an example of difficulties in formalising graphical arguments which are ubiquitous in the theory of computing.

翻译：我们描述了RANKING（一种用于在线二分图匹配的在线算法）的形式化正确性证明。我们的形式化工作的一个成果是，它揭示了该算法所有组合证明中存在一个漏洞。填补这一漏洞构成了本项工作的大部分努力，尽管该算法是理论计算机科学中研究最为深入的算法之一和核心成果。这一漏洞是形式化图形论证过程中困难的典型例子，而图形论证在计算理论中无处不在。