Online algorithms or Approximation algorithms

Stream: Is there code for X?

[davidkipstar]

I am interested in proving competitive ratios for online algorithms.
The direction should go towards prophet inequalities, secretary problem from game theory.
Is there any ground work done or work in progress for that topic?

[Shreyas Srinivas]

Currently none

[Shreyas Srinivas]

But I think it’s easier to work on online algorithms if you have established a baseline of discrete probability lemmas for sequences of random variables. I suspect mathlib will have some of this stuff

[Shreyas Srinivas]

Approximation algorithms is a whole different ball game. Once you are in the realm of sequential algorithms, life gets messy. But some of us (one person from the Isabelle side) are looking to write sequential algorithms in lean, porting them over from Isabelle. Separately there is an effort to formalise distributed graph algorithms (think LOCAL model)

[Shreyas Srinivas]

Feel free to DM me for details