150 takeovers, six boards, one theorem: what the TorchLean competition found

From 28 October to 10 November 2026, miners on the subnet competed to make neural-network inference in Lean faster without giving up a single bit of correctness. A submission was one Lean file with 12 binary32 kernels, and one machine-checked proof that they return exactly what the pinned specification returns, for every possible input. The validator checked the proof, timed the file inside whole models against the reigning champion, and crowned it if it was at least 3% faster.

226

submissions from 19 operators (coldkeys)

221

passed the proof gate; of the 5 refused, 4 were copies and 1 had a statement that did not typecheck

1,346

evaluations, each one entry timed on one board

150

takeovers across six boards, by 91 different files

The competition has ended and Tensor kernels has taken its place. This is what TorchLean produced, what went right, what went wrong, and what we changed.

What a submission had to prove

The 12 kernels are the ones CPU inference is made of: sum, dot, linear and gemm; conv2d, depthwise, avgpool and maxpool; addRelu, scaleShift, rmsnorm and layernorm. The arithmetic is FloatLib's: a dot product computed exactly and rounded once, IEEE addition, fused multiply-add, maximum and division. The proof covers every input, with NaNs, infinities and subnormals included, and every shape.

Each entry was timed on six boards: MLP, ResNet, MobileNet, normalized MLP, Mixer, and an overall board that runs all five. It ran on two machines, one x86 and one ARM, which counted equally. Every evaluation drew fresh shapes and values: typical sizes, large sizes and awkward boundary sizes, filled with ordinary, wide-exponent and sparse numbers.

To take a board, an entry needed three things:

• a median score at least 3% faster than the champion's;
• a bootstrap over the timing rounds that agreed;
• no workload, input type or CPU more than 10% slower than the champion's.

The overall board carried half of the competition's share and each model board a tenth, winner takes all.

How fast the final kernels are

The board only ever shows an entry against the champion it faced, and the benchmark changed several times, so multiplying those ratios together does not give an honest total. Every report also records how many inferences were fitted into each timed cell. Dividing a cell's time by that count gives the champion's absolute time per inference, on the same two machines from the first day to the last.

Time per inference, shipped kernels against the final champion

• Kernels we shipped
• Final champion

Data

board	shipped	final champion	x86	ARM
Overall	16.1 ms	#219: 117 µs	137×	126×
MLP	6.9 ms	#220: 54 µs	129×	91×
ResNet	18.2 ms	#175: 180 µs	101×	94×
MobileNet	21.9 ms	#221: 144 µs	152×	141×
Normalized MLP	11.5 ms	#218: 56 µs	206×	273×
Mixer	21.5 ms	#222: 78 µs	276×	271×

On x86, the final overall champion takes 117 µs for an inference that took the shipped kernels 16.1 ms: about 137 times faster. The five model boards end between 101 times (ResNet) and 276 times (Mixer). ARM tells the same story, from 91 to 273 times.

Most of the gain came on the first day. One entry took all six boards within 13 minutes of each other, 8 to 22 times faster than the kernels we shipped. Leaving the caching period aside, the overall champion's time then fell from about 1 ms to 117 µs over the next twelve days.

117 µs

per inference for the final overall champion on x86; the shipped kernels took 16.1 ms

101 to 276×

final champions against the shipped kernels on the five model boards, on x86

Where the speed came from

FloatLib's winners ran their loops in the CPU's 32-bit floats and checked the result for NaN. That does not carry over directly. TorchLean's dot product is exact and rounds once at the end, and a 32-bit loop rounds at every step.

The champions went one precision up. They decode each 32-bit float into the CPU's 64-bit floats, where the product of two 32-bit floats is exact, and prove the connection to the specification through Lean's model of hardware floats. The first champion to do this took the MLP board on the evening of 30 October. Of the 85 champion files published so far, 55 work this way.

The rest is plumbing, done carefully. All 85 files index with machine words instead of unbounded naturals, and 65 keep their data in packed float and byte arrays instead of generic ones.

Two days of caching

On 2 November the top of every board changed character.

