Un importante avance en álgebra geométrica en los últimos años es el nuevo sistema conocido como geometría de puntos, que trata los puntos como objetos directos de operaciones y simplifica considerablemente el proceso de razonamiento geométrico. En este documento, proporcionamos una descripción formal completa de la arquitectura de la teoría de geometría de puntos y ofrecemos una verificación formal rigurosa y confiable de la teoría de geometría de puntos basada en el demostrador de teoremas Coq. Simultáneamente, también se diseñan una serie de tácticas para ayudar en la demostración de proposiciones geométricas. Basado en la arquitectura teórica y tácticas de prueba, se construye un sistema de prueba de máquina de geometría de puntos interactivo, universal y escalable, PointGeo. En este sistema, se puede demostrar cualquier declaración geométrica resoluble mediante geometría de puntos, junto con información legible sobre el procedimiento de la solución. Además, los usuarios pueden ampliar la base de reglas agregando reglas confiables según sea necesario para ciertos problemas. La implementación del sistema amplía la biblioteca de recursos de Coq sobre álgebra geométrica, que se convertirá en una base de investigación significativa para los campos de álgebra geométrica, ciencias de la computación, educación matemática y otros campos relacionados.