I wanted to ask somewhat open-ended on what tools and packages exist in julia (and outside of julia) for computer assisted “numerical” proofs, and whether you know of examples where this has been done in the julia ecosystem.
Most numerical analysis concerns itself with approximations.
However, most pure mathematicians are in the business of proving theorems. We have beautiful fancy techniques to turn estimates into theorems, but these require a proof-grade estimates, not numerical error guesstimates.
In other words, the desired output of the numerical algorithm is not so much an approximation (akin to a search problem), but rather a verifiable certificate.
A very promising example is Lyapunov Function Search · SumOfSquares
In that example, one constructs a Lyapunov function of the form ax^2+by^2+c*z^2 with a,b,c > 1 for a specific rational 3d vectorfield.
Now @blegat – does the output of jump constitute mathematical proof, in your view, that the specific output coefficients give a Lyapunov function?
The specific coefficients look suspicously floating-point like, so is something like interval math used? Is it possible to also output a certificate, i.e. something like a 500 MB “execution trace” that can be fed into a simpler program, e.g. metamath or lean or coq for verification?
It is still common to have lengthy by-hand computations and estimates in papers; and people quickly get suspicious if one writes “and the right-hand side is nonnegative because solver XYZ said so”.
A much smaller frog to swallow is “solver XYZ constructed a certificate of nonnegativity; the sha1 of the certificate is xxxx, and it is available at yyyy, and can be verified with the simple and stable standard tool zzz”.
Another promising direction is https://juliaintervals.github.io/
So, e.g. @dpsanders – would you, personally, say that a claim by IntervalArithmetic.jl has the same “real mathematical proofiness” as e.g. a lean-verified proof or the old four color theorem?
To give a very simple but real-life example (dynamical systems / general relativity).
I have 5 real variables, x y a b c. These have a,b,c > 0, and 1 = x^2+y^2 + a^2 + b^2 + c^2 - 2ab + +2bc + 2ca. Use the shorthand r^2 = x^2 + (b-c)^2 and d^2=4bc.
Show that, for y < 0, and a, |b+c|, |b-c| < 1/2, and r >0 and d/r < 1 the following holds:
| sqrt(3) * x * (b+c) / r^2 + (a - 2(b-c))*(1 - (b-c)^2 / ((1-y)*r^2))| < 5.
This kind of computation is a royal pain! There is no proof to possibly write down, it is obvious after staring at it and doing elementary estimates. All the interesting work is done in identifying the quantity that must be controlled, and the regime where it can be controlled, and using that to prove theorems.
And yet, it would be nice to also plug that kind of thing into a notebook that verifies that yes, this is correct.
Towards less simplistic things! A pretty cool construction used interval arithmetic plus conley index to verify chaoticity in the lorenz equation (ODE): [math/9501230] Chaos in the Lorenz equations: a computer-assisted proof and its companion https://www.ams.org/mcom/1998-67-223/S0025-5718-98-00945-4/S0025-5718-98-00945-4.pdf
This should be a machine for cranking out theorems. But we don’t have the necessary support in DifferentialEquations.jl, do we @ChrisRackauckas ?
And even less simplistic. For example Computer-assisted proofs for semilinear elliptic boundary value problems | Japan Journal of Industrial and Applied Mathematics uses computer assisted proofs to construct solutions to e.g. - \Delta u = \lambda e^u with dirichlet boundary. This nonlinearity should make all of us shudder – obviously naive purely analytical techniques for existence of solutions will fail flat. And yet – obviously actual solutions will only have finite morse-index, so will be amenable to all our standard tools for approximation, especially discretization in a finite-dimensional function space. So it is feasible to take an approximate numerical solution, and then use some variant of Newton / Kantorovich / etc, plus a bunch of functional analysis, to prove a posteriori that a true continuous solution exists that is near the approximate numerical solution. Not just feasible, done!
Do we have the machinery in julia to replicate such things?
Ultimately, I’m coming at this more from the “want to prove theorem” side, not from the “what kind of theorem is feasible for computer-assistance”.I don’t really want to invent new computer-assisted proof techniques; I want to use the computer assistance to apply my favorite Conley index construction to specific things. I don’t really want to look into details of interval arithmetic implementations. I am pretty clueless about algebraic geometry, but it would be awesome if I could have a nice oracle “feed in description of semi-algebraic set, get certificate of emptiness | certificate of non-emptiness with a solution attached | nope, too difficult”. Many many elementary estimates can be formulated as “is this semi-algebraic set empty?”.