PROVED (LEAN): the site labels the problem proved with a Lean qualification, crediting Koizumi with the trapezoid question and the two triangle variants, recorded on the Koizumi claim page (2025); the cyclic quadrilateral (yes) and the polygon with congruent sides (no) are on the Kovač–Predojević claim page (2024). The statement asks five questions, listed as the problem's parts; four are answered yes and the convex polygon with congruent sides no. Because the parts differ in polarity, the standing derived from the two partial claims records an answer rather than the proof the label names. The Lean proof the label refers to is a third-party development, linked from both pages and under Formalization, which this corpus has not built.