I think the biggest jump between interactive theorem provers like Lean "normal" languages is the "interactive" part: Lean or Coq or the like really work well in a specialized IDE mode where you're editing the file and getting instant feedback about the state of your proof. You might be able to get a Python DSL to work, but there would be a lot of tooling work involved to pipe everything back.
You can write proofs in a non-interactive way, but you're signing yourself up for a lot of tedium.
EDIT: A video showing someone working through some simple stuff. You can obviously do a lot of things "in your head" but having the feedback loop is helpful. Though thinking about it more I don't think this precludes a Python DSL entirely. It would just require some smart design to support this form of interactivity. https://www.youtube.com/watch?v=VYFTph2izIs
That sounds... contradictory, isn't it? Python is immensely hostile to static analysis (note that I write this as someone who writes Python for a living, using pyright/mypy). If you remove the ability to perform static analysis from Lean, what's left?
Or do you mean a Python-like syntax on top of Lean4?
Note: Pretty sure that libtorch is written in C++ and CUDA.
