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