lean4 on android/ios ?

Stream: general

[TongKe Xue]

Has anyone managed to get Lean4 to run on Android/iOS? (Without the support of an external server -- i.e. needs to work even without wifi/data connections.)

[Context: thinking more about Lean4 x Gaming, and the possibility of doing lean4 proofs on a mobile interface, using thumbs to drag parts of equations to cancel, etc ... ]

[Snir Broshi]

I saw an image of Lean running on VSCode inside of a SteamDeck, but I can't remember where.
(Edit: it's on the lean-memes channel of the Lean discord, at Nov 2025)
Since Lean works (or used to work) on WASM there shouldn't be anything preventing us from building it for Android/iOS. Have you tried building it? Did you get build errors?

[TongKe Xue]

1. I have not tried building Lean4 on Android/iOS.

2. I spent a solid few days trying to get Lean4 to build on wasm32, failed to even replicate the 100k export limit error:
   #general > what is lean.js
   #general > reproducing lean4 wasm32 build of 100k export error

• a number of private conversations

and have not tried any custom Lean4 build since.

[TongKe Xue]

My limited understanding of the issue is:

1. Lean4 builds in "stages"
2. Thre is a single CMakefile (complicated, I don't understand its internals) which governs how Lean4 builds the "stages"
3. This had complications for me (even trying to replicate the wasm32 100k export issue)
4. Hacking this CMakefile is likely at the heart of getting it to build on Android/iOS.

Do you have any experience hacking this CMakefile ?
https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

[Snir Broshi]

TongKe Xue said:

Do you have any experience hacking this CMakefile ?

I don't, but I'm willing to try to get a working WASM build.
Do you think the WASM build will be performant enough for your use case on Android/iOS?

[TongKe Xue]

Most of the useful advice in this post comes from others (but in DMs, and I don't know if they want to be named), so I'm not attributing anyone here.

I'm currently taking a break from trying to get the Lean4/wasm32 build to work. If I were trying to get it to work, I would:

1. use the CI file from https://github.com/leanprover/lean4/pull/2855/files
2. glone the repo, checkout the tag of that commit
3. try to replicate the CI environment

My failure is on the last step, where I can not get it to link vs 32-bit gcc on my system:

make
[  6%] Performing build step for 'stage0'
[  0%] Built target initialize
[ 13%] Built target util
[ 25%] Built target kernel
[ 39%] Built target library
[ 44%] Built target constructions
[ 63%] Built target compiler
[ 63%] Built target leancpp
[ 63%] Built target make_stdlib
[ 81%] Built target leanrt_initial-exec
[    ] Building /home/y/tst/lean4/build/rel32/stage0/lib/lean/libleanshared.so
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libstdc++.so when searching for -lstdc++
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libstdc++.so when searching for -lstdc++
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/lib/gcc/x86_64-unknown-linux-gnu/12.3.0/../../../../lib/libstdc++.a when searching for -lstdc++
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/lib/gcc/x86_64-unknown-linux-gnu/12.3.0/../../../libstdc++.a when searching for -lstdc++
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: cannot find -lstdc++: file in wrong format
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libstdc++.so when searching for -lstdc++
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libstdc++.so when searching for -lstdc++
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/lib/gcc/x86_64-unknown-linux-gnu/12.3.0/libgcc.a when searching for -lgcc
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/lib/gcc/x86_64-unknown-linux-gnu/12.3.0/libgcc.a when searching for -lgcc
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: cannot find -lgcc: No such file or directory
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libgcc_s.so.1 when searching for libgcc_s.so.1
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libgcc_s.so.1 when searching for libgcc_s.so.1
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libgcc_s.so.1 when searching for libgcc_s.so.1
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: cannot find libgcc_s.so.1: No such file or directory
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libgcc_s.so.1 when searching for libgcc_s.so.1
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/n7pvb7gdf1g6dvj7sl92i882qjl4kyx9-gcc-12.3.0-lib/lib/libgcc_s.so.1 when searching for libgcc_s.so.1
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/lib/gcc/x86_64-unknown-linux-gnu/12.3.0/libgcc.a when searching for -lgcc
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: skipping incompatible /nix/store/2vwipws2crqcjxfzjyq9rjpk61iqf7pf-gcc-12.3.0/lib/gcc/x86_64-unknown-linux-gnu/12.3.0/libgcc.a when searching for -lgcc
/nix/store/fx1h3mmzl2hjci3nn15n26r57mc3cs3z-binutils-2.40/bin/ld: cannot find -lgcc: No such file or directory
collect2: error: ld returned 1 exit status
make[6]: *** [/home/y/tst/lean4/build/rel32/stage0/stdlib.make:48: /home/y/tst/lean4/build/rel32/stage0/lib/lean/libleanshared.so] Error 1
make[5]: *** [CMakeFiles/leanshared.dir/build.make:71: CMakeFiles/leanshared] Error 2
make[4]: *** [CMakeFiles/Makefile2:1279: CMakeFiles/leanshared.dir/all] Error 2
make[3]: *** [Makefile:146: all] Error 2
make[2]: *** [CMakeFiles/stage0.dir/build.make:86: stage0-prefix/src/stage0-stamp/stage0-build] Error 2
make[1]: *** [CMakeFiles/Makefile2:95: CMakeFiles/stage0.dir/all] Error 2
make: *** [Makefile:136: all] Error 2

Now, a reasonable question to ask is why try that commit -- rather than the latest. The issue is -- on the most recent Lean4 source, I can't even hit the "wasm 100k export limit error" -- something is breaking down before then. And the point of using the above CI / Commit, is you want to get to a point you can replicate the wasm32 build process.

I do not know if wasm32 will be performant enough on Android/iOS.

[Anthony Wang]

TongKe Xue said:

Has anyone managed to get Lean4 to run on Android/iOS? (Without the support of an external server -- i.e. needs to work even without wifi/data connections.)

At least for Android, this has been asked before such as in #general > Lean on Android. Not sure about iOS though.

[TongKe Xue]

Nice; thanks! I didn't realize (1) Android was that close to "stock" Linux and (2) MathLib cache size is the core problem.