## § Fungrim

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