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 the assumptions from which you can derive the ubiquitous lerp function and it's properties.
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.
Playing with Taylor polynomials using 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.
A Complex Equation Envelope.
A Coq proof regarding a simple question about voting.
An investigation into the superposition principle for differential equations.
An extension of my free monoid project with a scope expanding into group theory.
