Coding the matrix

I thoroughly admire efforts to turn mathematics into code – in the legacy of Coding the Matrix. A new book is being released on the topic of Logic: Mathematical Logic through Python. Proof assistants (the likes of Lean) are being continuously developed and becoming more and more mainstream by the hour. I am pretty sure developments in these fronts will revolutionise the teaching of mathematics, making them accessible to whole groups of hobbyists, the same way that autodiff revolutionised ML.