Lean-assisted QA
13 available views. Missing equivalent Lean tasks remain gaps, not borrowed proof credit. Reference answers stay closed until you choose to read them.
From atomic balance to reversibility
sogb-001 · 4 rubric points · public-dev
Open questionPL descent: the sign of the contraction factor
sogb-002 · 4 rubric points · public-dev
Open questionA quadratic envelope from one midpoint
sogb-003 · 4 rubric points · public-dev
Open questionRecovering joint probability mass from one marginal
sogb-015 · 4 rubric points · public-dev
Open questionA quadratic gradient through the actual sphere differential
sogb-016 · 4 rubric points · public-dev
Open questionAveraging a conditional event-error bound
sogb-017 · 4 rubric points · public-dev
Open questionGluing the right joint law before applying Minkowski
sogb-018 · 4 rubric points · public-dev
Open questionWhy a global Lipschitz function bounds its supporting vectors
sogb-019 · 4 rubric points · public-dev
Open questionWhy retaining one coordinate and conditionally resampling the other is invariant
sogb-021 · 4 rubric points · public-dev
Open questionFrom a selected-curve chord inequality to its first-order bound
sogb-022 · 4 rubric points · public-dev
Open questionAn actual gradient flow: objective decay with the zero-curvature branch
sogb-023 · 4 rubric points · public-dev
Open questionFrom Gibbs Poincaré to a directional covariance bound
sogb-025 · 4 rubric points · public-dev
Open questionFrom the Boolean cube to compact Gaussian log-Sobolev
sogb-028 · 4 rubric points · public-dev
Open question