From the podcast episode they talk about the idea of using an LLM for training by disallowing the model to write code. I've been experimenting with exactly that in conjunction with a proof checker (Agda) to help me learn some cubical type theory and category theory.

I find the LLM as interactive tutor reviewing my work in a proof checker to be a really killer combo.