[FOM] Formal verification

[Rempe-Gillen, Lasse]

Dear all,

On FOM on October 24, I proposed the challenge of formal verification of Misiurewicz's 1981 proof of a conjecture of Fatou from 1926. 

Freek Wiedijk kindly passed my suggestion on to John Harrison, who worked his magic and very quickly completed a full verification of the theorem in HOL Light.

http://code.google.com/p/hol-light/source/browse/trunk/Examples/misiurewicz.ml

The key statement proved is quite easy to parse:
"!u a. open u /\ ~(u = {}) /\ ~(a = Cx(&0))
         ==> ?n. a IN IMAGE (ITER n cexp) u."
That is: "If U is a nonempty open set and a is a non-zero complex number, then U contains a preimage of a under some iterate of f."

Many thanks to John for his amazing work, which demonstrates that the verification of theorems of modern complex analysis with relatively "elementary" proofs is certainly feasible at this point. 

The original summary of my challenge is included below as a reminder.

Best wishes,
Lasse

> 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.