# A Formal Analysis of RANKING

## TL;DR

This paper provides a formal correctness proof for the RANKING algorithm in online bipartite matching, revealing a gap in previous combinatorial proofs and highlighting challenges in formalising graphical arguments.

## Contribution

It presents the first formal proof of RANKING's correctness, identifying and addressing a gap in existing combinatorial proofs.

## Key findings

- Identified a gap in all prior combinatorial proofs of RANKING
- Formalised the correctness proof of RANKING
- Highlighted difficulties in formalising graphical arguments

## Abstract

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.

---
Source: https://tomesphere.com/paper/2302.13747