Running lean on Android

Stream: new members

[Vivek Rajesh Joshi]

Simple question: Is there any way to run Lean4 on an Android tablet? Like is there any android software that can run Lean or is it only possible through VS Code on Windows?

[Anand Rao Tadipatri]

The Lean web editor (https://live.lean-lang.org/) works on mobile devices too and may be sufficient for simple use cases.

[Kevin Buzzard]

I had Lean 3 running on an android phone, but it was rooted and I installed an Ubuntu chroot on it, installed Lean 3 following the instructions for linux and then used emacs as an IDE. Probably one could try the same thing with Lean 4 but I would not expect a good experience in some sense (at the very least you'd need a bluetooth keyboard to stop the builtin keyboard taking up half the screen; this is how I used the phone).