L3 · Multi-step proof and diagnosis
Mathematical QA
- From atomic balance to reversibility · natural-language: L3 / lean: L3
- PL descent: the sign of the contraction factor · natural-language: L3 / lean: L3
- Wasserstein symmetry without an optimal plan · natural-language: L3
- Why a sphere gradient is a projected ambient gradient · natural-language: L3
- Null atoms in a random-scan balance proof · natural-language: L3
- A quadratic gradient through the actual sphere differential · natural-language: L3 / lean: L3
- Averaging a conditional event-error bound · natural-language: L3 / lean: L3
- Why a global Lipschitz function bounds its supporting vectors · natural-language: L3 / lean: L2
- From subgradient energy to a finite-run best iterate · natural-language: L3
- Why retaining one coordinate and conditionally resampling the other is invariant · natural-language: L3 / lean: L2
- From a selected-curve chord inequality to its first-order bound · natural-language: L3 / lean: L3
- One null set for every event, or a different null set for each event? · natural-language: L3
- From Gibbs Poincaré to a directional covariance bound · natural-language: L3 / lean: L3
- Tensorizing a two-point entropy bound without losing the flip constant · natural-language: L3
- From the Boolean cube to compact Gaussian log-Sobolev · natural-language: L4 / lean: L3
- Chewi Optimization Exercise 3.2: the balanced gradient step · natural-language: L3
Structural graph QA
No structural question in this slice yet.
Difficulty is provisional. Each question discloses its own current editorial status; empirical calibration remains pending.