∑math20

Theoretical computer science · Result 111

One-sample matroid prophet inequalities against an almighty adversary

1 paperLean

For every finite matroid known in advance, gives a distribution-independent online rule using one independent sample per element and earning a universal constant fraction of the expected offline optimum. Values are independent and nonnegative, with finite expected optimum. The guarantee holds even when the arrival-order adversary sees all samples, values, and the rule's entire random seed; no polynomial-time implementation is asserted.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversary

One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversary

OpenAI · September 23, 2026

We prove that one independent sample per element suffices for a constant-competitive prophet inequality on every finite matroid. The guarantee holds even when the arrival-order adversary observes all samples, all online values, and the algorithm's entire random seed. The rule needs no description of the value distributions and achieves the absolute competitive ratio \(2^{-310}\).

Read PDF Download Source

Cite
@misc{OAI:One-Sample-Suffices-for-Matroid-Prophet-Inequalities-against-an-Almighty-Adversary-September-23-2026,
  author = {{OpenAI}},
  title = {{One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversary}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/One-Sample-Suffices-for-Matroid-Prophet-Inequalities-against-an-Almighty-Adversary-September-23-2026/final.pdf}{OAI:One-Sample-Suffices-for-Matroid-Prophet-Inequalities-against-an-Almighty-Adversary-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves a one-sample matroid prophet inequality with expected reward at least \(2^{-310}\) times the expected offline optimum. Each element has one independent sample paired with an identically distributed nonnegative online value, and all coordinates are independent. The rule and finite seed law depend only on the labeled matroid; choices are irrevocable and feasible after every prefix. The arrival order may depend measurably on all samples, values, and the seed, and only the offline optimum must be integrable.

A supporting hidden-vector selection result for fixed nonnegative matroid weights gives expected worst-order reward at least \(2^{-293}\) times the optimum, again with a finite seed law and prefix feasibility.

Comparator links

ResultComparator statement
One-sample matroid prophet inequality against an almighty adversaryMatroidProphet.lean
Hidden-vector matroid selection with worst-order guaranteeMatroidSecretary.lean

Scope note on GitHub →