we-solve (beta)

CS-146 · computer science · mathematics · Algorithmic game theory · Graph theory and combinatorics

One-sample matroid prophet selection

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every finite known matroid with mutually independent nonnegative weights and one independent sample from each unknown marginal law, can a distribution-free online selector achieve one fixed positive fraction of expected offline optimum, even when the measurable arrival order depends on both samples, all realized weights and the selector’s random seed? The expected optimum is assumed finite and no running-time restriction is imposed.

Short English statement

For every finite known matroid with mutually independent nonnegative weights and one independent sample from each unknown marginal law, can a distribution-free online selector achieve one fixed positive fraction of expected offline optimum, even when the measurable arrival order depends on both samples, all realized weights and the selector’s random seed? The expected optimum is assumed finite and no running-time restriction is imposed.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-146-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-146

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 111; 2026-09-23).

One-sample matroid prophet selection

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 111; 2026-09-23), the asserted result is that one sample per element gives a constant-factor matroid prophet rule even when the ordering adversary sees all values and the entire random seed, with guarantee $2^{-310}$.

Mathematical statement of the claimed result

Manuscript 1.
For any known finite labeled matroid $M=(E,\mathcal I)$, let $\operatorname{OPT}_M(v)=\max_{I\in\mathcal I}\sum_{e\in I}v_e$. Take mutually independent nonnegative $S_e,V_e$, each pair identically distributed with arbitrary law $D_e$, and assume $\mathbb E\operatorname{OPT}_M(V)<\infty$. An online rule sees exactly the sample vector $S$ before arrivals and an independent seed $R$. For every measurable arrival permutation allowed to depend on $M,(D_e),S,V,R$, it claims irrevocable independent selection $A$ with \[ \mathbb E\sum_{e\in A}V_e\ge2^{-310}\mathbb E\operatorname{OPT}_M(V). \] The rule does not know the value laws or future order.

The secretary consequence fixes nonnegative weights $w$ before randomness. A rule draws an independent full seed and random prefix length, observes and rejects that prefix of a uniform permutation; then an adversary knowing the full weights, prefix and complete seed may order the suffix. The accepted independent set still satisfies \[ \mathbb E\sum_{e\in A}w_e\ge2^{-293}\operatorname{OPT}_M(w). \] The adversary may not change the prefix distribution or select the weights after seeing it.

Outline of the argument

For manuscript 1 (family 111; 2026-09-23), reverse exposure turns samples into safe hidden-vector evidence. Geometric weight layers and nested flats guide greedy feasible selections, while rank expansion and nominal-path guards pay for all later choices uniformly over arrival orders.

Formal verification

For manuscript 1 (family 111; 2026-09-23), OpenAI lists Lean statements for this assertion: one sample per element gives a constant-factor matroid prophet rule even when the ordering adversary sees all values and the entire random seed, with guarantee $2^{-310}$.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are MatroidProphet.lean, MatroidSecretary.lean.

Their named declarations include OAI.MatroidProphet.Assigned.hidden_vector, OAI.MatroidProphet.Assigned.one_sample, OAI.MatroidProphet.Assigned.secretary, OAI.MatroidProphet.one_sample.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →