Mathematical Theory Exploration in Theorema: Reduction Rings
Alexander Maletzky

TL;DR
This paper presents the first formalization and verification of the theory of Gr"obner bases in reduction rings within Theorema, enabling automated computation and exploration of algebraic structures.
Contribution
It introduces a comprehensive formalization of reduction rings and Buchberger's algorithm in Theorema, integrating proof and computation for the first time.
Findings
Formalization of Gr"obner bases in reduction rings completed
Verified correctness of Buchberger's algorithm within Theorema
Developed tools for theory exploration and proof automation
Abstract
In this paper we present the first-ever computer formalization of the theory of Gr\"obner bases in reduction rings, which is an important theory in computational commutative algebra, in Theorema. Not only the formalization, but also the formal verification of all results has already been fully completed by now; this, in particular, includes the generic implementation and correctness proof of Buchberger's algorithm in reduction rings. Thanks to the seamless integration of proving and computing in Theorema, this implementation can now be used to compute Gr\"obner bases in various different domains directly within the system. Moreover, a substantial part of our formalization is made up solely by "elementary theories" such as sets, numbers and tuples that are themselves independent of reduction rings and may therefore be used as the foundations of future theory explorations in Theorema.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
