Formalizing Competitive Analysis of Online Algorithms in Lean 4
The project aims to formalize competitive analysis of online algorithms using the Lean 4 theorem prover. Online algorithms are algorithms that process input piece-by-piece in a serial fashion without knowledge of future inputs. Competitive analysis is a widely used framework for evaluating the performance of such algorithms by comparing them to an optimal offline algorithm that has complete knowledge of the input sequence in advance.
Current goals
The project is at the design stage. The goal is to develop a Lean 4 formalization of request answer games, defining online and offline algorithms, defining competitive ratio and all its variants.
Author: Maciej Pacut