[FOM] Formal verification

[Rempe-Gillen, Lasse]

Many thanks to all of you for the many thoughtful and thought-provoking responses to my questions.

Of course Bill Tait is absolutely right that my suggestion of asking "every beginning postgraduate student" to contribute a formally verified proof may have been overstating things - in fact, I would never seriously suggest a one-size-fits-all approach to mathematical education. But that wasn't really the point I was trying to make. :)

Huge thanks goes to Freek Wiedijk and Joachim Breitner for their willingness to invest time and effort into producing their amazing formalizations of my toy problem. I think this was really useful for me to understand the current state as it comes to formal verification - which is encouraging. 

My conclusion is that, while these systems are still a long way from being convenient for routine mathematical practice, they are much further along than many research mathematicians are likely to believe. Furthermore, despite the scope for further improvement, it seems to me that there is perhaps no need for revolutionary new ideas.

It appears that greater interaction between research mathematicians in a variety of areas and the Interactive Theorem Proving community would be helpful at this stage. Indeed, these might both stimulate developments in formal verification that would make life easier for real mathematical practice, and also raise the awareness of the current state-of-the-art further.

Let me therefore propose a slightly more serious problem for formal verification: Misiurewicz's 1981 proof of Fatou's 1926 conjecture that, for the complex exponential map f(z)=e^z, the Julia set is the entire complex plane. (Informally, the Julia set is the set of points where the function behaves 'chaotically'; see below for a version of the statement that is completely elementary.) 

This result is well-known in the holomorphic dynamics community, so its formalization would at least be noticed. At the same time, it has an elementary proof. Based on the experience of the current thread, if I was to get together with an expert user of a formal verification system, this should take days or weeks, rather than months. However, probably these experts have better things to do than to keep formalizing proofs that I suggest. :)

My proposal is for anyone who might be interested in contributing to this problem to email me off-list. (Some further detail is below for those who are interested.) If there are no takers, perhaps I or a motivated colleague will take this on at some point down the line, in which case the code from this week's toy example will undoubtedly be invaluable.

Best wishes, and thank you again,
Lasse

---
Further background on Misiurewicz's theorem.

Misiurewicz's original article is here:
[1] "On iterates of e^z", Ergodic Theorey and Dynamical Systems 1 (1981), 103-106.
http://dx.doi.org.ezproxy.liv.ac.uk/10.1017/S014338570000119X

I would be interested in a formal verification of the theorem in one of the following two forms. 

THEOREM 1. ([1, Lemma 6].) Let f denote the complex exponential map, and let U be a nonempty open subset of the complex plane. Then there exist x in U and a number n\geq 0 such that f^n(x) is real.

(Note: f^n denotes the n-th iterate of f.)

THEOREM 2. (Implicit in the proof of the main theorem of [1].) Let f denote the complex exponential map, and let U be a nonempty open subset of the complex plane. Then there exist x in U and a number n\geq 0 such that f^n(x) is real and negative.

(Theorem 1 implies the usual statement of Misiurewicz's theorem using techniques already known to Fatou. Theorem 2 *immediately* implies the usual statement of Misiurewicz's theorem, and follows from Theorem 1 using additional elementary methods.)

While it may seem as though the proof uses Montel's Theorem on normal families - whose formalization would likely require significant effort - I believe that all that is really required is Schwarz's lemma, which I understand is already formalized in HOL Light along with other results of elementary complex analysis. 

For further background, and a more conceptual yet elementary proof of Misiurewicz's Theorem, see my recent manuscript with Zhaiming Shen, "The exponential map is chaotic"; http://arxiv.org/abs/1408.1129. (On the face of it, the proof uses the hyperbolic metric, but if you look closely, again all that is required is the Schwarz lemma. However, I believe that for formal verification Misiurewicz's original proof, which mostly relies on direct computations, will be more amenable.)

PS. Another result that seems promising for formal verification is Sharkovskii's theorem (http://en.wikipedia.org/wiki/Sharkovskii's_theorem), either in its special case "period three implies chaos" - which should be fairly straightforward - or in its more general form, where it involves a small nightmare of bookkeeping but still doesn't use anything beyond the intermediate value theorem.