Intuitive geometric knowledge is an origin of human civilization, just as shown by the Plimpton 322 tablet that people in the Old Babylonian period (between −1900 and −1600) already knew the rule of the right triangle i.e., the Pythagorean theorem, through various instances of right triangles, almost one thousand years before proof was given in Greek time. From the analogue view, the machine’s consciousness would be better built starting from recognizing geometric configurations, formating of geometric concepts and discovering geometric properties from observing sufficiently many examples of geometric configuration without human interference, and automated verification (or proof) of the observed geometric theorems. Indeed, machine proof of geometric theorems has been regarded as an essential subject of artificial intelligence research during the inception of artificial intelligence. In the past few decades, researchers have made significant progress in using computers to prove geometric theorems. The research work of computer proof of geometric theorems is mainly developed from the following three directions:
1) Algebraic calculation method based on coordinates;
2) Point elimination method based on geometric invariants;
3) Proving theorems by simulating human thinking the reasoning database search method.
The machine proof of geometric theorems originated in the 1950s. Tarski  proposed that most of the decision problems in elementary algebra and elementary geometry can be verified using an algebraic method. Among many implementations, great progress was made by Wu Wen-Tsün in the 1970s. Inspired by ancient Chinese mathematics, Wu proposed the algebraic method of geometric theorem machine proof, called the “Wu’s method”   . Its basic idea is to transform a geometric problem into a system of algebraic equations, and then verify (prove or disprove) the geometric theorem by calculating the relationship between the system of algebraic equations. Wu’s method has been successfully used for the mechanized proof of geometric theorems along with the rapid development of computer algebra systems like Reduce, Derive, Mathematica, Maple, and so on. Soon after Wu’s initial work, the Gröbner basis method, which was developed by Buchberger for processing polynomial system in the 1960s, has also been widely used in the field of geometric theorem proving  . Both Wu’s method and Gröbner basis method are essentially verifying algebraic identities with some constrained variables and a set of polynomial constrained equations. Starting from the fact that the lower and upper bounds of a polynomial equation can be determined by its coefficients, Hong  proposed the “one-example illustration method” that can verify the correctness of a geometric theorem via a single instance of the related geometry statement. Furthermore, based on the following observation: if a multivariate polynomial has a value equal to zero on a sufficiently large grid, then this polynomial is always equal to zero, Zhang et al. proposed the “numerical parallel method” , which passed a certain scale of examples to verify whether the given polynomial is an identity. As Hong’s method usually involves constructing a very complicated example and computation of too large objects, Hong’s method had never been used in any non-trivial theorem, meanwhile, the parallel numerical method is the first numerical algorithm with practical and feasible significance in the machine proof of geometric theorems as it was easily implemented in portable computer (like CASIO’s PB700 or Sharp PC1500) at the end of 1980s.
When the above-mentioned algebraic methods are used to prove geometric theorems, they usually include large-scale complicated calculations involving polynomials, which geometric meaning generally can’t be understood by human, and for human it is also too difficult to check the correctness of the machine computation by manual method. Therefore, such proofs are called “human non-readable”. Zhang et al.  proposed to use the area method to prove the geometric theorem and realized the readable proof for the first time. Zhou et al.  introduced the Pythagorean difference to the proof process of Non-Euclidean geometric theorems. Similar to the area method and the Pythagorean difference method, a generalized vector method was suggested in . These methods are collectively referred to as the “geometric invariant method”  .
Another category method, the “deductive reasoning method” based on database searching, which simulates the idea of human proof of geometric theorems, namely, using known hypotheses and standard axioms to perform inference searches on geometric propositions, can be traced to 1960. Gelernter et al.  proposed a method that combined the backstepping method with the depth-first search and implemented a program based on the backstepping method on the computer. Nevins  combined the forward and backstepping method to prove the geometric theorem. Zhang et al.  gave a more effective method based on a geometric deduction database system. Based on the idea of a structured database, the amount of calculation in the inference process was significantly reduced, and it proves that generate geometric propositions are generally readable. It worths indicating that together with dynamic geometry programs (like Geometer’s Sketchpad), the deductive reasoning method has been widely used for developing educational software in China. Nevertheless, there has no report on studies to promote computers to obtain graphical intuitive analysis capabilities for elemental geometry yet.
Considering that the intuitive knowledge of geometry played the essential role in the development of human intelligence—in both meaning of humankind and human individuals, it is natural to expect that computing machines that are able to see or understand certain geometry meaning, like three-point collineance, four points lie on the same circle, or square of one edge equals to the sum of squares of other two edges in certain triangles, would eventually lead to a higher stage of machine intelligence—the ASI (Artificial Super Intelligence), Sun studied recently in his Master thesis  the problem to train the intelligent agents such as computers to “observe” a large number of intuitive geometric configurations, to combine the powerful algebraic computing capabilities and data storage capabilities of machine, so to understand and master the intuitive geometrical analysis capabilities of humans in the long-term goal of AI. The work implemented a symbolic computation program with Maple software to mimic dynamic geometry for randomly generating geometric configuration in batch, and designed several statistical formulas to discover latent geometry relationships from suitable amount of graphic data, therefore, exhibited a potential probability of the conscious evolution of the computing machine species.
As an English translation of one part of the thesis, this paper focuses on establishing statistics of geometric relations in graphic data and establishing a quantitative method for comparing the similarities between the distributions of graphic data.
The rest of this paper is organized as follows. In Section 2, we introduce the geometric theorem machine proof methods related to the content of this paper. In Section 3, we propose the geometric relationship detection method based on distribution similarity. In Section 4, we conducted numerical experiments and compared the results under different observation error levels. In the final section, we draw a short conclusion.
2. Related Methods of Mechanical Geometry Theorem-Proving
2.1. Wu’s Method
Let F and G be two multivariate polynomials about the variable , the class of F is k, and the highest degree of F and G about are d and s respectively. Arrange F and G in descending order of the variable and write as follows form:
Then, there must be a non-negative integer t and polynomials T and R. The highest coefficient of R with respect to is less than d or , which satisfies:
In Equation (2), R is the pseudo remainder of polynomial G with respect to polynomial F, denoted as .
If the polynomial group satisfies , or , , then the polynomial group TS of the following form is called a triangular polynomial group:
Assuming that is a triangular polynomial group, the remainder of polynomial G with respect to TS can be obtained by the following “continuous pseudo division”:
Let , and write Equations (4) as . Further, the remainder formula Equation (2) can be extended to the following form:
Among them, and are the initial formula and polynomial of respectively.
The general procedure of Wu’s method to prove geometric theorem is as follows:
1) The geometric theorem is algebraized, the known assumptions are partially transformed into a polynomial group H, and the theorem’s conclusion is transformed into a polynomial g.
2) The polynomial group H is sorted according to the Wu-Ritt principle  , and the ascending is obtained.
3) Solve the theorem conclusion polynomial g and the continuous pseudo-division of ascending sequence, get , and judge whether the residue R is 0. If , according to Equation (5), it is easy to get the equation , and can be derived from the non-degenerate condition and . From this, we can know that the theorem to be proved holds under non-degenerate conditions.
2.2. Numerical Parallel Method
The single-example illustration method has expanded a new idea for the machine proof of geometric theorems, but it has not been realized due to its high computational complexity. Zhang et al.  proposed a numerical parallel method inspired by Wu’s method.
Suppose the polynomial , the highest degree of the polynomial F to the variable is less than or equal to , and is an arbitrary subset of elements in the domain . If the following Equation (6) holds,F is an identity that is always 0:
The conclusion can be drawn from the above: To verify whether an n-ary polynomial with the highest degree of each variable of is an identity that is always 0, only N different numerical examples need to be verified, where .
The general procedure of Wu’s method to prove geometric theorem is as follows:
1) The geometric theorem is algebraized, the known assumptions are partially transformed into a polynomial group H, and the theorem’s conclusion is transformed into a polynomial g.
2) Solve the triangle polynomial set TS reduced by the polynomial set H. Solve the conclusion of the polynomial g for the remainder of TS, . Estimate the maximum degree of the remainder R for the independent variable.
3) According to Equation (6), construct the set of instances to be tested and substitute these instances into TS one by one, solve the specific values of the constraint variables, and then substitute them into g. If , it indicates that the instance is consistent with the theorem; Otherwise, this geometric theorem is generally invalid.
3. Intuitive Geometry Based on Experimental Mathematics and Statistical Analysis
3.1. Data and Statistics
The algebraic methods such as Wu’s method, single-example illustration method, and numerical parallel method prove geometric theorems. It is necessary to algebraize the geometric theorems. We propose to calculate the numerical value of the geometric configuration instance without algebraic processing, so it needs to generate a large number of geometric configuration legends. Data can be generated by changing the free points in the geometric configuration. We use Maple to write a dynamic geometry subroutine module similar to the geometric sketchpad and super sketchpad to realize the data generation of the geometric configuration.
The algebraic method proves the geometric theorem, and a polynomial expresses the geometric relationship by selecting appropriate coordinates. Our Maple program simulates the intelligent subject to observe the geometric configuration intuitively, adding slight disturbances to the data and rounding the coordinates of the points. In this way, it is not possible to directly use the polynomial to express the geometric relationship. In analogy to the geometric predicate in the algebraic method, we have constructed relevant statistics to express the geometric relationship.
The construction of statistics satisfies the following three principles:
1) , if and only if a particular geometric relationship is strictly valid numerically, the degree of approximate validity of a particular geometric relationship is measured by the degree of deviation from 0.
2) Statistics should eliminate the influence of dimensions.
3) For N samples Equation (7) that satisfy a particular geometric relationship, satisfy Equation (8)
We briefly explain the construction of statistics corresponding to commonly used geometric relations.
Measure equilateral triangle: use Equation (9) to measure.
Measurement angle bisector: Measured by the difference between the two angles formed by dividing the angle by a straight line. Measure vertical (or parallel):
the value is measured by the difference between the angle of two vectors and
(or 0), and the outer product of the vector measures the sign. The three points are measured in common: the value is measured by the farthest distance among the three points, and the directed area of a triangle measures the sign. Measure the collinearity of three points: use the smallest angle between the three points in the vector. Measure multiple points in a circle: fit a circle closest to these N points by the least square method, and then use Equation (10) to measure.
3.2. Distribution Similarity Geometric Relationship Detection
In this section, we propose a geometric relationship detection method based on distribution similarity. Before that, let me introduce the methods of measuring the similarity of distributions and the nonparametric test methods used in this paper.
Considering the similarity of two probability distributions, P and Q, Kullback-Leibler divergence (KL divergence) in Equation (11) and Jensen-Shannon divergence (JS divergence ) in Equation (12) can be used.
When the support sets of the two distributions, P and Q, do not overlap or the overlap is small, it is difficult for KL divergence and JS divergence to quantify the similarity between the distributions. In recent years, the similarity of the Wasserstein distance Equation (13) metric distribution has been widely used in machine learning. In this paper, we use Wasserstein distance to measure the similarity of distributions. In Equation (13), satisfies and . In general, it is tough to calculate the Wasserstein distance, but when the data dimension , the p-Wasserstein distance can be expressed as Equation (14). Among them, and are the quantile functions of P and Q, respectively.
In this way, the calculation of p-Wasserstein distance is simplified. In the previous section, we constructed the statistics of geometric relations and mapped the observation data to one dimension to use 1-Wasserstein distance Equation (15) to measure similarity.
In statistics, hypothesis testing is often used in statistical inference, inferring hypotheses about the population based on empirical data. It can also be used to test whether two distributions come from the same distribution. In this paper, we used two non-parametric tests. One is the Kolmogorov-Smirnov (K-S) test, which uses the K-S statistic Equation (16) or Equation (17) to accept or reject the null hypothesis.
Another method is referred to as the permutation test based on the 2-Wasserstein distance used in Matsui et al.  and Schefzik et al. . Considering the Wasserstein distance when and , it can be decomposed into three parts  in Equation (18).
Among them, the mean, variance and shape of the three items on the right are respectively distributed. is the Pearson correlation coefficient of the corresponding point in the quantile map of F and G. Equation (18) can be approximated by the empirical estimation formula Equation (19).
and are the distribution of the observation data , and and are the quantile functions of the observation data. The null hypothesis is . Under the condition that the null hypothesis is established, the distribution functions P and Q are obtained by random replacement of samples. Calculate the distance according to Equation (18), mark as the distances between the two distributions after all possible permutations. Then the p-value can be calculated according to Equation (20), where . The subset of can approximate Equation (20) to reduce the amount of calculation, and Equation (21) can be obtained.
The geometric relationship detection method based on distribution similarity mainly includes the following steps:
Step 1: Call the Maple subroutine to generate the corresponding geometric configuration legend, and generate a large sample data according to the dynamic geometry.
Step 2: Randomly select a batch of samples, and measure the similarity according to Equation (15). Under fixed disturbance , construct the standard distribution of each geometric relationship to measure the observation data distribution . Among them, f is a statistic that measures geometric relations.
Step 3: In Step 2, reduce the search range according to the 1-Wasserstein distance, and perform a significance test on the remaining distributions with high similarity. When and approximately obey the normal distribution, use the T-test and the F-test to test the position and scale parameters of the normal distribution, respectively. Otherwise, the permutation test is used for the non-parametric test. Use the K-S method to test whether and approximately obey a normal distribution.
The complete process can be found in Algorithm 1.
3.3. Integral Coefficient Invariant Discovery
In Section 3.2, we propose a geometric relationship detection method based on distribution similarity to explore the deterministic vertical and collinear geometric relationships in geometric configurations. In this section, we explore the integer coefficient relationship between the lengths of geometric quantities. This type of relationship involves uncertain, unknown quantities and uncertain integer coefficients. Since most of the relations between geometric quantities are homogeneous relations of first and second order in plane geometry, we study the first and second integer coefficient relations between the length of line segments in geometric figures. Specifically, there is a vector , and a group of integers that is not all 0 is found to satisfy Equation (24).
At present, the widely used integer relational algorithms are mainly the LLL algorithm proposed by Lenstra et al., and the PSLQ algorithm proposed by Bailey et al. In addition, Feng et al.  researched a PSLQ algorithm with empirical data as input. Our data is observational data, and the accuracy of the data does not meet the requirements of these algorithms, so we try to solve it in the following way.
First, we converted the sample data, and the generated data is uniformly expressed as an array of points P Equation (23),
where the order of points in P is fixed. There is a line between any two points by default, and all the line segment lengths in the geometric figure D Equation (24) are obtained, where d is distance.
Extending it to quadratic and the reciprocal of the geometric quantity get Equation (25) and Equation (26).
Then, we randomly select no less than m converted samples and write them as in the form of a matrix, and write the integer coefficient vector to be solved as , , wherem is the number of elements in D or . If the length of the line segment in the geometric configuration has an integral coefficient relationship, then there is such a that satisfies . Due to the observation error of the sample data, the problem is transformed into Equation (27).
Usually, in plane geometry, the integer coefficients between geometric quantities are relatively small. Due to the existence of such prior knowledge, we add regular term constraints based on Equation (27) to obtain Equation (28).
In addition, in geometric figures, the integer coefficient relationships that exist are not unique. In Equation (28), integer coefficient relationships involving a small number of geometric quantities will conceal the relationship involving more integer coefficients involving geometric quantities. Consider decomposing Equation (28) into sub-problems Equation (29).
Since the elements in D, , and are always non-negative, if satisfies Equation (28), then at least two components of are not 0 and are integers. We let a component of add constraints to Equation (28) to get Equation (29) to search sequentially.
The solution of Equation (29) is complex. We use the Cplex solver developed by IBM to solve this problem. The algorithm steps are shown in Algorithm 2, where the err refers to the sum of the difference between the approximate integral relationship and the strict integral relationship and the regular term.
4. Numerical Experiment
In this section, we construct observation data of some geometric theorems and performed numerical experiments on this basis, including 12 geometric theorems such as Orthocenter theorem, Centroid theorem, Incenter theorem, Morley theorem, Euler Line, Five Circles theorem, Nine-point Circle theorem, Ptolemy’s theorem, corollary to Ptolemy’s theorem, Candy theorem, Pappus theorem, and Desargue theorem. We first carry out numerical experiments under disturbances and then carry out numerical experiments with different disturbance levels of and , where is normal distribution.
Take the Orthocenter theorem to illustrate a feasible method of selecting thresholds to reduce the search space. Figure 1 is the Wasserstein distance of the geometric relationship of the three-point collinear relationship in the Orthocenter theorem. The Wasserstein distance is naturally divided into two categories. The right part does not satisfy the three-point collinear relationship, so the data of these combinations can be quickly excluded. In the Orthocenter theorem, the perpendicular, three-point common point relationship test is the same, and the hypothetical test of the result after rapid elimination is performed. The Orthocenter theorem, the empirical distribution of the perpendicular relationship
Figure 1. Wasserstein distance of the three-point collinear relationship in the Orthocenter theorem.
statistics of the three vertical lines, and the standard distribution of the perpendicular relationship statistics under disturbance are shown in Figure 2. A further hypothetical test is performed on the perpendicular relationship of the three vertical lines and the significance level a = 005. Because the empirical distribution and the standard distribution are approximately normal distributions, the parameter test is used directly. The results are shown in Table 1.
Since there are many collinear and perpendicular relationships, it is too verbose to list them all. Here are examples of each type of geometric relationship. The results are shown in Table 2, where 1-Wd means 1-Wasseratein distance.
We take Ptolemy’s theorem, the corollary of Ptolemy’s theorem, and Candy theorem as examples to carry out numerical experiments on the invariants of integral coefficients. The first is Ptolemy’s theorem, 100 samples are randomly selected to solve, and three effective solution vectors Equation (30) are obtained. These three solution vectors correspond to the same geometric relationship, which is the conclusion of Ptolemy’s theorem. We re-selected 100 samples for 10 experiments, and the errors obtained were 94.3702, 78.3523, 59.2743, 31.8584, 76.5764, 81.6923, 43.1427, 69.1004, 118.8367, 76.9757.
The second is the corollary of Ptolemy’s theorem, where the result of the corollary is in an order relationship with the size of the geometric value, and the length of the line segment is sorted before starting the solution. Similarly, 100 samples are randomly selected and solved to obtain the solution vector Equation (31).
Figure 2. The distribution of the perpendicular relationship statistics of the vertical lines, the lower right corner subfigure is the standard distribution and the rest are the empirical distribution.
Table 1. Hypothesis test of perpendicular relationship ( ).
Table 2. Geometric relationship detection results based on distribution similarity ( ).
Finally, in the numerical experiment of Candy theorem, the theorem’s conclusion could not be obtained. If we expand the conclusion of Candy theorem, we get a cubic relationship. It is tough to solve the cubic relationship. The dimension of the solution vector will be increased very largely, and the error will also accumulate due to the multiplication of each item.
The comparative experimental results of the other two groups of different disturbances can be seen in Table 3 and Table 4. The error of the integral coefficient invariant relationship in Table 4 is taken from the average of the results of 10 experiments, and “−” means that the result of the theorem is not obtained.
In this paper, we construct statistics that measure approximate geometric relationships for inaccurate observation data, map the observation data to one dimension through statistics. Using the distribution similarity of the Wasserstein distance metric, we propose a method for detecting geometric relationship similarities. The method has been successfully applied for checking the following geometric relations: 1) three lines intersect at one point; 2) three points lie on one line; 3) three points form one equilateral triangle; 4) two lines are parallel or perpendicular to each other; 5) one line bisects a given angle; 6) four points form a convex quadrilateral; and 7) four or more points lie on the same circle. We have also proposed a searching method to find linear or quadratic equations with integer coefficients between observed geometric quantities under certain prior conditions. The constrained searching method can be used to find linear or quadratic relation with integer coefficients between geometric quantities under a priori conditions. Numerical experiments show that the method proposed in this
Table 3. Geometric relationship detection results ( and , ).
Table 4. Integral coefficient relation error under different disturbance levels.
paper is adequate, which will help the machine to obtain intuitive analysis capabilities for geometric figures, which have practical significance and certain application prospects. Our experiment failed in finding a cubic relation in the CandyTheorem, namely, assume that AB is an arbitrary chord in the circle O, P is a point on AB, are arbitrary two points on the circle O, are intersection points of the circle O and line , and are intersection points of the chord AB with , respectively, then . We will try to overcome this difficulty by control error accumulation in numerical analysis. An interesting problem is to train computers to find latent inequalities from configuration data. A very simple and famous example of such kind is Euler’s Inequality, which states that the distance d between the incenter r and the circumcenter R of a triangle satisfies
and therefore . Since almost interesting theorems that involved equalities in Euclidean geometry have been well established in past three thousand years, a prospective application of machine intelligence in the future would be automated discovering of geometric inequalities through analyzing big data of geometric configurations.
 Tarski, A. (1951) A Decision Method for Elementary Algebra and Geometry. In: Johannes, K., Ed., Texts & Monographs in Symbolic Computation, Springer, Berlin, 24-84.
 Chou, S.C. and Gao, X.S. (1990) Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving. International Conference on Automated Deduction, Kaiserslautern, July 1990, 207-220.
 Kutzler, B. and Stifter, S. (1986) On the Application of Buchberger’s Algorithm to Automated Geometry Theorem Proving. Journal of Symbolic Computation, 2, 389-397.
 Hong, J.W. (1986) Can We Prove Geometric Theorems with Examples? Science in China Series A-Mathematics, Physics, Astronomy & Technological Science, 16, 234-242.
 Zhang, J.Z., Chou, S.C. and Gao, X.S. (1995) Automated Production of Traditional Proofs for Theorems in Euclidean Geometry I. The Hilbert Intersection Point Theorems. Annals of Mathematics & Artificial Intelligence, 13, 109-137.
 Chou, S.C., Gao, X.S. and Zhang, J.Z. (1993) Automated Production of Traditional Proofs for Constructive Geometry Theorems. Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, 19-23 June 1993, 48-56.
 Chou, S.C., Gao, X.S. and Zhang, J.Z. (1993) Mechanical Geometry Theorem Proving by Vector Calculation. Proceedings of the 1993 International Symposium on Symbolic and Algebraic Computation, Kiev, Ukraine, August 1993, 284-291.
 Gelernter, H., Hansen, J., Loveland, D. (1960) Empirical Explorations of the Geometry-Theorem Proving Machine. Western Joint IRE-AIEE-ACM Computer Conference, San Francisco, California, 3-5 May 1960, 143-149.
 Chou, S.C., Gao, X.S. and Zhang, J.Z. (2000) A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering. Journal of Automated Reasoning, 25, 219-246.
 Matsui, Y., Mizuta, M., Ito, S., Miyano, S. and Shimamura, T. (2016) D3M: Detection of Differential Distributions of Methylation Levels. Bioinformatics, 32, 2248-2255.
 Schefzik, R., Flesch, H. and Goncalves, A. (2021) Fast Identification of Differential Distributions in Single-Cell RNA-Sequencing Data with waddR. Bioinformatics.
 Irpino, A. and Verde, R. (2015) Basic Statistics for Distributional Symbolic Variables: A New Metric-Based Approach. Advances in Data Analysis and Classification, 9, 143-175.