Dynamical systems theory results like Takens' theorem

Stream: Is there code for X?

[André Muricy Santos]

I understand that continuous things don't play well with theorem provers, but I've seen that there's a lot of topology and analysis code. I'd really like dynamical systems research to play a bigger role in theorem proving (or vice versa)

[Yaël Dillies]

@Yury G. Kudryashov's original motivation for getting into Lean was to formalise dynamical system theorems. I'm sure he would love to talk to you about it, although I don't think he could afford to provide much more than talking given his current job.

[Patrick Massot]

André Muricy Santos said:

I understand that continuous things don't play well with theorem provers

Where did you get this idea? Did you see the sphere eversion project?

[André Muricy Santos]

Patrick Massot said:

André Muricy Santos said:

I understand that continuous things don't play well with theorem provers

Where did you get this idea? Did you see the sphere eversion project?

No, I haven't but i'll check it out. I got this idea from implementing such systems in Agda for my thesis, i just ended up discretizing everything. it seems Lean has an advantage over Agda in this regard, not only wrt theorems but also running simulations via SciLean.

[Yaël Dillies]

The ease of formalising certain topics in a given theorem prover is greatly a function of who uses that theorem prover. For example, Isabelle is (currently) much better for classical analysis than Lean simply because they have Manuel Eberl.

[André Muricy Santos]

Very interesting, I'd never thought of that...

[Patrick Massot]

Yaël’s message is a bit simplified. Manuel Eberl is of course amazing but one should not forget the role of John Harrison’s work, ported by Larry Paulson. Also Isabelle’s automation works very well in this context.

[André Muricy Santos]

I thought Isabelle wasnt a "big player" in the theorem proving space, but I guess I was wrong. I'll take a closer look at it :)

[Henrik Böving]

I'd say the three big players in interactive theorem proving are Isabelle, Coq and Lean. There are of course other systems like the various variants of Agda or to mention a non dependently typed one HOL Light but I don't think they enjoy the same amount of popularity.

[Mario Carneiro]

No, that statement is not wrong. I'm pretty sure Isabelle + AFP is larger than mathlib in terms of theorems proved, although it has a slightly different demographic / focus

[Yury G. Kudryashov]

What kind of dynamical systems results do you want to formalize? I have some plans but my day job takes too much time and energy.

[Yury G. Kudryashov]

Note that we don't have the right version of Whitney's embedding theorem, because we don't have Sard's theorem yet.

[Jeremy Avigad]

Fabian Immler's work on the Lorenz attractor is impressive:
https://link.springer.com/article/10.1007/s10817-017-9448-y

See also the work with Yong Kiam Tan on Poincaré-Bendixson:
https://saloranta.de/immler/fabian/documents/immler_tan_2020_poincare_bendixson.pdf