Database of 1-relation monoid word problem decidability proofs

The 1-relation monoid word problem decidability proof database is a collection of certificates specifying the decidability of the word problem in many 2-generated 1-relation monoids with relation length at most 10. Decidability of the word problem for all 1-relation monoids is a longstanding open problem in the field of semigroup theory, and this database constitutes the largest enumeration of small instances of the word problem to date. This is an early version of the database and it is being actively worked on as part of a larger effort by the authors to produce an encyclopedia of 1-relation monoid presentations.A Rocq formalization of the theory underpinning the certificates in the database, as well as a method of converting the SA certificates to formal Rocq proofs was developed in order to improve the trustworthiness and reproducibility of the database. The conversion script is available as part of this dataset, for the Rocq formalization, see github.com/hivert/MonoidPresentation/ as well as an upcoming article: Cirpons, R., Hivert, F., Mahboubi, A., Melquiond, G., Mitchell, J. D., Smith, F. Certifying the decidability of the word problem in monoids at large. To appear. In: Proceedings of the CPP (2026). For more details on the contents of the database see the files README.md and SA_certificate_format.md. For an introduction to the word problem in 1-relation monoids, we recommend the following survey article on the matter: Nyberg-Brodda, CF. The word problem for one-relation monoids: a survey. Semigroup Forum 103, 297–355 (2021). https://doi.org/10.1007/s00233-021-10216-8单关系幺半群（1-relation monoid）字问题（word problem）可判定性证明凭证数据库，是一套收录多份凭证的数据集，这些凭证明确了诸多关系长度不超过10的二元生成（2-generated）单关系幺半群的字问题可判定性。 所有单关系幺半群的字问题可判定性，是半群理论（semigroup theory）领域中长期存在的公开未解问题；本数据库是迄今为止针对小规模字问题实例规模最大的枚举集合。 本数据库尚处于早期版本，目前正由作者团队积极迭代开发，作为构建“单关系幺半群表示百科全书”这一更大研究项目的组成部分。 为提升本数据库的可信度与可复现性，研究团队开发了针对数据库中凭证所依托理论的Rocq形式化验证（Rocq formalization），以及一套将SA凭证（SA certificates）转换为标准化Rocq证明的方法。本数据集附带了该转换脚本；关于Rocq形式化验证的详情，可访问github.com/hivert/MonoidPresentation/，相关内容也将在一篇即将发表的论文中呈现： Cirpons, R.、Hivert, F.、Mahboubi, A.、Melquiond, G.、Mitchell, J. D.、Smith, F. 《大规模幺半群字问题可判定性的凭证验证》，已接收，收录于《CPP 2026会议论文集》（Proceedings of the CPP (2026)）。 如需了解本数据库内容的更多细节，请参阅README.md与SA_certificate_format.md文件。若想了解单关系幺半群字问题的相关入门知识，我们推荐以下综述文章： Nyberg-Brodda, C.F. 《单关系幺半群的字问题：综述》，《Semigroup Forum》第103卷，第297–355页（2021年），DOI: 10.1007/s00233-021-10216-8。