| Artificial intelligence research is the hotspot and frontier direction of current scientific and technological development,and it is particularly important to consolidate the basic theory of artificial intelligence.The mathematical theorem machine proof is a profound manifestation of the basic theory research of artificial intelligence.Theoretical machine proof mainly refers to the use of computer technology to realize the mathematical proof In order to realize the mechanization of mental work in mathematical reasoning.In recent years,with the development of computer technology,some proof tools Coq,Isabelle and HOL have appeared one after another,and the computerized formal proof of mathematical theorems has made great progress.This thesis gives a formal description of the basic definitions of sets,functions,and topology based on the proof auxiliary tool Coq,and makes the necessary preparations for constructing a formal system framework of connectivity in the topology space.On this system,the topology invariance in the topology space is studied The nature,that is,connectivity.Complete the formal proof of the theorems related to the connectivity of the topological space.All the descriptions and proofs of the theorem are compiled using Coq.The process fully reflects the interactivity,reliability,and intelligence of Coq. |
