One-sample matroid prophet inequalities
From OpenAI Aftermath
One-sample matroid prophet inequalities concern online selection under a matroid constraint when the value distributions are unknown and each element supplies only one independent sample in advance: can an online rule guarantee a constant fraction of the expected offline optimum, independent of the matroid? A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims such a constant guarantee on every finite matroid, even against an almighty adversary who chooses the arrival order after seeing all samples, all values and the rule's random seed. The collection includes a Lean formalization of this statement. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- For a single choice with known distributions the sharp reward fraction is 1/2, a bound that Krengel and Sucheston credit to Garling, and Kleinberg and Weinberg proved the same guarantee for arbitrary matroids with known distributions.
- Azar, Kleinberg and Weinberg developed the limited-information framework of samples and reduced single-sample prophet algorithms to order-oblivious secretary algorithms; Rubinstein, Wang and Weinberg obtained the optimal one-sample fraction 1/2 for a single choice, and Caramanis and coauthors developed single-sample guarantees under structured constraints.
- For the matroid secretary problem of Babaioff, Immorlica and Kleinberg, Lachish and Feldman, Svensson and Zenklusen obtained guarantees with a doubly logarithmic loss in the rank, the latter also giving a one-sample prophet inequality with the same loss; Fu and coauthors obtained a constant fraction for arbitrary matroids against an almighty adversary using a polylogarithmic number of samples per element, and Feldman, Svensson and Zenklusen improved the sample dependence.
The original result
- Claim. Theorem 1.1 of One sample suffices for matroid prophet inequalities against an almighty adversary states that there is a measurable online selection rule, independent of the value distributions, such that for every finite labelled matroid and independent nonnegative samples and values with matching laws and integrable offline optimum, against every measurable arrival order depending on the matroid, the laws, the samples, the values and the seed, the expected reward is at least 2−310 times the expected offline optimum. The manuscript states that its accounting section proves the stronger constant 2−293, that no running-time guarantee is claimed, and it derives a secretary consequence in which an adversary rearranges the labels after a random observation prefix.
- Method, as described: both results follow from a guarantee for fixed weights: after a random set of weights is revealed and its labels sacrificed, the expected minimum reward over all arrival orders is a constant fraction of the fixed optimum; a one-sample simulation glues samples and values on a random set of labels.
- Sources. The manuscript One sample suffices for matroid prophet inequalities against an almighty adversary at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves a one-sample matroid prophet inequality with expected reward at least 2−310 times the expected offline optimum, with the rule and a finite seed law depending only on the labelled matroid and the arrival order allowed to depend measurably on all samples, values and the seed, and a supporting hidden-vector selection result with worst-order guarantee 2−293. The Comparator statements are
MatroidProphet.leanandMatroidSecretary.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full", with no review note, and describes the hidden-vector selection result with constant 2−293 as an extra supporting statement. It records sandboxed Comparator passes for both challenges. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 (latest commit 11 October 2026) | R. Shea, shea256/matroid-prophet-inequality (GitHub, commit 8cd1395) |
Extension (quantitative) | A project developing quantitative refinements of the manuscript's construction in the same model: one independent sample per label, unknown independent value distributions, prefix feasibility and an adversary seeing every sample, value and seed bit. Its current result states a guarantee C* > (35/32)·2−31 times the expected offline optimum, given by an exact rational certificate, after successive versions starting from 2−36 announced on 10 October 2026. | The README describes the result as a written proof with same-agent verification and states that independent mathematical review and formalization are pending; finite checks accompany the proof, and it makes no priority claim. The work was developed with Codex assistance. |
| 2026-10-10 | cert-machine, openai/math lane K: MatroidProphet and MatroidSecretary | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the solutions of both challenges, in 277 s and 415 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list MatroidProphet or MatroidSecretary, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-16 | J. Jardine, Lattice24, referee review in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. The reviewer states that it read every section of the source, skimming the secretary corollary, and checked the one-sample simulation, the rounding step, the candidate-mass lemma, the density expansion and its generator budget, feasibility through nested layers and the reverse-exposure filtration step by step. | Part of an audit of the collection's manuscripts that the audit describes as complete. The review is published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
