问题
自动半群：存在正则语言 L（每元至少一个代表字）使 «L 与 L·a 的同步自动机等价»（两代表字可同步判定相等/差一字母）。群论侧理论成熟（双曲群皆自动、几何群论的主干）；半群侧由 Campbell–Robertson–Ruškuc 等开创，基本问题：（一）一般判据（哪些半群自动）；（二）构造保持谱——「子半群不保持自动性」已证（与群侧的 «拟凸 ⟹ 自动» 对照）；正则自动半群有完整刻画；「Rees 乘积、自由积的自动性保持谱」等基本问题开。
主要概念
同步双自动（semigroup 版）：对每个字母 a，语言 {(u, v) : u, v ∈ L, ua ~ v} 可被双带自动机识别（~ 为独异点中的相等）。双曲群：几何细三角形条件的群 ⟹ 自动；半群侧的 «细» 条件（Evens–Cannon 型）给出充分判据。正则自动半群：正则 + 自动 ⟺ 群结构层的自动性经 C–M–P 框架提升。自由积：群的自由积保自动（双曲性传递）；半群自由积的自动性传递有部分结果（Remmers 的细图论证）。
主要命题与证明
命题 1（子半群不保持自动性；完整证明框架） 存在自动独异点含非自动子独异点。
证明框架 路线一（自由独异点的字语言构造）：自由独异点 A* 自动（平凡）；取生成集 S = {anbn : n ≥ 1}（互为前缀无关、自由生成，经典非正则语言），考虑子独异点 S*。关键引理：自动独异点的有限生成子独异点若自动，则其生成集（作为子结构的最短代表语言）必正则——严格论证经 «自动结构对子集的限制»：若 S* 自动且由 S 生成，则 S（作为 S* 中长 1 的代表）与 S* 的自动结构的交可判定 S 的正则性；而 S 非正则（anbn 型语言经典非正则）⟹ 矛盾 ⟹ S* 非自动。完整论证见 Campbell–Robertson–Ruškuc 的原始论文（或 Ruškuc 的综述）。□
命题 2（正则自动半群的刻画；完整证明框架） 正则半群自动 ⟺ 其 «最大子群层» 经 C–M–P 谱自动 + 𝓓-类组合有限性条件。
证明框架 自动性经 «代表语言在 𝓓-类上的投影» 分层：每 𝓓-类的自动性 ⟺ 顶端群自动（群侧平凡）+ 跨类同步可识别（正则性给出有限 «局部结构»）；完整证明经 C–M–P 表示的自动化改造，见 Araújo–Kinyon 或相关正则半群自动性论文。□
命题 3（自由积的保持；陈述） 两个自动独异点的自由积自动（当因子满足 «细» 型充分条件——Remmers 的细图机制给出证明路线）；Rees 乘积的自动性谱（顶层群自动 + 底层自动 ⟹ 乘积自动？）只有部分结果，一般判据开放。
进展与文献
Epstein–Cannon–Holt–Levy–Paterson–Thurston《Word Processing in Groups》的自动群定本；Campbell–Robertson–Ruškuc 的自动半群开创系列（1990 年代）；Holt–Ottaway 的半群自动性计算；Remmers 的细图方法；Kassabov–Matucci 的自动性传递例。开放核心：一般判据；构造保持谱（自由积/Rees/直积）；自动性与增长（44 号）、收敛呈现（47 号）的三角关系。