I know it is partly subjective, but what is the most advanced/impressive result in analysis available in Isabelle/HOL?

I have virtually no experience with analysis, but one theorem very interesting to me that happens to have been formalized in Isabelle is Dirichlet's arithmetic progression theorem: https://www.isa-afp.org/entries/Dirichlet_L.html

Not sure I would call this an analysis result though…

I mean it uses techniques from complex analysis I guess…

There's all kinds of things like invariance of domain/invariance of dimension, the Riemann theorem, a very general form of multivariate change of variables for integration

Green's theorem (albeit still with some technical assumptions where it is not entirely clear if and how they can be lifted)

Ah, and there's Apéry's Theorem. Not sure if that's impressive; it's certainly well-known, but at the end of the day the proof just boils down to a few integrals and applying the Prime Number Theorem.

Last updated: Aug 15 2022 at 02:13 UTC