cauchy-kovalevskaya theorem

Stream: Is there code for X?

[Kevin Buzzard]

I'm at a conference, and Daniel Peralta Salas (who does PDEs) asked me if we have this theorem. This is a classical and very general result, whose proof is only a few pages long. Are we anywhere near a proof of this?

[Michael Rothgang]

I remember @Yury G. Kudryashov giving a talk with a list of 21 major theorems, asking the audience which ones were not formalised yet. (The answer: only 5, one of which was Fermat.) Cauchy-Kovalevskaya is among the list of not formalised yet.

[Damiano Testa]

Was this the link you were thinking of?

[Yury G. Kudryashov]

It shouldn't be too hard to formalize it but it never made it to the top of my priority list.