Optimisation · Float kernels
Faster float kernels, proved exact.
Miners submit one Lean file with four binary32 kernels: FloatLib's add and mul, and TorchLean's sum and batched matrix multiply built from them. Each one is proved equal to its specification, bit for bit. An entry 3% faster than the champion becomes the new champion, and the last three champions share the payout 60/30/10.
5Gq3gF…Q35pqu#14
1st60%5CQLTf…KYXEXx#12
2nd30%5FPSjK…eBwRsS#9
3rd10%
- Of validator weight
- 20%
- To take over
- 0.970×
- Challengers
- 1
- In the queue
- 0
- 25CyWuL…bLSbp9#80.926×Takes over14 Oct 2026, 15:48 UTC
- 35FHSpS…nJcS17#70.991×14 Oct 2026, 15:39 UTC
- 45Ck7hz…XjMEJo#61.629×14 Oct 2026, 15:05 UTC
- Faster
- Within noise
- Slower
- Takes over
- Champion, 1.000×
Former champion
5GEJkr…axx4sW#5
Time against the champion before it
0.825×
17% faster than the one beforeFrom 14 Oct 2026, 15:03 UTC to 14 Oct 2026, 15:52 UTC
Nanoseconds per step
- add66.3
- mul67.4
- sum34.2
- bmm75.7
Click a challenger to see where its time goes.
Where the time goes
Nanoseconds per step, each kernel summed over its three input types. Click an entry to compare it.
Champion before it295.0
#5 5GEJkr…axx4sW243.5 · 0.825×
By input type
add27% of the time79.0 to 66.3 ns0.839×
- Cancellation0.803×
- Near one0.860×
- Wide gap0.844×
mul22% of the time65.2 to 67.4 ns1.033×
- Tiny1.024×
- Spread1.001×
- Near one1.081×
sum16% of the time46.2 to 34.2 ns0.740×
- ReLU-like0.660×
- Wide range0.770×
- Dense0.750×
bmm35% of the time104.7 to 75.7 ns0.723×
- ReLU-like0.675×
- Wide range0.751×
- Dense0.729×
How to enter
One file, one hotkey, one try per registration
An entry is a single Kernel.lean sent from the miner client in the competition repository. Run the same gate on your machine first, against the shipped reference, before you spend a registration.
1Register a hotkey
Register on Subnet 66. Each registration allows one submission, and every stored entry spends it, whatever the outcome.
2Set up the kit
On Linux x86_64, clone the competition repository and run ./setup.sh. It installs Lean, FloatLib, Mathlib, the sandbox and the miner client, and can be rerun after an interruption.
3Measure, then prove
Start from the shipped reference. gate.py --bench times an entry before its proofs are done; the full gate checks policy, proofs and axioms, then times it.
4Submit
Send Kernel.lean, at most 256,000 bytes, signed with your hotkey. The same file twice from one hotkey is refused.
Miner client
./setup.sh
source .venv/bin/activate
cp -r kernels/full/incumbent my-entry
python gate.py --slot full --bench my-entry
python gate.py --slot full my-entry
python miner/submit.py submit my-entry --hotkey <file>
python miner/submit.py status <id>How it is scored
The rules
- 01The competition sets 20% of the validator's weights. The rest goes to the treasury.
- 02The last three champions share it: 60% to the current one, 30% and 10% to the two before it. A place nobody holds yet goes to the treasury, and so does everything while the shipped champion holds.
- 03Every entry is timed against the current champion: its total time over the champion's across twelve input types, three per kernel. Lower is faster, and a faster add or mul counts again inside sum and bmm.
- 04An entry takes over at 0.970× or lower, at least 3% faster, and only if its gain holds at the 5th percentile of a bootstrap over its 25 paired rounds (2000 draws). A copy of the champion never takes over.
- 05After a takeover the board starts again: every later entry is timed against the new champion.
- 06Every output must match the champion's bit for bit, including NaN, infinities and subnormals. One mismatch rejects the entry.
- 07Every stored entry spends its registration, whatever the verdict, including a validator error. Only a refusal before the entry is stored is free.
- 08If the champion cannot build or finish its own bench, its board pauses. Waiting entries keep their place, cost nothing and are retried. Only an operator can demote a champion.