The Natural Number Game suggests the possibility of rewriting mathematics textbooks with embedded interactive Lean code. I'm envisioning something like Google Colab or Mathematica, where you can insert either code blocks or text/LaTeX blocks.
Question: Is there already a good package for doing this?
If there were one, and it were available readily, this would accelerate the interface between mainstream mathematics and proof assistants. (Imagine classic mathematics texts rewritten with embedded code exercises.)
The best so far, to my knowledge, Patrick Massot's formatter discussed here, and maybe this is good enough? I'd be interested in knowing what is being done, and collecting the results here.
(Maybe this is CW?)