Discussion: Auto Polynomial

Stream: general

[Kenny Lau]

@Liam Schilling well done! is there a plan to integrate this into mathlib?

[Notification Bot]

A message was moved here from #announce > Auto Polynomial: An Experiment in Reflection for Polynomials by Floris van Doorn.

[Liam Schilling]

Since most of our systems are ad hoc and our tactics are specific-purpose, I'm not sure yet whether trying to directly integrate into Mathlib is the right way forward. I think that investigating the newly built-in Grind.CommRing.Poly type and the automations it provides will make the best way to bring our kind of automation to Mathlib more clear. I also imagine there is a lot of further work onPoly itself that we could contribute to Mathlib!

[Kevin Buzzard]

So we waited 5 years for computable polynomials and then two independent projects announce them on the same day?? #announce > Computable MvPolynomial + RingEquiv with MvPolynomial @ 💬

[Matthew Ballard]

So which one is faster...?

[Eric Wieser]

To save someone the click, that one has signature

abbrev CMvPolynomial (n : ℕ) R [Zero R] : Type

(and so quite reasonably requires you to number your variables in exchange for efficient computability)