Rózsa：面向无预设结合律或交换律的等式蕴含问题，Lean 证书求解 SAIR 挑战 199/200 题

Georgios Kissas 于 2026 年 10 月 19 日在 arXiv 首次提交 Rózsa 论文，提出用于 SAIR Mathematics Distillation Challenge 第二阶段的 Python 等式推理求解器。任务在不预设结合律、交换律或其他代数性质的二元运算集合上，判断一条方程是否蕴含另一方程，并要求提供 Lean 可检查的证明或反例。Rózsa 通过逐步应用公理并维护推导证据搜索正向证明，同时搜索有限代数结构与一个固定无限模型以给出反例，统一导出 Lean 证书。作者报告官方主评测解出 199/200 题（99.5%），位列第六；对长链推导有效，但无限反例能力仍有限。论文结果为作者报告的挑战评测成绩，不等于 Radar 独立复跑或泛化至任意一阶代数问题。