Two weeks, 208 proved float kernels: what the FloatLib competition found

From 14 to 28 October 2026, miners on the subnet competed to make IEEE-754 floating-point arithmetic in Lean faster without giving up a single bit of correctness. A submission was one Lean file with four binary32 kernels: add and mul on single floats, sum over a vector and bmm, a batched matrix multiply. Each came with a machine-checked proof that it returns exactly what FloatLib's specification returns, for every possible input. The validator checked the proof, timed the file against the reigning champion, and crowned it if it was at least 3% faster.

339

submissions from 26 operators (coldkeys)

326

passed the proof gate; 208 of them distinct files, the rest byte-identical resubmissions

38

takeovers, each one checked by a bootstrap over 25 paired timing rounds

184

of the 208 files run on the hardware FPU and prove that they are allowed to

We wanted to answer two questions at the end. How fast are the final kernels on inputs nobody was scored on? And how far is that from plain, unproved hardware floats?

What a submission had to prove

The proofs cover every input: NaNs, infinities, subnormals, signed zeros, every vector length and every matrix shape. sum adds from +0 in index order, and bmm accumulates acc + a·b in reduction order, so reordering the additions or fusing a multiply-add is not exact and not allowed. Files were capped at 256 kB, only Lean's three standard axioms were accepted, and escape hatches such as native_decide and implemented_by were banned.

A new entry took over when the ratio of its fastest rounds to the champion's was at most 0.970, and a bootstrap over 25 paired rounds agreed that its median round was faster. The last three champions shared the payout 60/30/10.

There were two benchmarks. Until the afternoon of 22 October, entries were timed on 12 fixed, public input classes: one sum length (1,000), one bmm shape (50×100×50), and not a single NaN, infinity or subnormal. From then on, every run drew about 200 cases from a private suite: ML-like values, sparse inputs, extremes, specials, subnormals, and wide ranges of lengths and shapes. Miners got a public twin of it to tune on.

One idea from the first day

Since Lean 4.34, Float32, the machine's own float type, has a logical model inside Lean. It compiles to the CPU's float instructions, but you can also prove theorems about it, and Lean's documentation invites float libraries to prove their operations equal to it.

Entry #9 did exactly that on 14 October at 15:50 UTC. It computes on the hardware, proves that whenever the hardware result is not NaN it equals the IEEE specification, and falls back to the slow proved software kernel otherwise. NaNs are the one place where the two can differ: Lean's model has one canonical NaN, and FloatLib's specification keeps NaN payloads. #9 took over seven minutes later. By the end, 184 of the 208 distinct files worked this way.

The idea is at its best in a loop, because a NaN anywhere in a sum carries through to the end.

Summing on the FPU, with a proof that it is allowed to

Ordinary inputA NaN at step 8

1. 10.75
2. 2-1.5
3. 32.25
4. 40.1
5. 53
6. 6-0.625
7. 71.2
8. 80.05
9. 9-2
10. 104.5
11. 110.3
12. 12-0.8

acc = 0

0 on hardware · 0 in software

• Hardware Float32
• NaN carried through
• Proved software kernel

bmm works the same way, one dot product per output: each runs in hardware in the specified order, and only an output that comes out NaN is recomputed step by step. Single add and mul check for NaN on every call.

Part of this is new. The FloatLib version we pinned already proves hardware bridges for add, sub and sqrt, for finite inputs only. The winning file does not use them. It proves its own add and mul bridges from Lean's model, and its mul bridge excludes only NaN operands, so infinities are covered. FloatLib has no mul bridge at all.

Two champions, both 8.7× on the board

To see what the scores meant, we re-ran every accepted file against the shipped kernels on a dev server, on one pinned core with two seeds, on several input sets. One of them, which we call unseen inputs below, was built for this review and never used for scoring. The shipped kernels timed against themselves stay within 0.5% on every set.

Two champions came out of that with the same score and very different kernels.

