ยง
Fungrim
https://fredrikj.net/math/fungrim2022.pdf
They want to integrate with mathlib to have formal definitions.