I've been learning about free objects in category theory.Bartosz Milewski's Category Theory for Programmers has been particularly very informative.
An investigation into what assumptions which you can derive the ubiquitous lerp function and it's proprieties.
Playing with the Hom Functor to better understand it.
I'm hoping to prove Zeckendorf's theorem in Coq without reference as a personal challenge.
I'm trying to (mostly) faithfully translate a theorem from the Bird-Meertens Formalism Wikipedia article into Coq.
A small project. I'm just playing with Coq.
An attempt to recreate a simple proof that all functions between fields can be decomposed into the sum of an even and an odd function.
Playing with Tarski's axioms for Euclidean geometry.
