Stretch goal

Stream: maths

[David Michael Roberts]

I just had a look at Tucker's paper "The Lorenz attractor exists" https://doi.org/10.1016/S0764-4442(99)80439-X a 6-page (or really 5-page) summary of his proof that the Lorenz attractor exists and exhibits chaotic behaviour. The proof seems to rely on a bunch of C programs to do a whole lot of estimates. Some bright young things interested in getting analytical stuff up and going in Lean could probably do worse than build toward formal verification of some of these.

[Rob Lewis]

https://dl.acm.org/citation.cfm?id=3230191

[David Michael Roberts]

To save others a click, title is "A Verified ODE Solver and the Lorenz Attractor"; it's a formalised version of Tucker's work using Isabelle/HOL. But, it would be an interesting branch out from algebraic number theory to attack ODEs.

[Fabian Immler]

Tucker's journal article "A rigorous ODE solver and Smale's 14th problem" https://doi.org/10.1007/s002080010018
presents the proof in more detail than the 5-page summary.

Note that the verification that I did in Isabelle/HOL was restricted to the numerical part of Tucker's proof (i.e., section 3 in the 5-page summary, sections 4 and 5 in the journal).

Verification of the analytical part (section 2 in the summary, section 3 in the journal) would be completely novel, so there is lots of things to do ;-)