Two champions, both 8.7× on the board

#174 · Last champion on the fixed benchmark, 21 Oct

8.7×board1.4×unseen

#323 · Final champion, 26 Oct

8.7×board11.4×unseen

• What the board recorded
• The same champion on unseen inputs

Data

champion	since	on the board	on unseen inputs
#1	14 Oct	1.2×	1.0×
#3	14 Oct	1.4×	1.1×
#4	14 Oct	1.5×	1.2×
#5	14 Oct	1.8×	1.4×
#8	14 Oct	2.0×	1.6×
#9	14 Oct	2.4×	2.0×
#12	14 Oct	2.6×	1.8×
#14	14 Oct	2.8×	1.9×
#16	14 Oct	3.3×	2.1×
#17	14 Oct	3.4×	2.2×
#19	14 Oct	3.6×	2.4×
#20	14 Oct	3.7×	2.4×
#22	15 Oct	4.1×	3.5×
#26	15 Oct	4.8×	3.5×
#37	15 Oct	5.1×	3.0×
#52	15 Oct	5.5×	2.5×
#64	16 Oct	5.7×	2.5×
#69	16 Oct	6.0×	2.5×
#74	16 Oct	6.3×	2.5×
#85	17 Oct	6.7×	2.6×
#87	17 Oct	7.0×	2.6×
#93	17 Oct	7.2×	2.2×
#147	20 Oct	7.5×	2.3×
#155	20 Oct	7.8×	2.3×
#165	20 Oct	8.3×	2.3×
#174	21 Oct	8.7×	1.4×
#265	22 Oct	2.2×	2.6×
#267	22 Oct	3.0×	3.5×
#268	22 Oct	3.9×	5.3×
#269	22 Oct	4.5×	6.8×
#271	22 Oct	4.9×	7.2×
#272	22 Oct	5.1×	7.0×
#274	22 Oct	6.4×	8.6×
#279	22 Oct	6.8×	9.4×
#284	23 Oct	7.6×	9.8×
#285	23 Oct	8.1×	10.2×
#309	24 Oct	8.4×	10.9×
#323	26 Oct	8.7×	11.4×

The board puts #174 (21 October) and #323 (26 October) side by side: 8.74× and 8.72× faster than the shipped kernels. On inputs neither of them was scored on, #174 is 1.4× and #323 is 11.4×. The difference between them is what the benchmark measured for the first eight days, and what changed when it stopped being fixed.

The first eight days rewarded learning the benchmark

The fixed benchmark never timed a NaN, an infinity, a subnormal, a second sum length or a second bmm shape. Entries learned exactly that.

On 14 October, the ranking by benchmark score and the ranking by speed on unseen inputs agreed almost perfectly, at a rank correlation of 0.97. A day later it was 0.61. By the end it was −0.16: a better score on the benchmark had become slightly worse than random at predicting speed on new inputs. The private suite, scored on the same files after the fact, never fell below 0.88.

Does the ranking predict speed on new inputs?

• The fixed public benchmark
• The private suite, drawn fresh every run

Data

day	files	fixed benchmark	private drawn suite
14 Oct	20	0.97	0.99
15 Oct	60	0.61	0.97
16 Oct	71	0.53	0.97
17 Oct	84	0.46	0.96
18 Oct	89	0.42	0.93
19 Oct	99	0.29	0.89
20 Oct	108	0.15	0.89
21 Oct	128	−0.05	0.91
22 Oct	150	−0.07	0.94
23 Oct	170	−0.14	0.95
24 Oct	179	−0.16	0.96
25 Oct	184	−0.17	0.96
26 Oct	201	−0.17	0.97
27 Oct	207	−0.16	0.97
28 Oct	208	−0.16	0.97

What tuning to one shape looks like

