# Maple Program for MC 2021 Paper: a Machine Proof of an Inequality for the Sum of Distances between Four Points on the Unit Hemisphere using Maple Software

### EasyChair Preprint 6349

26 pages•Date: August 23, 2021### Abstract

In this document, we present the Maple program for our

Maple Conference 2021 paper, where we proved a geometrical inequality

which states that for any four points on the unit hemisphere, the largest

sum of distances between the points is $4+4\sqrt{2}$ using Maple computation.

In our proof, we have constructed a rectangular neighborhood of the local

maximum point in the feasible set, which size is explicitly determined,

and proved that (1): the objective function is bounded by a quadratic

polynomial which takes the local maximum point as the unique critical

point in the neighbor- hood, and (2): the rest part of the feasible set can

be partitioned into a finite union of a large number of very small cubes

so that on each small cube the conjecture can be verified by estimating

the objective function with exact numerical computation. The attched

Maple program is for the second part. The work on first part, i.e., the

construction of the critical neighborhood, has been published recently in

the ADG 2021 (the Thirteenth International Conference on Automated

Deduction in Geometry), where we have proved that the sum of distances

between points contained in the constructed neighborhoods is not larger

than $4+4\sqrt{2}$, also using Maple computatin.

**Keyphrases**: Branch and Bound, Maple program, computational geometry, global search algorithm, inequality