L-砖块与有界合取半格：Isabelle/HOL 中的形式化
计算机科学中的逻辑
2025-09-25 v1 交换代数
摘要
我们在 Isabelle/HOL 中对等价于 L-砖块与有界合取半格对象部分的完整形式化，采用 AI 辅助的方法论，将大型语言模型作为推理助手贯穿于证明开发过程。该等价性最初由 Cangiotti、Linzi 和 Talotti 在其关于正交模组半格和量子逻辑相关的超复合结构研究中建立。我们的形式化严格验证了主要理论结果，并演示了建立此等价性的变换具有互为逆变的性质。该开发展示了多值代数运算的数学深度，以及在处理复杂形式化项目中运用 AI 增强式交互式定理证明的潜力。
引用
@article{arxiv.2509.19854,
title = {L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL},
author = {Alessandro Linzi},
journal= {arXiv preprint arXiv:2509.19854},
year = {2025}
}