Low hanging fruits?

Stream: Computer algebra

[Ilmārs Cīrulis]

The first idea that comes to mind is solving system of linear equations over field, ring, something else too, maybe.

One provides coefficient matrix and vector of constant terms with in the structure with all necessary operations computable, then Lean provides the solution. Which should be the simplest case of SLE solving.

Does this make any sense? :sweat_smile:

[Ilmārs Cīrulis]

It's this overwhelming silence from the 4th of February that motivated me to post here.

And it could be interesting for me to implement something relatively easy.

[Jacques Carette]

In CAS circles, people make a difference between "computational algebra" and "symbolic computation". Computational algebra has sophisticated algorithms but straightforward semantics -- and thus indeed 'low hanging fruit' for mathlib.

Symbolic computation is a very different kettle of fish as the semantics is often ill-defined. More precisely, a lot of algorithms are only defined operationally with vague (at best) denotational semantics. And since mathlib does extensional mathematics, a lack of denotational semantics is a serious problem.

[Kim Morrison]

Factoring polynomials over finite fields (an effective algorithm, with a computational representation of polynomials) seems like one of the obvious next steps, that I would love to see progress on.

[Jacques Carette]

Factoring polynomials over finite fields

This is indeed one of the foundational cornerstones of modern CASes.