The rapid development of artificial intelligence technology requires reliable theoretical support for key breakthroughs. Mathematics is the foundation of all science and technology, and mathematical logic is the intersection of mathematics and logic, using mathematical methods to describe logical problems. Mathematical logic has a profound impact on computer science, and artificial intelligence cannot do without computers and mathematics. Therefore, the theory of mathematical logic is the foundation of artificial intelligence technology. Breaking through technological bottlenecks requires strengthening the research and learning of fundamental theoretical knowledge. Propositional calculus is an introductory content in mathematical logic, which forms predicate calculus on the basis of propositional calculus, forming first-order logic and further developing higher-order logic. Propositional calculus forms various systems based on different rule systems. In this paper, the theorem proving auxiliary tool Coq is used to formally describe the Na system and Hilbert system of propositional calculus, and explore their equivalence relationship, providing a formal verification process.