Huh. I’m reading this because I’m attempting to at least partially walk your path right now, although with a different set of math subjects (starting off with my lacking foundations in probability theory and Bayesian statistics, moving towards algebra and category theory, and also algorithmic information theory, and also wanting to work on my foundations in logic to accompany my healthy knowledge of computability theory).
Mostly I’m just finding that bashing my dopaminergic circuits with reward signals when studying helps to overcome the akrasia—to the point that I now find myself regularly tempted to study my unofficial material rather than work on my official research and coursework!
Also, I’ve discovered the CoqIDE theorem-proving assistant is about as addictive to me now as Legend of Zelda games used to be.
Huh. I’m reading this because I’m attempting to at least partially walk your path right now, although with a different set of math subjects (starting off with my lacking foundations in probability theory and Bayesian statistics, moving towards algebra and category theory, and also algorithmic information theory, and also wanting to work on my foundations in logic to accompany my healthy knowledge of computability theory).
Mostly I’m just finding that bashing my dopaminergic circuits with reward signals when studying helps to overcome the akrasia—to the point that I now find myself regularly tempted to study my unofficial material rather than work on my official research and coursework!
Also, I’ve discovered the CoqIDE theorem-proving assistant is about as addictive to me now as Legend of Zelda games used to be.
So, what you’re saying is that you’re addicted to Coq. :)
Tomoko scream