La creciente importancia de la formalización basada en la demostración de teoremas en matemáticas e informática destaca la necesidad de formalizar teorías matemáticas fundamentales. En este trabajo, empleamos el demostrador de teoremas interactivo Coq para formalizar metódicamente el lenguaje, la semántica y la sintaxis de la lógica proposicional, un aspecto fundamental del razonamiento matemático y la construcción de pruebas. Construimos cuatro sistemas de axiomas de estilo Hilbert y un sistema de deducción natural para la lógica proposicional, y establecemos sus equivalencias a través de pruebas meticulosas. Además, proporcionamos pruebas formales para meta-teoremas esenciales en lógica proposicional, incluyendo el Teorema de Deducción, el Teorema de Sonoridad, el Teorema de Completitud y el Teorema de Compacidad. Importante, presentamos una prueba formal exhaustiva del Teorema de Completitud en este documento. Para reforzar la prueba del Teorema de Completitud, también formalizamos conceptos relacionados con mapeos y cardinalidad, y entregamos una prueba formal del teorema de Cantor-Bernstein-Schröder. Además, diseñamos tácticas Coq automatizadas explícitamente diseñadas para el sistema de inferencia de lógica proposicional delineado en este estudio, lo que permite la verificación automática de todas las tautologías, todos los teoremas internos y la mayoría de las inferencias sintácticas y semánticas dentro del sistema. Esta investigación aporta una biblioteca Coq versátil y reutilizable para la lógica proposicional, presentando una base sólida para numerosas aplicaciones en matemáticas, como la expresión y verificación precisas de propiedades en programas de software y circuitos digitales. Este trabajo tiene una importancia particular en los dominios de la formalización matemática, la verificación de la seguridad de software y hardware, y en el mejoramiento de la comprensión de los principios del razonamiento lógico.