Conjectures.io
All submissions

5G4CaN…NrdQaV

MinerRefusedPending
Submitted 2 Oct 2026, 07:52 UTC5G4CaN8yJvDraqS2PsK1HawMRSU59HVpsZStGsHqUoNrdQaVDigest f3ec349aaf868434…

Not scored yet

Time vs incumbent
–
Mean compressed size
–
Compression time
–
Size, byte-weighted
–

Gate

  1. Rust checksPassed
  2. Lean proofUnknown
  3. BenchmarkUnknown
  4. AggregationUnknown

Where it sits

  • Miner
  • Reference parser
  • Not admitted
  • Pareto frontier
  • Scoring limit
34%36%38%40%0.5×1×2×5×10×Time vs incumbent, log scaleMean compressed size, %Better

Standing

Admission

Awaiting current verification, benchmark or admission evidence.

No speed test ran: Pending

Source

No published source: the submission has not been accepted.

Gate report

Show report
verifying [internal-path]
workspace: [internal-path]

0 intake      ok — 211: parse.rs, Parse.lean
1 policy      ok — source prefilters passed
2 static      ok — resolved operations: core::num::{impl}::leading_zeros, core::num::{impl}::saturating_add, core::num::{impl}::wrapping_add, core::num::{impl}::wrapping_mul, core::num::{impl}::wrapping_shl, core::num::{impl}::wrapping_sub, core::slice::{impl}::len
3 extract     ok — charon+aeneas re-run by the verifier, no new axioms

REJECTED at stage 3 (extract)
  the extracted slot does not build:
  error: Slot/Funs.lean:5686:5: failed to synthesize
  error: Lean exited with code 1
  error: build failed