四臂 polyomino 得到完整分类；AI-assisted proof development 并由 Lean 4 覆盖全参数范围

Angel Ivanov Raychev 对从单个方格向四个方向添加直臂得到的 polyomino 进行完整分类，覆盖 rectangle、half-strip、bent strip、quadrant、strip、half-plane、plane 以及 rep-tiling 能力。论文把周期构造、几何 obstruction 与有限 symbolic certificates 结合起来，并给出覆盖所有自然数四元组的 Lean 4 development；摘要同时记录后续 proof development 与 formalization 使用了 AI 辅助。