[Agda] Agda student's research

[Peter Divianszky]

Hello,

Recently I began an informal Agda course at my workplace.
One of the participants is a mathematics student at ELTE Budapest 
University.
So far he likes Agda a lot and he plans to start an Agda
development which would do symbolic derivation with correctness proofs.
He could start with polynomials over a ring.

My question is, do you know of similar developments in Agda?

Thanks,

Peter