A Machine Proof Of The Twin Prime Conjecture For The Conditional Independence Of The Peano Axiom Group

The discipline of artificial intelligence is one of the major scientific and technological development strategies of the country at present and in the future,and is a very key discipline in the development of computer science.Theorem machine proof is an important branch of the artificial intelligence discipline,which can give more rigorous and accurate verification of the establishment of computer programs,which is a profound embodiment of the basic theory of artificial intelligence.With the rapid development of computer science,the interactive theorem proof tool Coq is widely used in the field of theorem proof,it has a strong mathematical model and good scalability,and has so far assisted in the completion of a number of internationally renowned theorems.This thesis takes Mr.Zhang Herui’s book "Fundamentals of Modern Generations" and Mr.Wang Shiqiang’s paper "Some Connections between the Goldbach Conjecture and PA:A Logical Discussion of Some Number Theory Problems(Ⅱ.)" as the formal content.Mr.Wang Shiqiang’s paper uses the compactness theorem in model theory to re-examine the properties of primes,mutual primes,twin prime conjectures from the perspective of the median class of modern generation numbers,integer rings,and modular residual class rings,and proves that for a certain equivalence of the twin prime conjectures of natural number systems and some equivalence of the first-order Peano axiom group,the former is logically independent of the latter.With the help of the interactive theorem proof tool Coq,this thesis formalizes its contents and completes the machine proof of the conditional independence of the twin prime conjecture for the axiom group of Peano.The main tasks are as follows:1.Starting from the definition of sets,we complete the formal definition of the basic concepts of equivalence relations,sets and other basic concepts,complete the formal description of the properties of groups,rings,integer rings,prime elements,modular residual rings and integer parts of the group ring theory,and realize the preliminary construction of the framework of the machine proof system.2.We implement the coq formalization of the twin prime conjecture and the Peano axiom group,construct and formalize one of the remaining rings of integer rings suitable for the twin prime conjecture and another kind of residual ring of integer rings that do not fit the twin prime conjecture.3.We use the compactness theorem in model theory to construct the.correlation model,give a formal description of the independence of the condition,and realize the machine proof of the theorem.