I'd love to see more OC on this site, but most of my content lately has been, uh, niche. Nonetheless, here is a little something that might be interesting to Devac at least :)

The golden ratio and the Fibonnaci numbers have a pretty neat relationship. I've been learning to use Coq, an interactive theorem prover, lately, and tried my hand at using it to prove the basics of this relationship. I was inspired by MIT's Introduction to Algorithms book (aka CLRS) which I've been reading bits of as part of a reading group.