[FOM] A computationally very hard, mathematically very interesting problem

[Arnold Neumaier]

On 08/13/2014 01:48 AM, Timothy Y. Chow wrote:
in the thread ''Formally verifying "checkers is a draw"'':
>
> Bas Spitters remarked, "It is not clear to me that there are many
> naturally occurring co-NP-hard results."  I think that there are a lot
> of them lying around but we just haven't drawn attention to them.  It is
> common, for example, to see an assertion along the following lines in a
> mathematical paper: "We conjecture that P(n) is true for all n.  We have
> verified that P(n) is true for n <= 26."  If P(n) is co-NP-hard then
> this throwaway comment in the paper may represent large amount of
> computation. Many combinatorial non-existence results have a co-NP-hard
> flavor even if they are not officially co-NP-hard.

 > Many finite computations might be uninteresting, but it is not hard
 > to imagine that there might be many interesting theorems whose proofs
 > reduce to a finite computation.  A full proof of the interesting
 > theorem might need to include the full verification of P(n) for all
 > n <= 26.

A 165 years old, computationally very hard, and mathematically very
interesting problem from the geometry of numbers is the determination
of the exact values for Hermite's constant gamma_n; for a definition
see
     http://en.wikipedia.org/wiki/Hermite_constant
Finding it is equivalent to proving that some particular n-dimensional
lattice is the densest possible, which can be proved to be a finite
task for each value of n. Only the values for n<=8 and n=24 are known;
the likely exact values for n<=26 come from the densest known lattices; see
    J. Conway and N.J.A. Sloane,
    Sphere packings, lattices and groups, 3rd ed.,
    Springer, Berlin 1998.
(His list from the first edition has not improved since then in
dimensions n<=26.)

The proofs for n<=4 are fairly easy. A conceptual proof for n<=8 was
given by Blichfeldt 1935, based on a huge number of cases - done by
hand but with arguments indicated so briefly that the proof is very
difficult to verify by hand; see the story in Section 8 in
    S.S. Ryshkov and E.P. Baranovskii,
    Classical methods in the theory of lattice packings,
    Russian Math. Surveys 34 (1979), 1--68.
    http://iopscience.iop.org/0036-0279/34/4/R01/
The ''next'' case n=24 was handled only recently in
    H. Cohn and A. Kumar,
    Optimality and uniqueness of the Leech lattice among lattices,
    Ann. Math. 170 (2009), 1003--1050.
It could be handled only due to an arithmetic coincidence that is 
special to dimensions n=1,2,8,24.

A proof for n=9 is expected to be extremely involved, let alone a proof 
for all n<=26.

If an automatic theorem prover could settle the next case before a human 
can, it would make the case for the maturity of automatic theorem 
provers for problems in ordinary mathematics.

Arnold Neumaier