ODEs in Coq/Isabelle/...

Stream: general

[Winston Yin (尹維晨)]

Does anybody who is more knowledge about other proof assistants know what the status of ODE libraries (esp. existence/uniqueness) is in other formalisation projects? Say, there could be a standalone library or something hidden in a larger formalisation project. @Yury G. Kudryashov and I would like to see how the current theory in mathlib compares with other efforts.

[Patrick Massot]

https://saloranta.de/immler/fabian/documents/immler_tan_2020_poincare_bendixson.pdf probably contains useful data.

[Patrick Massot]

More generally, more papers by Fabian Immler should be relevant.

[Yury G. Kudryashov]

We're trying to figure out whether we have something new that wasn't formalized elsewhere.

[Patrick Massot]

Yes I understood that.