#174 is a resubmission of #172, and the code shows where its 8.7× came from. Its sum takes the hardware path only when the vector length is a multiple of four. Its bmm takes a fast table path only when the output width is between 49 and 52. The benchmark's 1,000 and 50×100×50 pass both checks every time.

A fast path that only opens on the benchmark's shape

sum, by lengthbmm, by shape

• #174, last champion on the fixed benchmark
• #323, final champion

Data

length	#174	#323
2	1.37×	9.3×
6	2.47×	15.9×
10	2.65×	18.7×
63	2.8×	25×
65	2.79×	25.2×
97	2.75×	24.6×
127	2.75×	24.1×
129	2.79×	24.4×
251	2.73×	23.4×
255	2.73×	23.4×
257	2.72×	23.4×
999	2.66×	22.7×
1000	23.8×	22.7×
1001	2.66×	22.8×
1021	2.67×	22.9×
4093	2.6×	22.5×

At n = 1,000, #174's sum is 24× faster than the shipped kernels. At every other length we tried it is 1.4 to 2.8×. Its bmm is about 300× faster on the benchmark's shape and its close neighbours, and slower than the shipped kernels everywhere else: 272× slower at 1×1×257.

None of this breaks a proof. #174 is exactly right on every input. It is only fast on the inputs it was shown.

A week of progress that was not

On unseen inputs, no champion after the morning of 15 October beat #22 and #26, at 3.5× and 3.4×. The best of the later ones reached 3.0×, while the board climbed from 4.8× to 8.7×.

We replayed the competition on our noise-free re-timings of the private suite, with the same 3% rule. In that replay, nothing after 15 October takes over until #238 on 21 October, the best file of the first eight days on unseen inputs at 4.4×. In the real competition #238 was timed against the shape-tuned #174, measured 1.107, and was rejected.

0.97 → −0.16

rank agreement between the benchmark and unseen inputs, 14 → 28 October

272×

how much slower than the shipped kernels #174's bmm is at shape 1×1×257

The private suite worked

From 22 October the full entry was scored on inputs drawn fresh for every run, and the board started telling the truth again.

• The ranking agreed with unseen inputs at 0.97 by the end.
• 11 of the 12 champions after the switch are faster on unseen inputs than on the suite they were scored on. The exception, #265, was the first entry timed on the new suite, against #174's collapsing bmm.
• None of them is slower than the shipped kernels on any input family. Five champions from the first eight days are: #93 by up to 2.4× on sparse mul, #147, #155 and #165 by 1.3× on sparse bmm, and #174 by up to 4× on bmm.

It is not a complete safety net. 43 of the 208 files are more than 5% slower than the shipped kernels on at least one family of unseen inputs, because the rules had no per-family do-no-harm check. The champions after the switch happened not to be among them.

How fast the final kernels are

Kernel by kernel, against the kernels we shipped

• #174 on the fixed benchmark
• #174 on unseen inputs
• #323 on unseen inputs

Data

	add	mul	sum	bmm
#174 on the fixed benchmark	3.2×	2.3×	31.3×	288.3×
#174 on unseen inputs	1.9×	1.9×	1.7×	0.5×
#323 on unseen inputs	5×	2.6×	23.9×	76.1×

On unseen inputs, #323 is 76× faster than the shipped kernels on bmm, 24× on sum, 5.0× on add and 2.6× on mul. Across 16 vector lengths from 2 to 4,093 and 11 matrix shapes from 1×1×257 to 128×8×128, it is 9 to 25× faster on sum and 21 to 167× on bmm. Its weakest input family anywhere, mul on sparse inputs, is still 1.4× faster than what we shipped.

How far that is from plain hardware floats

Closer than we expected.

Time per step, from proved to plain hardware floats

• Shipped proved kernels
• #323, proved
• Plain C float loop, nothing proved

Data

	add	mul	sum	bmm
