First-order logic, as a pillar of mathematical foundations, includes completeness as one of its fundamental theorems. Gödel’s Completeness Theorem reveals the equivalence between syntactic reasoning and semantic reasoning in first-order logic, establishing a solid foundation for formal logical systems. This paper constructs a machine proof system for first-order logic using the interactive proof assistant Coq, systematically completing the formalization of Gödel’s Completeness Theorem. To address key challenges in the proof process, we propose an innovative constant replacement method that ensures an ample supply of unused constant symbols in the Henkin construction by doubling the indices of constants appearing in a set, effectively solving technical challenges in formal verification. This research not only confirms the correctness of Gödel’s Completeness Theorem from a machine-verifiable perspective but also provides reliable tools and methods for formal logic theory research.