Proofs

Open on GitHub

Free Monoid Proof

Free Monoid Proof

I've been learning about free objects in category theory.

Bartosz Milewski's Category Theory for Programmers has been particularly very informative.

Open on GitHub

Lerp Reverse Maths

Lerp Reverse Maths

An investigation into what assumptions which you can derive the ubiquitous lerp function and it's proprieties.

Open on GitHub

Hom Functor Play

Hom Functor

Playing with the Hom Functor to better understand it.

Open on GitHub

Zeckendorf Proof?

Zeckendorf

I'm hoping to prove Zeckendorf's theorem in Coq without reference as a personal challenge.

Open on GitHub

Bird-Meertens MaxSegSum

Zeckendorf

I'm trying to (mostly) faithfully translate a theorem from the Bird-Meertens Formalism Wikipedia article into Coq.