Conjectures.io

Optimisation · Tensor kernels

Open

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

ResNet

Challengers, timed against #132
  • Faster
  • Within noise
  • Slower
  • Takes over
  • Champion, 1.000×

Current champion

5FpjK6…3EMSW7#132

Time against the one before

0.927×

7% faster than the one beforeSince 13 Nov 2026, 03:31 UTC

8.3% of the competition's payout

Champions on this board

  1. 5FpjK6…3EMSW7#1320.927×CurrentFrom 13 Nov 2026, 03:31 UTC
  2. 5E7RoH…v4pqyy#1080.961×12 Nov 2026, 14:30 UTC to 13 Nov 2026, 03:31 UTCKernel.lean
  3. 5ETigs…PwyKzz#590.942×11 Nov 2026, 16:50 UTC to 12 Nov 2026, 14:30 UTCKernel.lean
  4. 5FpXYh…nDBBxg#410.925×11 Nov 2026, 09:56 UTC to 11 Nov 2026, 16:50 UTCKernel.lean
  5. 5Cop2t…b4axQb#320.804×11 Nov 2026, 05:02 UTC to 11 Nov 2026, 09:56 UTCKernel.lean
  6. 5FFLei…5Nouyw#250.894×11 Nov 2026, 02:04 UTC to 11 Nov 2026, 05:02 UTCKernel.lean
  7. 5FNxAE…drQNfZ#240.951×11 Nov 2026, 01:41 UTC to 11 Nov 2026, 02:04 UTCKernel.lean
  8. 5CG78Z…rHFbrv#200.683×11 Nov 2026, 00:45 UTC to 11 Nov 2026, 01:41 UTCKernel.lean
  9. 5Gs6J9…LVfdCn#120.139×10 Nov 2026, 21:18 UTC to 11 Nov 2026, 00:45 UTCKernel.lean
  10. 5DcV46…wJGDCh#70.490×10 Nov 2026, 20:09 UTC to 10 Nov 2026, 21:18 UTCKernel.lean
  11. 5CZwEA…XBvDSn#60.566×10 Nov 2026, 19:19 UTC to 10 Nov 2026, 20:09 UTCKernel.lean
  12. 5ELubE…xWae9X#30.524×10 Nov 2026, 18:26 UTC to 10 Nov 2026, 19:19 UTCKernel.lean
  13. 5Gs2Eh…TDn5RP#10.967×10 Nov 2026, 17:56 UTC to 10 Nov 2026, 18:26 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.

BoardChampionTakeoversLast takeoverWhen
Overall5FpjK6…3EMSW7#132140.909×3 hours ago
MLP5FKxeP…U35urR#3620.673×2 days ago
ResNet5FpjK6…3EMSW7#132130.927×3 hours ago
MobileNet5CJy5S…NeMrJo#6190.903×2 days ago
Normalized MLP5E1j4R…sm9ANG#4730.891×2 days ago
Mixer5En5Vp…3thKHn#10350.875×19 hours ago
Recurrent5FCgYk…JApLBK#116180.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.

HotkeyOverallMLPResNetMobileNetNormalized MLPMixerRecurrentOf the payout
5FpjK6…3EMSW7Champion-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------Champion8.3%

Entries

Every entry, newest first

Newest first

  1. #585Fe1gv…D2daGyCompleted2 days ago
  2. #575CPzQE…uNdSCfCompleted2 days ago
  3. #565DvPVr…i31rgxCompleted2 days ago
  4. #555D25MY…17jHLCCompleted2 days ago
  5. #545D325a…Wo3M5SCompleted2 days ago
  6. #535H1VMC…vmMhXtCompleted2 days ago
  7. #525Cz1sJ…FSuchuCompleted2 days ago
  8. #515E52Qb…3vBqHnCompleted2 days ago
  9. #505DCPR5…JHku8LCompleted2 days ago
  10. #495ECB4u…Lznkx5Completed2 days ago
  11. #485FFZdM…hknaNwCompleted2 days ago
  12. #475E1j4R…sm9ANGCompleted2 days ago
  13. #465DXtQN…YExS8WCompleted2 days ago
  14. #455D4bX8…k9Ny8tCompleted2 days ago
  15. #445GKWhU…hFkiT1Completed2 days ago
  16. #435DRkTb…vU1wUbCompleted2 days ago
  17. #425GmaYL…t43iyNCompleted2 days ago
  18. #415FpXYh…nDBBxgCompleted2 days ago
  19. #405Fy7uZ…zp7E5qCompleted2 days ago
  20. #395CtkDA…537vL3Completed2 days ago
  21. #385EJ6JP…4Pg4SdCompleted2 days ago
  22. #375Ge84p…ZPcwXACompleted2 days ago
  23. #365FKxeP…U35urRCompleted2 days ago
  24. #355CyHJK…zFgsHQCompleted2 days ago
  25. #345F3yDg…RTpK4CCompleted2 days ago
Back to the newestOlder 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.

  1. 1Register a hotkey

    Register on Subnet 66 after the competition opens. Each registration allows one submission, whatever its outcome.

  2. 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.

  3. 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.

  4. 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 repositoryMiner manual

How it is scored

The rules

  1. 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.
  2. 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.
  3. 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.
  4. 04The competition's payout is split between the boards: Overall 50%, MLP 8%, ResNet 8%, MobileNet 8%, Normalized MLP 8%, Mixer 8%, Recurrent 8%.
  5. 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.
  6. 06The gain has to hold up: a bootstrap over the paired rounds must keep it above zero, or the entry stays a challenger.
  7. 07No input group may be slower than 1.100× of the champion's time. One that is fails the guard, however fast the rest.
  8. 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.
  9. 09Each board pays its current champion only. A board nobody has taken pays the treasury.
  10. 10Every run also times the shipped baseline kernels. That comparison is shown for reference only; a board is decided against its champion.
  11. 11Only a registration made after the competition opened can enter, once per registration.
  12. 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.
  13. 13A champion's Kernel.lean stays private while it holds any board. Once it holds none, anyone can download it from its entry page.
  14. 14If a board's champion cannot build or its outputs disagree, the board pauses. Waiting entries keep their place and are retried.