Ancestors

Written by Dima Pasechnik 🇺🇦 🇳🇱 on 2024-09-05 at 18:59

In passing I mentioned in a paper

that #ProofAssistant with good certified computer algebra capabilities is not available, nor will be any time soon. And, well, I'm told by a referee either to remove this claim, or provide a reference.

Does anyone know what to cite here?

=> More informations about this toot | More toots from dimpase@mathstodon.xyz

Written by Andrej Bauer on 2024-09-05 at 20:33

@dimpase You could try to search the literature to find work on combining proof assistants and computer algebra systems. You can then summarize what is out there, for instance "previous efforts to combine proof assistants and computer algebra systems [13, 69, 666, 42] have demonstrated that one either has to trust the CAS and thereby significantly lower correctness guarantees, or severely hamper the power of CAS by insisting that it produce verifiable certificates (which CASs are not designed to do)."

Some literature that comes to mind:

Analytica

https://library.wolfram.com/infocenter/Articles/3152/

https://doi.org/10.1023/A:1006079212546

Mathematica + Lean

https://arxiv.org/abs/2101.07758

In https://doi.org/10.4230/DagRep.13.10.1 the following two reports are relevant:

Proving an Execution of an Algorithm Correct?

James H. Davenport (University of Bath, GB)

Using verified code inside CASes

Alex Best (King’s College – London, GB) and Tobias Nipkow (TU München – Garching, DE)

That's about what I can produce off the top of my head at 10pm.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Written by soaproot on 2024-09-06 at 06:56

@andrejbauer @dimpase Oh wow, very cool to see what people have been doing in this area. I'm idealistic enough to dream that some version of the "produce verifiable certificates" approach will be implemented some day, but even to me it sounds like a lot of work if we are lucky, and hitting problems we don't know how to solve if we are unlucky.

=> More informations about this toot | More toots from soaproot@sfba.social

Written by Andrej Bauer on 2024-09-06 at 07:05

@soaproot @dimpase With certificates you immediately hit NP and then you have a million dollar problem in your hands.

=> More informations about this toot | More toots from andrejbauer@mathstodon.xyz

Written by Jacques Carette on 2024-09-06 at 12:46

@andrejbauer @soaproot @dimpase Outside of the super-basic computer algebra algorithms that mostly have complexity the same as matrix multiplication, the rest of the useful ones tend to be double-exponential (worst-case), or worse.

CASes are also quite full of pseudo-algorithms because the problems they solve are in general in uncomputable / undecidable domains.

NP is child's play for CASes.

=> More informations about this toot | More toots from JacquesC2@types.pl

Written by Philip Zucker on 2024-09-06 at 14:47

@JacquesC2 @andrejbauer @soaproot @dimpase

I'm a bit confused. When the CAS pseudo-algorithms do work, there is some informal reasoning that the output is correct that in principle could be formalized in the next 100 years. Some of what they do is equational search / term rewriting for which reasonable certificates would be the chain of steps. I don't see how being in NP or worse impacts the feasibility of producing certificates for particular solutions. SAT solvers certainly can produce certificates when they succeed.

=> More informations about this toot | More toots from sandmouth@types.pl

Written by Philip Zucker on 2024-09-06 at 14:56

@JacquesC2 @andrejbauer @soaproot @dimpase

To some degree all a certificate has to be is some form of logging that isn't totally incomprehensible to an outsider. The traces of any solver that is working are proof objects of sorts. That's what unsat certificates are basically.

=> More informations about this toot | More toots from sandmouth@types.pl

Toot

Written by Jacques Carette on 2024-09-06 at 17:08

@sandmouth @andrejbauer @soaproot @dimpase As was (re)discovered over the summer at the HIM seminars is that certificates (i.e. positive information) for negative statements are very difficult. In particular things like "polynomial p is irreducible over field F" is fiendishly difficult. Certificates for the correctness of positive computations are quite easy, comparatively speaking.

=> More informations about this toot | More toots from JacquesC2@types.pl

Descendants

Written by Dima Pasechnik 🇺🇦 🇳🇱 on 2024-09-06 at 17:29

@JacquesC2 @sandmouth @andrejbauer @soaproot sure, certificates for things like irreducibility (be it numbers, or algebraic variety), non-negativity (of multivariate polynomials, etc), emptiness (Nullstellensatz, Positivstellensatz, etc) are in general difficult - for good theoretical reasons: there are bad lower bounds.

=> More informations about this toot | More toots from dimpase@mathstodon.xyz

Written by Philip Zucker on 2024-09-06 at 20:10

@JacquesC2 @andrejbauer @soaproot @dimpase so would a CAS return an opinion about this question? Is the problem that it applies a pile of non systematic sufficient criteria?

=> More informations about this toot | More toots from sandmouth@types.pl

Written by Jacques Carette on 2024-09-06 at 20:21

@sandmouth @andrejbauer @soaproot @dimpase It depends - sometimes it's an actual algorithm, but it has never been engineered to leave any kind of reasonable trace and lots of the real information is all meta, i.e. in the correctness proof of the algorithm which typically only exists in paper-math form.

And yes, a lot of these things are often structured as several sufficient criteria first (because they are fast) and then some complex algorithm last (because it's slow as molasses, but works if you're patient enough.)

Sometimes, it's trickier still: The Risch algorithm is correct for its specification (solving a problem in differential algebra) but it is known to be wildly incorrect for its usage in practice, i.e. finding anti-derivatives. Lo and behold, analysis and algebra are different disciplines!

=> More informations about this toot | More toots from JacquesC2@types.pl

Written by Dima Pasechnik 🇺🇦 🇳🇱 on 2024-09-06 at 22:32

@JacquesC2 @sandmouth @andrejbauer @soaproot

Risch algorithm (in a restricted case) needs Schanuel conjecture to hold to be correct; and moreover, in general it needs ability to test for zeros, something that is in general impossible, as shown by Richardson:

https://en.wikipedia.org/wiki/Richardson%27s_theorem

=> More informations about this toot | More toots from dimpase@mathstodon.xyz

Written by Refurio Anachro on 2024-09-07 at 12:14

Sometimes SAT solvers can certify that there is no match. You are right, there must be situations which cannot be certified easily, but I think it may be slightly more subtle than what you said.

@JacquesC2 @sandmouth @andrejbauer @soaproot @dimpase

=> More informations about this toot | More toots from RefurioAnachro@mathstodon.xyz