Proved tensor kernels, raced on six boards.

One Lean file supplies the twelve kernels behind five neural networks, with a proof that each one equals the pinned specification. The same file is timed on six boards, one per model family and one overall. Beat a board's champion by enough to count and the board is yours.

Where the payout goesEach board's part of the competition's payout goes to its current champion. A board nobody has taken pays the treasury.

Overall50%
Champion5HKaTt…oF77vZ
MLP10%
Champion5HKaTt…oF77vZ
ResNet10%
Champion5HKaTt…oF77vZ
MobileNet10%
Champion5HKaTt…oF77vZ
Normalized MLP10%
Champion5HKaTt…oF77vZ
Mixer10%
Champion5ES53t…ERXCzz

Boards: 6
Takeovers: 12
Entries: 19
In the queue: 14
To take over: 0.970×

The boards

Six boards, one file

Every entry is timed on all six. A board is held by its last champion until an entry beats it, or by the shipped reference until the first one does.

Board

MLP

Challengers, timed against #5

EntryTime

Faster
Within noise
Slower
Takes over
Champion, 1.000×

Current champion

5HKaTt…oF77vZ#5

Time against the one before

0.966×

3% faster than the one beforeSince 28 Oct 2026, 19:59 UTC

10.0% of the competition's payout

Champions on this board

5HKaTt…oF77vZ#50.966×CurrentFrom 28 Oct 2026, 19:59 UTC
5Gb23s…iaWuoX#20.129×28 Oct 2026, 17:57 UTC to 28 Oct 2026, 19:59 UTCKernel.lean

Standings

Who holds what

Every paid place across the six boards, and the part of the competition's payout it adds up to.

Hotkey	Overall	MLP	ResNet	MobileNet	Normalized MLP	Mixer	Of the payout
5HKaTt…oF77vZ	Champion	Champion	Champion	Champion	Champion	-	90.0%
5ES53t…ERXCzz	-	-	-	-	-	Champion	10.0%

Entries

Every entry, newest first

19 entries

Qualified
Timed
Guard failed
Being timed
Not planned

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. Build and time it on your own machine against the shipped reference before you spend a registration.

1Register a hotkey
Register on Subnet 66 after the competition opens. Each registration allows one submission, whatever its outcome.
2Set up the kit
Clone the competition repository and run ./setup.sh --dev. It installs the pinned Lean packages, the sandbox and the miner client.
3Start from the reference
Copy kernels/exact/incumbent, make it faster, and keep the proof that every kernel equals the specification.
4Submit and follow it
Send Kernel.lean, at most 256,000 bytes, signed with your hotkey. The client prints an ID; its page here shows the proof, every board and every run.

Miner client

./setup.sh --dev
cp -r kernels/exact/incumbent my-entry
.venv/bin/python miner/submit.py submit my-entry --hotkey <file>
.venv/bin/python miner/submit.py status <id>
.venv/bin/python miner/submit.py report <id>
.venv/bin/python miner/submit.py boards
.venv/bin/python miner/submit.py leaderboard --board mlp

Competition repository Miner manual

How it is scored

The rules

01An entry is one Kernel.lean with all twelve kernels and a Lean proof that each equals the pinned specification. The proof is checked once, then the file is timed.
02The same file runs on six boards: one per model family and an overall board that mixes all five. Each board has its own champion and its own challengers.
03The competition's payout is split between the boards: Overall 50%, MLP 10%, ResNet 10%, MobileNet 10%, Normalized MLP 10%, Mixer 10%.
04An entry takes a board over at 0.970× or lower, at least 3% faster than its champion, timed on every benchmark machine on the same inputs.
05The gain has to hold up: a bootstrap over the paired rounds must keep it above zero, or the entry stays a challenger.
06No input group may be slower than 1.100× of the champion's time. One that is fails the guard, however fast the rest.
07Each board pays its current champion only. A board nobody has taken pays the treasury.
08Only a registration made after the competition opened can enter, once per registration.
09The same Kernel.lean from one hotkey is refused, even after re-registering, and a copy of an accepted entry is rejected before it is timed.
10A champion's Kernel.lean stays private while it holds any board. Once it holds none, anyone can download it from its entry page.
11If a board's champion cannot build or its outputs disagree, the board pauses. Waiting entries keep their place and are retried.