FLT proof as a single self-contained .olean

FLTShaken.ltar unpacks to one Lean .olean holding the transitive constant closure of fermat_last_theorem: 1,052,234 constants, no dependencies on other oleans. It is a drop-in replacement for the 375 GB build directory as the input to independent proof checking.

You should trust the safety and soundness of this artifact at most as much as the original source. Consider proper sandboxing before running any of the steps below.

download	1,088,752,089 bytes (1.01 GiB)
sha256	0b5b13ff88c30eaf078c676366b462dc70eb0809fb4e0754156c7df432bf8a87
unpacked	22,525,862,600 bytes (20.98 GiB), imports in 0.45 s
toolchain	Lean 4.33.1 (819816b2e0a3bf405af45ae5c7af2491d8f5bee6)
source	commit c2f7829b3

Exporting

You cannot use this artifact to load FLT in your IDE but you can run it through lean4export in order to run external checkers on it.

# `leantar` comes with Lean 4.33.1+
elan run --install leanprover/lean4:v4.33.1 leantar -x FLTShaken.ltar   # extracts lib/FLTShaken.olean

Build the exporter against the same toolchain — its lean-toolchain already pins v4.33.1:

git clone https://github.com/leanprover/lean4export
cd lean4export && git checkout 15f6055 && lake build && cd ..

Then export:

# consider adjusting parallelism
LEAN_PATH=$PWD/lib LEAN_NUM_THREADS=8 \
./lean4export/.lake/build/bin/lean4export FLTShaken -- \
  flt_pinned flt_mathlib fermat_last_theorem FermatLastTheorem \
  Nat String String.mk Char Quot Quot.mk Quot.lift Quot.ind \
  propext Quot.sound Classical.choice \
  Nat.add Nat.sub Nat.mul Nat.pow Nat.gcd Nat.div Nat.mod Nat.beq Nat.ble \
  Nat.land Nat.lor Nat.xor Nat.shiftLeft Nat.shiftRight \
  String.ofList Char.ofNat List eagerReduce \
  > flt.ndjson

Expect 37,770,970,450 bytes, sha256 208167cd2f562bf99aff54d2b71f24d271b44a29d8d525abc35c1e0ac54863cb, in about 44 minutes at 59 GB peak. Feed flt.ndjson to the checker of your choice.

Naming the constants after -- ensures the hash is reproducible by fixing the order of declarations, and makes this export identical to one taken directly from the full build.

Checking

The output has been built with in-process kernel checking disabled as the target is external checking. Testing on external checkers is in progress; at the time of writing, nanoda with patches from this repo (v0.4.13+instrumentation+E1+E2+E3, 16 threads) has succeeded:

Checked 1052234 declarations with no errors
24 min 05 s, 45.5 GiB peak