This chapter explores the foundational differences between proof assistants Metamath Zero and Deductee, with a focus on their structural and operational methodologies. It highlights the efficiency of proof checking in Metamath Zero through directed acyclic graphs, and contrasts this with the complexities of type checking in dependent type theories. Additionally, the chapter discusses the challenges of translating axioms into Lean proofs and emphasizes the importance of semantic preservation across different proof systems.