The benchmark at the time gave every timed repetition of a cell the same input, and kept the fastest of three samples. An entry that remembered its last answer could skip all the work after the first call. The first one to try recovered the generator's random seed from the input and kept a memo table of finished results. Later ones kept results in a global store that survives between calls.

Every cached value came with a proof that it equals the specification, so no output was ever wrong. The proofs did their job. The stopwatch did not.

What each champion took per inference

OverallMLPResNetMobileNetNormalized MLPMixer

• Champion
• Champion that cached its outputs

Data

champion	since	time per inference	on fresh inputs
#2	28 Oct	1.0 ms
#5	28 Oct	837 µs
#8	28 Oct	845 µs
#54	30 Oct	741 µs
#59	30 Oct	549 µs
#91	31 Oct	431 µs
#99	1 Nov	298 µs
#112	1 Nov	245 µs
#126	2 Nov	212 µs
#136	2 Nov	188 µs
#140	3 Nov	80 µs (repeated inputs)
#148	3 Nov	11 µs (repeated inputs)
#149	3 Nov	8.9 µs (repeated inputs)
#150	3 Nov	6.9 µs (repeated inputs)
#152	3 Nov	5.5 µs (repeated inputs)
#163	4 Nov	4.6 µs (repeated inputs)	2.1 ms
#165	4 Nov	171 µs
#166	5 Nov	167 µs
#192	5 Nov	134 µs
#202	6 Nov	140 µs
#213	9 Nov	132 µs
#219	10 Nov	117 µs

On the board, these entries ran an inference in 3 to 6 µs, about 40 to 50 times faster than the champions before them. Seventeen such files took a board 39 times between 2 and 4 November, and held each board for 39 to 55 hours.

On 4 November we changed the benchmark:

• every inference gets its own fresh input;
• a timing is the median of three samples, not the best of three;
• each sample runs in a fresh process.

The caching champions were still on the boards, so the next entries were timed against them under the new rules. That re-timed the champions themselves.

The caching champions, before and after fresh inputs

• Last champion before caching
• Caching champion, as the benchmark recorded it
• The same file on fresh inputs

Data

board	before caching	caching champion, recorded	same file, fresh inputs
Overall	#136: 188 µs	#163: 4.6 µs	2.1 ms
MLP	#110: 187 µs	#154: 4.9 µs	215 µs
ResNet	#136: 181 µs	#163: 4.8 µs	1.9 ms
MobileNet	#136: 298 µs	#159: 5.9 µs	575 µs
Normalized MLP	#130: 123 µs	#154: 3.1 µs	4.6 ms
Mixer	#130: 158 µs	#159: 3.6 µs	25.2 ms

On the overall board, #163 went from 4.6 µs to 2.1 ms, eleven times slower than the last champion before caching. On Mixer, #159 took 25 ms, slower than the kernels we shipped. The next entries took the boards back at recorded ratios as low as 0.009. Those ratios measure how far the caches fell, not how good the newcomers were: they ran at 140 to 270 µs, about where the champions had been before caching started.

Not all caching went away, and it was not meant to. Several later champions still keep a store between calls, and use it for values worked out from the weights, such as decoded weight arrays. With a new input for every inference that can only save setup work within a sample, which the benchmark allows. Caching outputs no longer pays.

39

takeovers by 17 files that cached their outputs, 2 to 4 November

4.6 µs → 2.1 ms

the last caching champion on the overall board, before and after fresh inputs

Half the evaluations ran out of time

685 of the 1,346 evaluations ended in a timeout, most of them a single benchmark run over its five-minute limit.

What happened to each evaluation, by board

• Took the board
• Not fast enough, or overtaken while waiting
• Stopped by the regression guard
• Ran out of time

Data

board	Took the board	Not fast enough, or overtaken while waiting	Stopped by the regression guard	Ran out of time	evaluations
Overall	22	6	31	166	225
MLP	22	15	112	76	225
ResNet	29	21	68	105	223
MobileNet	31	32	59	101	223
Normalized MLP	23	11	72	119	225
Mixer	23	11	73	118	225

