Conjectures.io

Optimisation · TorchLean kernels

Open

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%

    Champion5HCF2C…HHscAS

  • ResNet10%

    Champion5HCF2C…HHscAS

  • MobileNet10%

    Champion5HCF2C…HHscAS

  • Normalized MLP10%

    Champion5HKaTt…oF77vZ

  • Mixer10%

    Champion5Gn6jG…SsMvrX

Boards
6
Takeovers
16
Entries
19
In the queue
13
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

Mixer

As it stood under #2Back to the current board
Challengers, timed against #2
  • Faster
  • Within noise
  • Slower
  • Takes over
  • Champion, 1.000×

Current champion

5Gn6jG…SsMvrX#6

Time against the one before

0.965×

4% faster than the one beforeSince 28 Oct 2026, 20:47 UTC

10.0% of the competition's payout

Champions on this board

  1. 5Gn6jG…SsMvrX#60.965×CurrentFrom 28 Oct 2026, 20:47 UTC
  2. 5ES53t…ERXCzz#40.876×28 Oct 2026, 19:41 UTC to 28 Oct 2026, 20:47 UTCKernel.lean
  3. 5Gb23s…iaWuoX#20.045×28 Oct 2026, 18:08 UTC to 28 Oct 2026, 19:41 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.

HotkeyOverallMLPResNetMobileNetNormalized MLPMixerOf the payout
5HKaTt…oF77vZChampion---Champion-60.0%
5HCF2C…HHscAS-ChampionChampionChampion--30.0%
5Gn6jG…SsMvrX-----Champion10.0%

Entries

Every entry, newest first

19 entries

  1. #195EWacn…JjBDKzWaiting1 hour ago
  2. #185DCwnB…Vt7SWcWaiting2 hours ago
  3. #175E4yXf…Ro2TuwWaiting3 hours ago
  4. #165EoHGu…8tCAyjWaiting4 hours ago
  5. #155DseAi…jYb7ZUWaiting4 hours ago
  6. #145E1kHW…JAq5oRWaiting4 hours ago
  7. #135EgqCS…9gPwm4Waiting4 hours ago
  8. #125FZHxN…PdepfQWaiting4 hours ago
  9. #115ERNeG…ULUTWVWaiting4 hours ago
  10. #105GsBit…yitPJGWaiting4 hours ago
  11. #95EvfEa…aRy7TDWaiting4 hours ago
  12. #85E5Pz7…BejLBrBenchmarking4 hours ago
  13. #75HCF2C…HHscASBenchmarking4 hours ago
  14. #65Gn6jG…SsMvrXCompleted4 hours ago
  15. #55HKaTt…oF77vZCompleted4 hours ago
  16. #45ES53t…ERXCzzCompleted4 hours ago
  17. #35CJyYn…1c4fHACompleted4 hours ago
  18. #25Gb23s…iaWuoXCompleted4 hours ago
  19. #15GWepY…riSvEkRejected4 hours ago
  • 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.

  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 --dev. It installs the pinned Lean packages, the sandbox and the miner client.

  3. 3Start from the reference

    Copy kernels/exact/incumbent, make it faster, and keep the proof that every kernel equals the specification.

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

How it is scored

The rules

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