The Formal Proof Of Geometric Theorem In Coq Case Study

Artificial intelligence is a new technology science for simulating and extending human intelligence.As a branch of computer science,it aims to understand the essence of intelligence and produces a new intelligent machine which can simulate human intelligence to think and make decisions.The research in this field includes robots,language recognition,image recognition,natural language processing and expert system.Since the birth of artificial intelligence,its theory and technology have become increasingly mature,and the field of its application has been expanding.The outstanding manifestation of artificial intelligence in the field of mathematical mechanization is machine proof.The purpose of machine proof is to realize the proof of theorem by means of computer and auxiliary proof tool.Current auxiliary certification tools include Coq,Isabelle,HOL Light,etc.Coq is currently one of the most mainstream auxiliary proof procedure in the world.It originated in France.Its core is inductive construction calculus,which also makes Coq have a strong rigor and reliability.Moreover,Coq's interactive proof environment also brings great convenience to users.At present,people have used Coq to prove numerous mathematical theorems,the most famous of which is the machine proof of"four-color theorem"completed by Gonthier and Werner in 2005.After that,Gonthier gave the machine verification of the"classification theorem of finite simple groups"in 2012,and Hales and others completed the computer proof of "Kepler's conjecture" in 2015.These achievements have made Coq,an auxiliary certification tool,more and more influential in academia.Elementary geometry is an important research topic in the field of mathematics.Since Euclid founded elementary geometry,the development of geometry has been inseparable from elementary geometry.The projective geometry and non Euclidean geometry were all developed on the basis of elementary geometry.Yang Lu Theorem is a elementary geometry theorem put forward by Mr.Yang Lu,a famous mathematician in China.As an extension of Kepler Theorem,Yang Lu Theorem has been included in the Dictionary of Geometry compiled by Mr.Iwata,Japan.It is a very representative theorem and has a great influence abroad.In the preparation of the formal proof of Yang Lu's theorem,we can not only construct a series of concepts of elementary geometry,but also introduce the concepts of analytic geometry such as coordinates and vectors.Finally,we can describe and prove Yang Lu's theorem through the concepts and properties constructed.With the aid of the auxiliary proof tool Coq,this paper completes the construction of elementary geometric concepts such as point,line,surface,angle and the concepts of vector and coordinate.Finally we gives the complete description and machine proof of Yang Lu's theorem.The innovative point of this paper is to use the interactive auxiliary proof tool Coq to carry out machine proof,and this is the first mechanization of Yang Lu's theorem.It is an attempt to formalize the construction of elementary geometric system.We can make more attempts on this basis and develop more different geometric systems in the future.