Following up on my work on Bayesian stats tools (PyMC): I have put together MCEx, a pretty nice package for messing around with MCMC package design. It’s considerably more modular than PyMC, far far smaller, has fewer features and uses Theano as its computational core (compiles to C, does graph optimizations, calculates derivatives). I have run into one major problem: I currently link Free Variables (parameters to fit) to prior distributions by passing them to a distribution function; I have been convinced(look for Anand’s comments near the bottom) this approach is Not Right, but the approach PyMC takes (free variables come from a prior distribution function) seems clunky and Not Right either. I suspect understanding this better requires me to learn more foundational probability theory. Probability Theory textbook recommendations welcome.
Learning Type Theory: Long ago, I asked about how to go about learning the foundations of math (link), I think what I was really interested in is how to do math formally, so you can drill down and understand all the component steps; math without any hand waving. After some exploration, I decided math through type theory and proof assistants seems like the most attractive option. Type Theory is attractive to me because I am a programmer and Type Theory promises a unification of math and computation.
My eventual goal is to understand type theory thoroughly enough to be able to build a proof assistant like Coq. My goal is not to build one, but just understand it well enough that I could be satisfied with my understanding when I work in Coq. I would also like to eventually write up a tutorial for how to repeat this learning process.
In the last month I’ve picked up this study again. I’ve read most of Type And Programming Languages, and I am now looking to gain more intuitive understanding by learning functional programming (Standard ML and Haskell because it seems to have better libraries). I am learning Haskell by writing interpreters for the various calculi in TaPL. My notes on learning type theory are here.
After some exploration, I decided math through type theory and proof assistants seems like the most attractive option.
I am fascinated by proof assistants, for approximately the same reasons you are. I think it would be very worthwhile for someone to put a real useable UI on top of a proof assistant, and sell it as an aid for learning mathematics. Keep us updated about what you find out.
Following up on my work on Bayesian stats tools (PyMC): I have put together MCEx, a pretty nice package for messing around with MCMC package design. It’s considerably more modular than PyMC, far far smaller, has fewer features and uses Theano as its computational core (compiles to C, does graph optimizations, calculates derivatives). I have run into one major problem: I currently link Free Variables (parameters to fit) to prior distributions by passing them to a distribution function; I have been convinced(look for Anand’s comments near the bottom) this approach is Not Right, but the approach PyMC takes (free variables come from a prior distribution function) seems clunky and Not Right either. I suspect understanding this better requires me to learn more foundational probability theory. Probability Theory textbook recommendations welcome.
Learning Type Theory: Long ago, I asked about how to go about learning the foundations of math (link), I think what I was really interested in is how to do math formally, so you can drill down and understand all the component steps; math without any hand waving. After some exploration, I decided math through type theory and proof assistants seems like the most attractive option. Type Theory is attractive to me because I am a programmer and Type Theory promises a unification of math and computation.
My eventual goal is to understand type theory thoroughly enough to be able to build a proof assistant like Coq. My goal is not to build one, but just understand it well enough that I could be satisfied with my understanding when I work in Coq. I would also like to eventually write up a tutorial for how to repeat this learning process.
In the last month I’ve picked up this study again. I’ve read most of Type And Programming Languages, and I am now looking to gain more intuitive understanding by learning functional programming (Standard ML and Haskell because it seems to have better libraries). I am learning Haskell by writing interpreters for the various calculi in TaPL. My notes on learning type theory are here.
I am fascinated by proof assistants, for approximately the same reasons you are. I think it would be very worthwhile for someone to put a real useable UI on top of a proof assistant, and sell it as an aid for learning mathematics. Keep us updated about what you find out.
Yes, part of the reason I am interested in this topic is that math seems like it should be taught formally.