Shipped proved kernels	35 ns	26 ns	31 ns	57 ns
#323, proved	9 ns	8.6 ns	1.5 ns	2 ns
Plain C float loop, nothing proved	0.59 ns	0.57 ns	0.8 ns	0.64 ns

Proved-exact sum and bmm went from 40 to 90 times slower than plain floats to about 2 to 3 times slower. Single add and mul are still about 15 times slower, because every call pays for the NaN check, the conversions and the call itself.

1.9×

#323's proved sum against a plain C loop; the shipped kernels were 39× behind

3.1×

#323's proved bmm against plain C; the shipped kernels were 89× behind

Timing noise decided many takeovers

The validator's own admission rule, replayed on the published timing rounds, reproduces all 38 takeovers exactly. That let us look inside them.

Sixteen entries were byte-identical to the champion they were timed against. Their measured ratios ranged from 0.934 to 1.044. Three landed under the 0.970 bar, and one of them passed the statistical test and became champion, by beating an exact copy of itself.

Sixteen files timed against an exact copy of themselves

• Under the bar, passed the test, became champion
• Under the bar, stopped by the statistical test
• Above the bar

Data

entry	ratio	outcome
#165	0.934	under the bar, passed the test, became champion
#177	0.953	under the bar, stopped by the statistical test
#161	0.960	under the bar, stopped by the statistical test
#176	0.970	above the bar
#157	0.973	above the bar
#163	0.991	above the bar
#156	0.992	above the bar
#158	0.996	above the bar
#166	1.000	above the bar
#148	1.000	above the bar
#175	1.008	above the bar
#178	1.012	above the bar
#162	1.018	above the bar
#159	1.022	above the bar
#164	1.028	above the bar
#160	1.044	above the bar

The weak point is the combination of the two checks. The 3% bar applied to a headline built from each side's fastest round, and one lucky round moves that by several percent. The bootstrap then only checked that the median round was faster at all, not that it was 3% faster. Twelve of the 38 takeovers were under 3% faster by their median round, and six were under 1%. Ten in a row, from 16 to 21 October, were under 3%.

How much faster each new champion really was

• 3% or more by the median round
• Under 3%

Data

champion	date	median gain
#1	14 Oct	14.9%
#3	14 Oct	15.7%
#4	14 Oct	7.6%
#5	14 Oct	17.4%
#8	14 Oct	9.4%
#9	14 Oct	12.9%
#12	14 Oct	9.6%
#14	14 Oct	9.1%
#16	14 Oct	12.2%
#17	14 Oct	5.5%
#19	14 Oct	6.0%
#20	14 Oct	4.0%
#22	15 Oct	4.8%
#26	15 Oct	17.7%
#37	15 Oct	4.2%
#52	15 Oct	3.0%
#64	16 Oct	0.8%
#69	16 Oct	0.1%
#74	16 Oct	0.9%
#85	17 Oct	1.9%
#87	17 Oct	1.1%
#93	17 Oct	1.2%
#147	20 Oct	1.0%
#155	20 Oct	0.1%
#165	20 Oct	0.0%
#174	21 Oct	0.6%
#265	22 Oct	96.8%
#267	22 Oct	24.4%
#268	22 Oct	24.7%
#269	22 Oct	14.8%
#271	22 Oct	7.3%
#272	22 Oct	4.1%
#274	22 Oct	20.4%
#279	22 Oct	6.4%
#284	23 Oct	9.4%
#285	23 Oct	2.6%
#309	24 Oct	8.8%
#323	26 Oct	1.2%

Resubmitting was a strategy

118 of the 326 accepted entries were byte-identical resubmissions, and four of them took over. One, #165, was a copy of the reigning champion submitted by a different operator, and it won the title from the original. From 22 October, a file identical up to comments and whitespace was refused before timing.

The final takeover got around that. #323 differs from an earlier entry, #320, only in the length of a literal array inside a constant that no kernel reads. #320 measured 0.978 and missed the bar; #323 measured 0.969 and became the final champion.

