Proved tensor kernels, raced on seven boards.

One Lean file supplies the nineteen kernels behind six families of neural networks, recurrent ones included, with a proof that each one equals the pinned specification. The same file is timed on generated workloads and on trained models with real data, on seven 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%
Champion5FpjK6…3EMSW7
MLP8%
Champion5FKxeP…U35urR
ResNet8%
Champion5FpjK6…3EMSW7
MobileNet8%
Champion5CJy5S…NeMrJo
Normalized MLP8%
Champion5E1j4R…sm9ANG
Mixer8%
Champion5En5Vp…3thKHn
Recurrent8%
Champion5FCgYk…JApLBK

Boards: 7
Takeovers: 64
Entries: 25+
In the queue: 0
To take over: 0.970×

The boards

Seven boards, one file

Every entry is timed on all seven. 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 #36

EntryTime

Faster
Within noise
Slower
Takes over
Champion, 1.000×

Current champion

5FKxeP…U35urR#36

Time against the one before

0.673×

33% faster than the one beforeSince 11 Nov 2026, 07:48 UTC

8.3% of the competition's payout

Champions on this board

5FKxeP…U35urR#360.673×CurrentFrom 11 Nov 2026, 07:48 UTC
5Gs2Eh…TDn5RP#10.021×10 Nov 2026, 17:55 UTC to 11 Nov 2026, 07:48 UTCKernel.lean

Results

Every takeover, as measured

Each takeover is timed against the champion it replaced, on the benchmark of the day. A dot is one takeover; the lower it sits, the larger the gain. Lower is faster.

Board	Champion	Takeovers	Last takeover	When
Overall	5FpjK6…3EMSW7#132	14	0.909×	3 hours ago
MLP	5FKxeP…U35urR#36	2	0.673×	2 days ago
ResNet	5FpjK6…3EMSW7#132	13	0.927×	3 hours ago
MobileNet	5CJy5S…NeMrJo#61	9	0.903×	2 days ago
Normalized MLP	5E1j4R…sm9ANG#47	3	0.891×	2 days ago
Mixer	5En5Vp…3thKHn#103	5	0.875×	19 hours ago
Recurrent	5FCgYk…JApLBK#116	18	0.868×	14 hours ago

Each takeover's time against the champion it replaced

Takeover
First on a changed benchmark
Below 0.500×
Takeover bar

Standings

Who holds what

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

Hotkey	Overall	MLP	ResNet	MobileNet	Normalized MLP	Mixer	Recurrent	Of the payout
5FpjK6…3EMSW7	Champion	-	Champion	-	-	-	-	58.3%
5FKxeP…U35urR	-	Champion	-	-	-	-	-	8.3%
5CJy5S…NeMrJo	-	-	-	Champion	-	-	-	8.3%
5E1j4R…sm9ANG	-	-	-	-	Champion	-	-	8.3%
5En5Vp…3thKHn	-	-	-	-	-	Champion	-	8.3%
5FCgYk…JApLBK	-	-	-	-	-	-	Champion	8.3%

Entries

Every entry, newest first

Newest first

Back to the newest Older entries

Qualified
Timed
Too slow
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. It installs the pinned Lean packages, the sandbox and the miner client; ./setup.sh --check lists anything missing.
3Start from the reference
Copy kernels/exact/incumbent, make any of the nineteen kernels faster, and keep the proof that every kernel equals the specification.
4Submit and follow it
Send Kernel.lean, at most 1 MiB, signed with your hotkey. The client prints an ID; its page here shows the proof, every board and every run.

Miner client

./setup.sh
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 recurrent

Competition repository Miner manual

How it is scored

The rules

01An entry is one Kernel.lean with all nineteen kernels and a Lean proof that each equals the pinned specification, bit for bit. The proof is checked once, then the file is timed.
02The same file runs on seven boards: MLP, ResNet, MobileNet, normalized MLP, Mixer, Recurrent and an overall board that mixes all six. Each board has its own champion and its own challengers.
03Each board times generated workloads and, where the competition enables it, trained models on real data. Both suites count towards the time, by fixed published weights.
04The competition's payout is split between the boards: Overall 50%, MLP 8%, ResNet 8%, MobileNet 8%, Normalized MLP 8%, Mixer 8%, Recurrent 8%.
05An 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.
06The gain has to hold up: a bootstrap over the paired rounds must keep it above zero, or the entry stays a challenger.
07No input group may be slower than 1.100× of the champion's time. One that is fails the guard, however fast the rest.
08The native build may take at most 960 s and one timed run at most 3600 s, and the paired runs on each board share a fixed time budget with the champion. An entry that runs out of time is decided Too slow and gets no score.
09Each board pays its current champion only. A board nobody has taken pays the treasury.
10Every run also times the shipped baseline kernels. That comparison is shown for reference only; a board is decided against its champion.
11Only a registration made after the competition opened can enter, once per registration.
12The 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.
13A champion's Kernel.lean stays private while it holds any board. Once it holds none, anyone can download it from its entry page.
14If a board's champion cannot build or its outputs disagree, the board pauses. Waiting entries keep their place and are retried.