packaging Lean in apt for Claude?

Stream: Machine Learning for Theorem Proving

[Jason Gross]

When asked to write Rocq, Claude (web chat interface) will apt install coq to test it. When asked to write Lean, Claude will note that GitHub is blocked and doesn't manage to install Lean. Does anyone want to package Lean in a launchpad ppa to fix this?

[Justin Asher]

Is this possible or practical?

I just had Claude poke around in the sandbox VM that it can spin up, and it told me it contains about 10 GB of storage. Installing Mathlib/Lean takes up about 8 GB.

[Adam Topaz]

Is it possible to configure the claude sandbox? FWIW, I use my coding agents (via opencode) in incus containers.

[Justin Asher]

It might be easier to connect Claude via an MCP tool/connector to Lean 4 Web (https://live.lean-lang.org/).

[Adam Topaz]

I don't think going through the web editor is a good idea. That doesn't really scale to actual Lean development/proof writing, and if many people do this it would put unnecessary strain on the servers that host the web editor.

[Yury G. Kudryashov]

It should be possible to package elan for apt.

[Yury G. Kudryashov]

UPD: It looks like it's packaged.

[Yury G. Kudryashov]

Ubuntu has a elan package. It's at version 3.1.1 in 25.10.

[Yury G. Kudryashov]

Why installation of Lean takes so much space (8 GB)? I saw Docker images with Lean+Mathlib that are smaller.

[Li Xuanji]

I think it depends on whether you look at the compressed / uncompressed docker image (the docker registries I know like docker hub and GHCR all store compressed images) and whether the image is designed to download additional stuff after pull (e.g. the docker image produced by https://github.com/leanprover-community/mathlib4/blob/master/.docker/gitpod/Dockerfile doesn't contain Mathlib)

I was recently creating docker images where the image contains Mathlib and the prebuilt oleans (so in theory, after pulling the docker image, you can test code against Mathlib without an internet connection); the compressed size is 3.58 GB and the uncompressed size is 10.14 GB. You can test it out with this one-liner:

docker run --rm ghcr.io/ldct/mathlib4:v4.27.0 bash -c 'cd /project && echo "import Mathlib" > T.lean && lake env lean T.lean && echo ok'

And here's claude's breakdown of what takes up space in the uncompressed image

=== FULL IMAGE BREAKDOWN ===

--- Base OS (Ubuntu 24.04) ---
173M    /

--- Lean toolchain (/root/.elan) ---
  lib/lean/Lean (compiler+stdlib olean):
1.1G    /root/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean/Lean/
  lib/lean/Init:
349M    /root/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean/Init/
  lib/lean/Std:
293M    /root/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean/Std/
  lib/lean/Lake:
93M /root/.elan/toolchains/leanprover--lean4---v4.27.0/lib/lean/Lake/
  bin:
6.4M    /root/.elan/toolchains/leanprover--lean4---v4.27.0/bin/
  src:
29M /root/.elan/toolchains/leanprover--lean4---v4.27.0/src/
  elan itself:
13M /root/.elan/bin/

--- Mathlib build artifacts (/project/.lake/packages/mathlib/.lake/build) ---
  .olean files (compiled modules):       1798 MB
  .olean.private files:                  2875 MB
  .olean.server files:                   96 MB
  .ilean files (interface):              237 MB
  .c / .ir files (C codegen):            123 MB
  cache binary:                          175 MB
  hash/trace (metadata):                 ~2 MB

--- Other .lake packages ---
152M    /project/.lake/packages/batteries/
134M    /project/.lake/packages/aesop/
42M /project/.lake/packages/proofwidgets/
24M /project/.lake/packages/Qq/
12M /project/.lake/packages/plausible/
5.6M    /project/.lake/packages/importGraph/
5.2M    /project/.lake/packages/LeanSearchClient/
512K    /project/.lake/packages/Cli/

--- Mathlib source ---
102M    /project/.lake/packages/mathlib/Mathlib/

(If anyone is curious, I'm trying to package these dockerfiles to run as Cloudflare containers, which should scale up nicely. Here's a cURL command which runs against a containers that has lean but no Mathlib: curl -X POST https://lean4-servers.xuanji.workers.dev/lean-4-27-0 -d '#check Nat.add_comm')

[Jason Gross]

Hm, even though elan is packaged, it can't install lean b/c elan goes through github to get Lean. (I tried to get claude to install it here.)

[Kevin Buzzard]

(I just use Claude code locally if I want Claude to write lean code)

[Kim Morrison]

If you want to use claude.ai, you will need to go to https://claude.ai/settings/capabilities and add *.githubusercontent.com and *.lean-lang.org to the "Additional allowed domains". After that it seems to work fine: https://claude.ai/share/1e1e988c-3849-4e8a-a22c-aeb6fd546eb5

[Kim Morrison]

I've also connected to Claude Code Web to various lean repositories, after creating a new environment with liberal (the above, or even *) permissions for accessing other hosts.

[Kim Morrison]

But both of these options are incredibly slow and painful compared to use Claude Code, and as such I don't think it is valuable to move things away from *.githubusercontent.com or *.lean-lang.org to support this use case.

[Franz Huschenbeth]

Kevin Buzzard said:

(I just use Claude code locally if I want Claude to write lean code)

https://simonwillison.net/2025/Jun/16/the-lethal-trifecta/

In case you have not heard of the lethal trifecta :)

[Justin Asher]

Franz Huschenbeth said:

In case you have not heard of the lethal trifecta :)

I wonder how long until we have our first large-scale bug caused by LLM prompt injection.

[Li Xuanji]

Kevin Buzzard said:

(I just use Claude code locally if I want Claude to write lean code)

For those people interested in running claude code on Some Else’s Computer, I found exe.dev pretty good for this at $20/mo (persistent VMs for installing lean, web UI to talk to the LLM, LLM UI preinstalled)