33
$\begingroup$

I think I can improve the current upper bound concerning an open problem. The ideas are purely combinatorial, but in the end I have to calculate the maximum of a really ugly, non elementary function with four variables. I did this with a computer, and the output was good so that's why I think I can improve the bound. (In the most precise sense, as this is not a real proof, but clearly not nothing.)

My first question is: What kind of computer calculations can be included in a paper?

To be a little bit more specific, my function includes the inverse of the binary entropy function (actually both inverses). This is not an elementary function and it is not implemented in Wolfram Mathematica (the program I am working in). So I had to calculate its values numerically. My function sometimes involves two of such functions nested in each other, but only at most 3 times. During the process I had to obtain upper bounds on complicated functions with two variables, I did this by plotting them and plotting the plane of the corresponding constant, and observing that the graph of the function is under the plane.

To elaborate a bit further, I saw in other papers, that if you prove that the required constant is a solution of a certain equation, it is okay to stop there and say that "and this constant is approximately 2,32", as this can be calculated easily with arbitrarily small error. But I feel like my proof is not complete, as I do not know the error of the approximation of my function, and somehow I am also not satisfied by the "plotting and observing" type bounds. I believe them to be true, but this method lacks rigour. On the other hand, I feel that my real contributions to the subject are the combinatorial ideas. It is of course important to prove that they really improve the current bounds. But I feel that this should be easy. But non elementary functions are making it not that easy. My second question is: What would be the best solution, if my goal is to write a good paper?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ I think your question is ambiguous. When you write "what kind of computer calculations can be included in a paper?", you may mean two different things: either you ask which computer assisted proofs can be considered as proofs, and make it into a published article; or you may ask what to write down explicitly in a paper reporting on such a proof. You may also want to ask both, but in any case you should make that clear. $\endgroup$
    – Benoît Kloeckner
    Commented Jul 26, 2015 at 7:57
  • 2
    $\begingroup$ In addition to putting stuff in the paper, a practical alternative is to make mathematica (or other relevant software) notebooks available online, in addition to any amount of additional written supplementary material. This material serves the purpose of making the work "more verifiable" --- and saves on valuable space in the paper, which I think should be used to include the "highlights" of even the computational part. $\endgroup$
    – Suvrit
    Commented Jul 26, 2015 at 13:39
  • $\begingroup$ @BenoîtKloeckner I am more interested in your second variant. Now I got so many valuable responses, I'll have a hard time choosing the one to accept. $\endgroup$
    – Daniel Soltész
    Commented Jul 26, 2015 at 14:41

4 Answers 4

Reset to default
20
$\begingroup$

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)

they show how to prove inequalities such as

          Inequality
          (from p.11 of the arXiv version.)
Their abstract begins:

We present a formal tool for verification of multivariate nonlinear inequalities. Our verification method is based on interval arithmetic with Taylor approximations. Our tool is implemented in the HOL Light proof assistant and it is capable to verify multivariate nonlinear polynomial and non-polynomial inequalities on rectangular domains.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Thank you, strictly speaking this might only be an answer to my second question, but it might help me a lot. I will read the paper! $\endgroup$
    – Daniel Soltész
    Commented Jul 25, 2015 at 18:42
  • 4
    $\begingroup$ Hales has set a(n appropriately) high bar for us all. $\endgroup$
    – Joseph O'Rourke
    Commented Jul 25, 2015 at 19:14
  • 2
    $\begingroup$ So, Daniel, when you wrote, "My question is: What kind of computer calculations can be included in a paper?" what you meant was "My first question is: What kind of computer calculations can be included in a paper?" --- is that right? $\endgroup$
    – Gerry Myerson
    Commented Jul 25, 2015 at 23:36
  • $\begingroup$ @GerryMyerson In short: yes. (I edited the question accordingly, thank you.) Actually I think that the MO community would benefit more from a general what to do what not to do type of answer. But I personally benefit more from answers to the second one. $\endgroup$
    – Daniel Soltész
    Commented Jul 26, 2015 at 1:39
12
$\begingroup$

Look at interval arithmetic. Warwick Tucker used this to prove Smale's fourteenth problem, which is a pretty good precedent for its use in a proof.

Improve this answer
$\endgroup$
10
$\begingroup$

This is a problem that I have faced also. One approach is to try to prove rational polynomial bounds on the relevant functions (by Taylor series with remainder, for example) that are accurate enough to satisfy the same inequalities. Then you can prove the inequalities rigorously by various methods; the paper of Solovyev and Hales that Joseph links to describes free software better than I knew of before. If the functions vary too much you might need to subdivide the domain and apply the method separately to each part.

You will then face the problem of what to put in the paper, as nobody wants to see page-long intermediate expressions. But at least you can describe how you went about constructing a rigorous proof.

Improve this answer
$\endgroup$
8
$\begingroup$

I suggest glancing at two papers:

Hagedorn, Thomas. "Computation of Jacobsthal’s function $h(n)$ for $n< 50$." Mathematics of Computation 78.266 (2009): 1073-1087.

Hajdu, L., and N. Saradha. "Disproof of a conjecture of Jacobsthal." Mathematics of Computation 81.280 (2012): 2461-2471.

Both of them describe somewhat massive projects which involve a lot of computation. They give algorithmic descriptions as well as some sample computations. Although I personally want more, they provide enough detail that I do not question the validity of their work. You might use them as examples for how to write up your results.

Gerhard "The Computer Says So, QED" Paseman, 2015.07.25

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ Lest my statement be interpreted too strongly, let me say that I have not personally verified the contents. They may contain errors. However, the thoroughness and clarity of the exposition lead me to the confidence that I can replicate and verify the results, as can anyone else. When I am ready, I will check their work because they wrote down enough for me to do so. Gerhard "Then I'll Build The Bridge" Paseman, 2015.07.26 $\endgroup$
    – Gerhard Paseman
    Commented Jul 27, 2015 at 1:39

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .