Gaussian Quadrature / Orthogonal Polynomials

Stream: Is there code for X?

[giacomo gallina]

Hi, me and a few of my friends were searching for some theorems to formalize in Lean as part of a university exam, and it would be cool if we could use this opportunity to contribute to mathlib. I was thinking that a few theorems on orthogonal polynomials and gaussian quadrature could be feasible, and I didn't find them in mathlib, although I'm new to Lean so maybe I just missed them. Do you know if they are really missing from mathlib? Or if there's someone already working on them? Thanks for the help, and sorry if this isn't the right stream to ask this!

[Johan Commelin]

Welcome! It doesn't ring a bell for me. But I'm not the expert on that part of mathlib.