← Stacks · lean-pkg documentation

lts-2026.10: Lean v4.35.0, Mathlib v4.35.0

The first lean-pkg LTS stack (proposal 0004, accepted 2026-10-17). The machine-readable file is lts-2026.10.yaml (schema lean-pkg-stack/1).

Status: declared 2026-10-18 by the maintainer. The declaration covers the five stage 0 matrix entries that reach receipts on the stack (below). gromov-filling-lean, the sixth, is a documented migration case outside the declared matrix: its JordanCurveTheorem dependency is still on Lean v4.29.0 and does not build on Mathlib v4.35.0 (migration notes).

A stack is a tested combination that later lean-pkg releases keep working on; it is not a certificate that the toolchain has no kernel bug.

The pins

	Pin
Lean toolchain	leanprover/lean4:v4.35.0 (tag commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, released 2026-10-12)
Mathlib	tag v4.35.0, commit 56a005855ea17e0b0958f73ec801ae140b0a1679 (2026-10-13, “chore: bump toolchain to v4.35.0”)
lean-pkg	>=0.12.0,<1.0: every lean-pkg release from 0.12.0 on, until the 1.0 freeze
Supported until	2028-04-30 (about 18 months)
Successor	none yet (lts-2027.04)

The Mathlib commit is recorded beside the tag because a tag can be moved; git ls-remote https://github.com/leanprover-community/mathlib4 refs/tags/v4.35.0 printed that commit on 2026-10-17.

Palomar floor. lean-pkg’s pinned Palomar rules require a toolchain of at least v4.35.0-rc2 (the first with lake comparator). v4.35.0-rc2 ≤ v4.35.0, so packages on this stack can be Palomar-graded. Strictly, the held-back rule of the proposal would pick v4.34.1 on 2026-10-17; that is below the floor, and the floor wins (open question 2, decided).

Comparator tools

On this toolchain the comparator receipt uses the toolchain mechanism (comparator): the toolchain’s own lake comparator, with its bundled kernels. The stack pins them as v4.35.0 ships them, read from src/CMakeLists.txt of leanprover/lean4 at the tag commit:

Tool	Source	Pin
lake comparator	in-tree (src/lake, Lake/CLI/Check.lean)	the toolchain commit
leanexport	in-tree (src/LeanExport)	the toolchain commit
leanchecker	in-tree	the toolchain commit
NanoDa (nanoda_bin)	ammkrn/nanoda_lib	3a2407216ee84a75f9e1aead6803d0578be06ae7
con-ron	leanprover/con-ron	dd8d8218892c871276b1e569d3decbb368bba1b6

The SHA-256 of each binary in the Linux release asset lean-4.35.0-linux.tar.zst (asset digest 7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d) is in the YAML file under comparator_tools.binaries_sha256, keyed as the comparator receipt’s toolchain digests (lake_sha256, leanexport_sha256, leanchecker_sha256, nanoda_bin_sha256, con-ron_sha256). A comparator receipt made on this stack on Linux x86_64 should record exactly those.

Using the stack

With a lean-pkg that has stage 1 (after 0.14.0), lean-pkg new NAME --stack lts-2026.10 starts a package on the stack, and stack: lts-2026.10 in coverage.yaml opts an existing one in; lean-pkg doctor NAME then says whether its committed pins match (how to opt in). An existing package moves to the stack by hand:

1. lean-toolchain: leanprover/lean4:v4.35.0.
2. The Mathlib require in the lakefile: rev = "v4.35.0" (lakefile.toml) or @ "v4.35.0" (lakefile.lean).
3. lake update (on this Mathlib it also fetches the build cache), then lake exe cache get, then lake build of the package’s modules.
4. stack: lts-2026.10 in coverage.yaml, to opt in (needs a lean-pkg after 0.14.0; older ones refuse the key).
5. A new commit and new receipts (lean-pkg verify); the old receipts keep binding the old commit.

The stage 0 matrix

Each entry is a fresh scratch copy (never pushed, never leased, with a throwaway registry), moved to the pins above, then lake update, lake exe cache get and lake build, then verify (the comparator receipt and the lower-tier receipt at one commit, and the gate), page --write, publish --dry-run and receipt check. All six ran on 2026-10-17 on one Linux laptop (24 CPUs), one entry at a time, capped at 8 CPUs (CPUQuota=800%, LEAN_NUM_THREADS=8). Wall time, CPU time and peak memory are the cgroup’s (cpu.stat, memory.peak), so every child process counts. The Mathlib cache was cold for the first entry and shared after that.

