Certifying the Decidability of the Word Problem in Monoids at Large

Explore a conference presentation that introduces a comprehensive toolbox for the Rocq proof assistant designed to verify the decidability of the word problem for finitely presented monoids. Learn how this innovative approach addresses the fundamental challenge that while the word problem for monoids is generally undecidable, having decision procedures for specific monoids has significant practical applications. Discover the toolbox's methodology, which heavily relies on proofs by reflection guided by external oracles to handle computationally intensive verification processes. Examine the successful application of this approach to several large presentations from mathematical literature and understand how it was scaled to handle a massive database of one million 1-relation monoids. Gain insights into the unique considerations required for the Rocq formalization to ensure formal proofs could be verified within reasonable time constraints when dealing with such enormous datasets. Understand the theoretical foundations of the word problem in monoid theory and see how formal verification techniques can be applied to algebraic decision problems at unprecedented scales.