Formalizing Factorization in Monoids and Noetherian Rings.

This thesis focuses on the formalization of basic topics in commutative algebra\ud using the proof assistant Isabelle. This written exposition will provide an\ud overview of the work that was completed to formalize the following objectives\ud in Isabelle:\ud 1. Define a Noetherian ring using three di!erent characterizations.\ud 2. Show the existence of factorization in a Noetherian domain.\ud 3. Show the uniqueness of factorization in a principal ideal domain.\ud 4. Lay the ground work needed to prove unique factorization in K[x1, ..., xn],\ud where K is a UFD.\ud Chapter 1 provides a brief introduction to formalization and a detailed outline\ud of the five theory files that were formalized for this project. Chapter 2\ud explains the fundamentals of formalization in Isabelle and serves as a reference\ud guide to the formal work completed for my thesis. In Chapters 3 through 7, we\ud explore the outlined mathematical concepts in greater detail. In each of these\ud five chapters we will define and prove the results that were formalized in each\ud of the theory files. This exposition ends with a few closing remarks about this\ud project and ideas for future development in Isabelle, using the work from this\ud thesis. After the exposition an appendix is provided that gives all of the Isabelle\ud file that were produced for this project.Mathematic