Entry	Moved	lake update + cache	lake build	Peak memory (update / build)	verify	page –write	publish –dry-run	receipt check
new --kind paper	pins only	41.5 s wall, 83.2 s CPU (cold)	9.4 s, 12.1 s CPU	9.5 GB / 2.0 GB	ok, 38 s	ok	push and consent open	PASS (14/14)
new --kind library	pins only	35.5 s, 73.7 s CPU	7.8 s, 11.5 s CPU	8.7 GB / 1.6 GB	ok, 37 s	ok	push and consent open	PASS (14/14)
π-λ tutorial	pins only	36.7 s, 73.8 s CPU	7.3 s, 11.6 s CPU	9.2 GB / 1.5 GB	ok, 51 s	ok	push and consent open	PASS (14/14)
markovprocess-pilot	lakefile only	36.5 s, 75.8 s CPU	54.8 s, 313.9 s CPU	8.8 GB / 3.9 GB	ok, 188 s	refused (pre-existing)	5 open (below)	FAIL 2 (pre-existing)
total-coloring-lean	33 edits in 14 files	35.3 s, 77.6 s CPU	48.1 s, 223.3 s CPU (clean)	8.6 GB / 4.8 GB	ok, 143 s	refused (pre-existing)	5 open (below)	FAIL 2 (pre-existing)
gromov-filling-lean (migration case, outside the declared matrix)	blocked	15.1 s, 56.4 s CPU	failed: 57 errors, 72.5 s, 498.4 s CPU	8.4 GB / 3.9 GB	not reached

The lake exe cache get after lake update took 2.5 to 3.1 s wall each time: on this Mathlib, lake update downloads the cache itself (Mathlib’s post-update hook, 9,031 files cold), so the explicit step only confirms it. The cache download’s peak memory, about 9 GB, is the largest of any step; each checkout holds 7.3 to 7.7 GB under .lake. The verify column is the end-to-end wall time of both receipts and the gate.

Receipts. Every entry that reached verify has a comparator receipt (mechanism toolchain, toolchain leanprover/lean4:v4.35.0) and a lower-tier receipt bound to the same commit, with sorry count 0 and only the standard axioms. Their SHA-256:

Entry	Comparator receipt	Lower-tier receipt
new --kind paper	f981cf8c9494cfe56af3385b009535b0a54ff8bdcd0dcf7e27517e1405c2150a	7b457f4de3e11c2e83bb41a0dd2e1cf810c463143078ea594202e15fe8e81e7a
new --kind library	c5d975fe42a78d298b48675cda319c5c6bf9a1e8c4be5c4371c784d9702790ae	f6fd974863528c073af9c8e6568e8ec8119e79caeff4c6e77b85e87c71c2e40d
π-λ tutorial	172fa29ecb8fd5defb56bb1ca47f9ce788ae86de1464023ea55c8f1d7cfe2dcf	57ffda91ffcdbcb6e06b6dc69a49ce80590819ca2f40b8d68c93f61f6afc288f
markovprocess-pilot	7a672169f1b3cfdbf5f182e78e0bfbb729dbac92a056f6b6ac1dd0b86015001b	27e2dab04cd8844616038a6c300241c5bbd1f3b4a4e2c88bf86028a765954bbd
total-coloring-lean	deb546772ace8e1394c1015ddcc08baa331c540634bc90a752acef036fff6d23	969dde9443bbe62ccbee413f6d3ef6948ba188f2e41afb6c2493bb7787db09cd

The receipts bind scratch commits that exist nowhere else; the hashes record that the run happened, not a published artifact.

Digest check. Each of the five comparator receipts records the toolchain digests lake_sha256, leanexport_sha256, leanchecker_sha256, nanoda_bin_sha256 and con-ron_sha256. All five match comparator_tools.binaries_sha256 in the stack file exactly.

publish –dry-run. A scratch copy is never pushed and has no recorded author consent, so those two items stay open for every entry by design. markovprocess-pilot and total-coloring-lean also have no REUSE licensing data, and their claims ledger and page fail for the reason below.

