Ancestors

Toot

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

Descendants

Written by Conor Mc Bride on 2024-09-05 at 19:07

@dimpase I'd look in the direction of the "Frex" (free extension) literature from @ohad and friends.

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

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 Dima Pasechnik 🇺🇦 🇳🇱 on 2024-09-05 at 20:44

@andrejbauer great, may I steal "previous efforts ..." ?

=> More informations about this toot | More toots from dimpase@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 Dima Pasechnik 🇺🇦 🇳🇱 on 2024-09-06 at 12:52

@JacquesC2 @andrejbauer @soaproot in our experience, limited to Lean 3, verifying an identity holding between few explicit, circa, 100x100 matrices with small coefficients in (\mathbb{Z}) required esoteric hacks, and took hours of CPU time.

That is, experience with proof assistants. With CASes, my experience, starting over 30 years ago with Cayley (now called Magma) and Maple IV, is more positive.

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

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

@dimpase @andrejbauer @soaproot Lean's mathlib is an especially hostile place to do computation (not Lean, either 3 or 4, as a PL, it's fine - it is the library which is a serious impediment).

mathlib is optimized for proofs in a particular logic (i.e. classical). CASes are optimized for computation and some (like Maple) try to be as user-friendly as possible. It turns out that those are two quite radically different parts of the design space for math software!

=> 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

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

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

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

@andrejbauer @dimpase You can go WAY further back. Here's something from 1993:

J Harrison and L Th´ery. Reasoning about the reals: the marriage of HOL and maple. In A Voronkov, editor, Logic programming and automated reasoning: proceedings of the 4th international conference, LPAR ’93, volume 698 of Lecture Notes in Computer Science, pages 351–359. Springer-Verlag, 1993

and then trace forward from that.

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

Written by Apostolis on 2024-09-06 at 12:59

@andrejbauer @dimpase Having a formal structured way of introducing different systems of computation, either physical systems with sensors, or other digital systems like a computer algebra system, is the way to go in my opinion. My inspiration is @MartinEscardo 's way of structuring typetopology.

It is how mathematicians do things, by making assumptions and looking at what happens.

=> More informations about this toot | More toots from apostolis@social.coop

Written by Martin Escardo on 2024-09-06 at 20:34

@apostolis @andrejbauer @dimpase

I may say more tomorrow or later.

But one thing to say now is that the assumptions are not random in TypeTopology. They are calculated, in our minds, to be as minimal as possible.

We don't just wildly start with any assumption and see what happens.

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

Written by Meven Lennon-Bertrand on 2024-09-06 at 13:35

@dimpase Assia Mahboubi's Fresco ERC grant (https://fresco.gitlabpages.inria.fr/) is supposed to go in that direction. She must have done a good literature review around that, but as far as I can tell it is not immediately available on the project's website, sadly… But you might have more chance by digging around some more?

=> More informations about this toot | More toots from mevenlennonbertrand@lipn.info

Written by Dima Pasechnik 🇺🇦 🇳🇱 on 2024-09-06 at 16:01

@mevenlennonbertrand thanks, it's a very useful reference. However, looking at what's on the page there, I see a DSL meant to produce e.g. certified GMP and BLAS replacements. So that seems to be a low level stuff - which in my particular case (combinatorics with a lot of finite fields and similar things) is tangential to what I need.

The paper is about describing SageMath (Python etc) implementation of constructions Hadamard matrices:

https://doc.sagemath.org/html/en/reference/combinat/sage/combinat/matrices/hadamard_matrix.html

A referee asked - hey, why don't you verify your constructions in a proof assistant?

I tried to explain in a revision, one thing led to another 🙂

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