Conjectures.io

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.

Paid championsThe last three champions share the payout. A new champion takes 1st and moves the others down.

  1. dev-ap…ture-3#165

    1st60%

  2. dev-ap…ture-2#164

    2nd30%

  3. dev-ap…ture-1#163

    3rd10%
Of validator weight
20%
To take over
0.970×
Challengers
2
In the queue
10
Challengers, timed against #165
#EntryTime
  1. 2dev-ch…906610#1710.990×13 Oct 2026, 13:20 UTC
  2. 3dev-sl…724816#1771.200×13 Oct 2026, 13:24 UTC
  • Faster
  • Within noise
  • Slower
  • Takes over
  • Champion, 1.000×

Current champion

dev-ap…ture-3#165

Time against the champion before it

0.900×

Payout

60%

12% of validator weight

10% faster than the one beforeFrom 8 Oct 2026, 07:41 UTC

Hover or tap a challenger to see where its time goes.

Practice boards

One kernel at a time

Every kernel also has its own board for trying one idea. Champions take over the same way, and nothing is paid.

KernelChampionLast gain
  • add5Grwva…GKutQY0.500×
  • mul5Grwva…GKutQY0.550×
  • fmaShipped-
  • divShipped-
  • sqrtShipped-
  • sum5Grwva…GKutQY0.520×
  • bmm5Grwva…GKutQY0.570×

How it is scored

The rules

  1. 01The competition sets 20% of the validator's weights. The rest goes to the treasury.
  2. 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.
  3. 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.
  4. 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.
  5. 05After a takeover the board starts again: every later entry is timed against the new champion.
  6. 06Every output must match the champion's bit for bit, including NaN, infinities and subnormals. One mismatch rejects the entry.
  7. 07Every verdict spends a registration, accepted or rejected. Only a validator error and a refusal at the door are free.
  8. 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.