[FOM] Foundational Challenge

[Timothy Y. Chow]

Martin Dowd wrote:

> A problem I just ran in to in some complexity theory research seems 
> relevant here. Program verification is a venerable branch of computer 
> science, and has bee used in the sphere packing project I believe. But 
> some very simple problems have seemingly "inherently long" proofs. For 
> example, the fact that a particular Turing machine computes x+y may be 
> formulated as an equation of polynomial time arithmetic. A proof in 
> polynomial time arithmetic would be long. I don't think any work has 
> been done in this area. Using known program verification methods, a 
> short proof could probably be given for something like a loop program.
> Ab initio, it doesn't seem that any amount of "improvement" to the 
> formal system would be likely to reduce the length of a proof for the 
> Turing machine.
> - Martin Dowd

I made some related remarks back in 2007, and touched on the subject again 
in 2014.

https://cs.nyu.edu/pipermail/fom/2007-June/011667.html
https://cs.nyu.edu/pipermail/fom/2007-July/011740.html

https://cs.nyu.edu/pipermail/fom/2014-August/018057.html

In other words, we already have examples of theorems that have a PSPACE 
flavor to them, indicating that they're unlikely to have short 
certificates (I'm afraid I'm currently a skeptic of Gordeev and Haeusler's 
claims to have proven NP = PSPACE).  "Checkers is a draw" isn't 
particularly interesting mathematically, but I suspect that more 
interesting mathematical examples are on the horizon.

Possibly the S-unit equation is in this family.  The S-unit equation is a 
famous equation in number theory, and recently, explicit solutions of the 
S-unit equation have figured in some mainstream number-theoretic work. 
These computations are non-trivial, and are typically executed in Sage. 
I don't understand the math very well, and asking for a 
PSPACE-completeness result may be too much to hope for, but S-unit 
equations seem to not possess short certificates.  If that is true, then 
any proof assistant will necessarily take a long time to verify the proof.

Here's one paper that gives more details.

https://arxiv.org/pdf/1903.00977.pdf

Tim