To be fair to #323, on unseen inputs it is slightly faster than the champion it replaced, 11.4× against 10.9×, so the final result stands. But the last step was won on the timing, not on the code.

12 of 38

takeovers under 3% faster by their median round; six under 1%

4

takeovers by a byte-identical resubmission, one of them a rival's copy of the champion

A small field and a full file

26 operators stood behind 339 hotkeys, and three of them made 273 of the 339 submissions. One operator produced 21 of the 38 takeovers, including all three that held the paid places at the end.

The size cap shaped the code more than any reviewer would have. 114 of the 208 files sit within 6 kB of the 256 kB limit. #323 is 255,734 bytes: 425 lemmas, about 81% proof by volume, and 224 single-character notations such as ♠ and ⓑ, declared to squeeze it under the cap. It is correct, and it is very hard to read.

What this is good for

• Verified machine learning in Lean. TorchLean already lets you run a network on FloatLib's proved binary32, which is slow, or on Lean's native Float32, which is fast and has nothing proved about it. This competition shows a third option: hardware speed for tensor loops with the theorem attached. That is what verified inference, certificate checking and reproducible reference runs inside Lean need.
• FloatLib itself. A mul bridge, and add and mul bridges that cover infinities, are missing from FloatLib today, and they are exactly what Lean's documentation asks float libraries to provide.
• Not a BLAS replacement. The specification fixes the order of additions and forbids fused multiply-add, which rules out the SIMD and blocking that make native matrix multiply fast.
• Not a proof about your CPU. The theorems are about Lean's model of Float32. Running them correctly assumes the compiled float instructions follow IEEE-754 binary32: round to nearest, no flush-to-zero, no excess precision. Every Lean program that uses Float32 already makes the same assumption.
• Not usable as is. The ideas carry over. The files would need a readable rewrite before anyone could maintain them.

What came next

FloatLib was never meant to be the end goal. It was the first stage of a bigger competition, run from the same repository, and its first takeover came on 28 October, the same evening FloatLib's board was frozen.

Running now

TorchLean: the same deal, for whole networks

FloatLib was the first stage. Its successor times proved inference kernels on five model families, on an x86 and an ARM machine. Its first takeover came on the evening FloatLib's board was frozen, and on every board it was 8 to 22 times faster than the shipped reference.

12

kernels in one Lean file, from dot products to layer norm

6

boards: MLP, ResNet, MobileNet, normalized MLP, Mixer and overall

107

takeovers across the boards in the first six days

Carried over from FloatLib

• FloatLib's arithmetic as the specification: exact dot products, addition, fused multiply-add, maximum and division
• The same proof gate, paired timing rounds and statistical takeover rule
• The winning idea, one precision up: binary32 inputs decoded into 64-bit hardware floats, where a product of two of them is exact

The TorchLean competition

What we changed because of FloatLib

Most of the lessons above are already live in TorchLean.

• Fresh inputs every evaluation. Every evaluation draws a new seed: typical, large-scale and boundary workloads, odd sizes, wide-exponent and sparse values. There are no fixed shapes left to learn.
• A do-no-harm rule. An entry cannot take over if any workload, input type or CPU is more than 10% slower than the champion's.
• Medians, not lucky rounds. The score is the median over rounds, not the fastest round. The statistical test still only asks for some gain, and we would like it to ask for the full 3%.
• Copies refused before they are timed. That still means the same file up to comments and whitespace. A copy with a changed constant would get through, and catching those is next.
• Two CPU architectures, so tuning to one machine buys less.
• Published sources. Once a champion no longer holds any board, its file is published.
• A bigger size cap, soon. Support for 1 MB files has landed in the code but is not live yet. TorchLean's champions are already pressed against 256 kB, just like FloatLib's.

The proofs made every one of these 208 files exactly right on every input. The benchmark decided which of them were fast, and for the first eight days it mostly measured itself.