This chapter examines the complexities surrounding axiomatic strength in proof assistants like Agda, discussing challenges in understanding their foundational aspects due to limited documentation. It also highlights experiences with various theorem provers such as Lean and MetaMath, emphasizing the importance of understanding different systems to appreciate their unique methodologies. The chapter advocates for the translation and interoperability of proofs across systems to foster a unified framework for mathematical verification.