Topic: Stretch goal
David Michael Roberts (Oct 16 2019 at 07:13):
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 (Oct 16 2019 at 07:23):
David Michael Roberts (Oct 16 2019 at 09:23):
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 (Oct 18 2019 at 20:27):
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 ;-)
Last updated: May 10 2021 at 07:15 UTC