Migration notes

• Scaffolds and tutorial: no source change. lean-pkg 0.12.0’s scaffold pins v4.35.0-rc2 (toolchain and Mathlib); moving it is the two-line pin change. The π-λ tutorial’s Lean files, copied verbatim from the tutorial, build unchanged. For the paper scaffold an author must first fill coverage.yaml (its FILL-ME markers are refused by design) and name a posted manuscript version: the run used a one-theorem sample note pinned as {repo, commit, sha256}, since an unposted version fails receipt check’s coverage check.
• lake build with no target builds nothing in the scaffold. On Lean v4.35.0 Lake prints no targets specified and no default targets configured (“This will be an error in a future version of Lake”), because the scaffold’s lakefile.toml has a [[lean_lib]] but no defaultTargets. The scaffold’s own next steps name the modules (lake build MOD.Solution MOD.Axioms), which build. A stage 1 scaffold for the stack should add defaultTargets.
• markovprocess-pilot: a transitive Mathlib. The package requires only MarkovProcess, whose newest commit is still on v4.35.0-rc2. It moves by adding its own require mathlib at rev = "v4.35.0"; Lake then resolves Mathlib to the stack commit, and MarkovProcess and the package build with no Lean change. Lake warns that a solution file imports Mathlib without module.
• total-coloring-lean: v4.32.0 to v4.35.0. With warningAsError = true, deprecations are errors. 33 one-line edits in 14 files: Set.mem_setOf_eq to Set.mem_ofPred_eq; dif_pos and dif_neg to dite_eq_left and dite_eq_right; letI to let where the goal is a proposition (a new linter); the arguments of SimpleGraph.mem_incidenceFinset became implicit; and three proofs of _ :: _ ≠ [] where simp no longer closes a goal that is not type-correct after unfold, replaced by List.cons_ne_nil. The comparator moves from the legacy mechanism to toolchain.
• gromov-filling-lean: v4.29.0 to v4.35.0, a migration case outside the declared matrix. Its require mathlib must come after its JordanCurveTheorem dependency in lakefile.lean, or that dependency’s transitive pins win (Lake says so). The first build then stops at 57 errors in 15 modules. Most are the package’s own compatibility lemmas that Mathlib now has (has already been declared: Circle.angleDiff, Affine.Simplex.closedInterior_*, Finset.powersetCard_biUnion and others), plus about twenty proof breaks. Four are in the third-party JordanCurveTheorem dependency (SectionE_Parity, where decide, Even and Multiset membership elaborate differently), whose newest commit is on v4.29.0. Moving this package needs that dependency moved upstream, or a patched copy, which is its authors’ choice; then the package’s own migration (the compatibility lemmas removed, the proofs repaired, and a new build to find what the first frontier hid). Once it reaches receipts it can join the stack’s matrix.
• Known, pre-existing, not caused by the stack. markovprocess-pilot and total-coloring-lean compare declarations in an Audit namespace, while their claims name the library declarations. lean-pkg 0.12.0’s claimed-theorems and coverage (R11) checks therefore fail. The mapping lives in their index entries (judged_as), which claims.yaml cannot express. receipt check on an untouched clone of markovprocess-pilot at its index pin fails the same check. That clone’s receipts also bind 9bb873e7aa31, an earlier commit whose sources differ from the pin, so its binding check fails too. For the run, each of these two packages got a scratch verify.sh (the scaffold’s, with its modules) and a library coverage.yaml, kept with the migration patches outside the repository.

The lab’s packages (read-only survey)

The lab registry’s 43 packages, by the toolchain each one records (2026-10-17; nothing built):

Distance from the stack	Packages	Toolchains
Same toolchain (v4.35.0)	14	13 also on the stack’s Mathlib commit; 1 on another Mathlib commit
One release behind	9	6 on v4.34.1, 1 on v4.34.0, 2 on v4.35.0-rc2
Older	20	14 on v4.32.2, 1 each on v4.32.0, v4.34.0-rc2, v4.33.0-rc1, v4.29.0, v4.17.0, v4.11.0-rc2

Of the 20 older ones, 15 are active, 2 public, 1 verified-private, 1 archived and 1 scratch. Whether lab packages are expected to stay on a stack is open question 6 of the proposal, still open.