Zulip Chat Archive
Stream: general
Topic: Lean on Android
Julian Berman (Jul 29 2025 at 09:21):
It was never impossible to run Lean on Android (in a second Kevin will come around saying he had emacs running Lean on a phone in 2007), but as an FYI to anyone who wants Lean on the go, now that Android 15 has added an official Linux Terminal app which is just Debian in a VM, it's essentially trivial to run Lean on Android compared to doing so in Termux. I followed the normal installation instructions for elan, and here's lean.nvim running on my Pixel 7 (I'm sure the emacs plugin would work too):
I haven't tried the Mathlib cache because I've not got enough space free to do so on this device, but I would strongly suspect everything just works now.
Arthur Paulino (Jul 29 2025 at 10:22):
This is awesome. My mind went straight to the potential of using Lean on tablets in math classes
Kevin Buzzard (Jul 30 2025 at 20:41):
It was 2017 :-) (and it was rooted)
Frederick Pu (Nov 26 2025 at 23:55):
downloads mathlib cache ... phone crashes
Frederick Pu (Nov 26 2025 at 23:55):
(my phone can barely run the camera app)
Kevin Buzzard (Nov 27 2025 at 00:59):
I'm not sure I ever had mathlib running natively :-) (and there was no cache back then, although mathlib was only 30K lines of code back then too)
Anthony Wang (Nov 27 2025 at 01:56):
(deleted)
Julian Berman (Nov 27 2025 at 01:56):
Yeah well, it's the future, here in 2025 we now have truly marvelous proofs whose size fits (barely) in the size of our disks:
Screen_Recording_20251126_205349_Terminal.mp4
Frederick Pu (Nov 27 2025 at 16:40):
wait how much disk is mathlib
Frederick Pu (Nov 27 2025 at 16:40):
i maxed out the disk on my school lab machine by git pulling from mathlib
Etienne Marion (Nov 27 2025 at 16:51):
Around 8GB
Ruben Van de Velde (Nov 27 2025 at 19:14):
The code itself not so much, right? But lake exe cache get pulls down compiled code which is an order of magnitude larger, as I recall
Gavin Zhao (Nov 27 2025 at 19:16):
Now that Android has experimental desktop mode, you can connect your phone to an external display and run the Linux Terminal app on it with Lean and Neovim installed...
Gavin Zhao (Nov 27 2025 at 19:21):
All I need is for the Android desktop mode to get mature so I no longer need a laptop, just a small portable display + phone + 60% keyboard.
Last updated: Dec 20 2025 at 21:32 UTC