The overall board was hit hardest. It times 180 cells in a run, five times as many as a model board, under the same limit. It gave a score to only 55 of 225 entries, and it carried half the reward. The entries it timed out were not hopeless ones: on the model boards where the same entries did get a score, their median was 3% slower than the champion's. 23 submissions timed out on every board and never got a score at all.

The do-no-harm rule was too sharp

The 10% regression guard was a lesson from FloatLib, where a champion could be much slower than the one before it on inputs the benchmark did not weigh. In TorchLean it checked every cell: each workload, each input type, each CPU.

It stopped 47 submissions that were at least 3% faster overall, with the bootstrap agreeing. A model board has 72 cells per evaluation, and each cell is 50 ms of timing. In 22 of those blocked evaluations three cells or fewer were over the limit, and in 9 it was a single cell. The cells that tripped were spread evenly over workload types and both CPUs. A real regression would cluster somewhere. This is what noise looks like.

47

submissions fast enough to take a board and stopped by the guard

9

of those evaluations failed on exactly one cell out of 72

Two CPUs mostly agreed

641 evaluations have a score on both machines. Across the whole range the two agree closely. Near the bar they agree less: in 84 evaluations one CPU said faster and the other said slower. Two champions were slower than their predecessor on x86 and took over on the strength of ARM.

Scoring on two architectures is still worth it, because it makes tuning to one machine less attractive. It also means a close call can be decided by which machine was having the quieter minute.

A small field and a full file

Two operators held every board at the end: one held the overall and ResNet boards, the other the remaining four. Eleven of the 19 operators took a board at least once. Nine had also competed in FloatLib, and they made 78 of the 150 takeovers. FloatLib's most successful operator made the first takeover on every board, and the first ones again after the caching fix.

The size cap shaped the code again. Of the 80 published files from before the cap was raised, 58 sit within 8 kB of the 256 kB limit, written with one-character Unicode names to fit. Once larger files were accepted, around 5 November, champions grew to between 400 and 600 kB. They are correct, and they are very hard to read.

What this is good for

• Verified inference in Lean. Exact, proved binary32 inference for five model families now runs in tens to hundreds of microseconds, not tens of milliseconds. That is what certificate checking, reproducible reference runs and verified machine learning inside Lean need.
• Not a library yet. The files are compressed to fit the cap and would need a readable rewrite before anyone could maintain them. Tensor kernels starts from our original kernels, not from these champions.
• Not a comparison with unproved code. We did not time these kernels against plain floats or an ML framework, so this post says nothing about that gap.
• Not a proof about your CPU. The theorems are about Lean's model of floats. Running them correctly assumes the hardware follows IEEE-754, the same assumption every Lean program that uses floats already makes.

What came next

Running now

Tensor kernels: more kernels, real models

Tensor kernels replaced TorchLean on 10 November, the afternoon TorchLean's boards closed. It asks for the same kind of file and the same kind of proof, on a wider set of kernels and a benchmark built on what TorchLean taught us.

19

kernels in one Lean file, with recurrent networks added to the five families

7

boards: one per model family and one overall, each with its own time limits

2

kinds of workload: generated ones, and trained models running on real data

Carried over from TorchLean

• The same deal: one file, one proof that every kernel equals the pinned specification, timed against the champion
• TorchLean's last benchmark: a fresh input for every inference, the median of three samples, a fresh process for each
• Our original kernels as the starting point on every board, and as a fixed yardstick inside every evaluation

The Tensor kernels competition

What we changed because of TorchLean

• Fresh inputs for every inference, from the first day. Caching outputs does not pay on the new boards.
• Time limits per board, so a large board cannot time out most of its entries.
• The regression guard is recorded, not enforced, until we have a version that tells a regression from noise.
• A fixed yardstick in every evaluation. The original kernels are timed alongside each entry, so progress from the starting point is measured directly and not worked out afterwards, as it had to be here.
• Trained models next to generated ones, so speed on real inputs is visible.
• Still to do: a written rule on state between calls. Reusing setup work is fine and reusing outputs is not. That should be in the rules, not only in the benchmark.

The proofs kept every one of 221 files exactly right on every input. For two days the benchmark measured memory instead of speed, and we fixed it. The kernels that came out run whole-model inference two orders of magnitude faster than where we started.