Lean-checked proofs for OEIS A153772 and A266928

Elementary proofs and Lean formalizations of two assertions in OEIS: the third-largest starting value at a fixed first hitting time of 1 for the usual Collatz map (A153772), and the exact exceptional family for a least-semiprime-divisor variant (A266928). The conjectures are attributed to Markus Sigg and Michel Lagneau. The project uses Lean 4.33.1 and a fixed mathlib revision. This version is a draft for review; no historical priority or external acceptance is claimed. OpenAI Codex assisted with the arguments, formalization, searches, and writing under the direction of Pascal Le Clech. The usual Collatz conjecture is not settled by these results. The note and original documentation are licensed under CC BY 4.0; the original Lean code and verification script are licensed under MIT. Third-party material retains its own terms. The archive contains the statement review, bounded prior-work searches, and reproducibility instructions.