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.

kingmudsy:

Wow, Coq is *not* intuitive to me! This is really cool, though - super functional, which is an aspect of programming I've wanted to explore more. I had a little boilerplate Haskell game awhile ago, but I can't seem to find it on GitHub...

Something about how your rules are started with "Lemma" and ended with "QED" is funny to me, but maybe I'm just being a big nerd :)

posted by ilex: 76 days ago