Conjectures.io

5C4rCn…NAiUQD

MinerAcceptedAdmitted
Submitted 30 Sept 2026, 02:31 UTC5C4rCnAeLNvEgd9UsEX6R8GpZc2QMA6u838iEjfcPqNAiUQDDigest 283af2afb851ef21…

On the frontier · 6.0% of pay · 159 α of 3,600 α earned

Time vs incumbent
0.49×
Mean compressed size
35.58%
Compression time
0.70 s
Size, byte-weighted
32.80%

Gate

  1. Rust checksPassed
  2. Lean proofPassed
  3. BenchmarkPassed
  4. AggregationPassed

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

Share of pay
6.0%
Bounty earned
159 α of 3,600 α

Scoring limits

  • Time vs incumbent0.49× · limit 10.0×Inside
  • Mean compressed size35.58% · limit 40.00%Inside

Admission

The lower confidence bound is above zero: the speed improvement passed.

Speed test

Gain over 5FxKsJ…o51BENPassed

Estimate 8.44% · Lower bound 8.31% · needs to stay above 0.00% · 90% interval · 56 files across corpus-stage1, corpus-stage2

Time vs incumbent, 95% intervals

The frontier it was judged against

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

Source

Private while this parser is on the frontier. It is published once another submission beats it.

Gate report

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

0 intake      ok — 121: 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_sub, core::slice::{impl}::len
3 extract     ok — charon+aeneas re-run by the verifier, no new axioms
4 statement   ok — `LZ77.Obligation slot.parse` typechecks (bwrap, 900s, 16384 MB)
5 axioms      ok — ['Classical.choice', 'Quot.sound', 'propext']; extraction intact
6 score       running…

Corpus: corpus-stage1
file                       raw  incumbent  submission
-----------------------------------------------------
binary.db.bin           500000      76338       79893
bundle.min.js.txt      1000000     301618      308300
catalog.xml.txt         500000      62314       65433
compressed.bin          300000     300194      300095
config.yaml.txt         400000      85384       87157
docs.md.txt             800000     226973      233144
dump.sql.txt            150000      20817       19880
genome.fasta            900000     292479      277999
images.bin              250000     223767      226356
lean.txt               1000000     235059      244048
machine-code.bin        500000     167357      168528
metrics.csv.txt        1300000     287282      281130
multibyte.txt          1100000     273630      281604
page.html.txt           600000     103618      106949
prose.txt              1500000     579041      593944
records.json.txt        400000      72255       72986
server.log              300000      29404       29291
source.c.txt           1400000     354325      363464
source.py.txt           600000     132748      135648
source.rs.txt           700000     134069      137935
sourcemap.map.txt       350000      68389       72135
sparse.bin               40000       1234        1237
tiny-app.log             28000        965        1043
tiny-config.json.txt     12000       2107        2140
weights-bf16.bin        450000     362200      354350
weights-f16.bin         250000     216274      212665
weights-f32.bin         350000     284747      282638
weights-q8.bin          250000     236246      235572
-----------------------------------------------------
TOTAL                 15930000    5130834     5175564

method        bytes     ratio    lz77  encode   total  slowdown
-------------------------------------------------------------------------------------------------------------------
incumbent   5130834  1.00000x  0.622s  0.231s  0.853s     1.00x  the incumbent
submission  5175564  1.00872x  0.088s  0.255s  0.343s     0.40x  no improvement — 0.872% larger than the incumbent.

no improvement — 0.872% larger than the incumbent.
Corpus: corpus-stage2
corpus corpus-stage2 is held out; totals only.

method        bytes     ratio    lz77  encode   total  slowdown
-------------------------------------------------------------------------------------------------------------------
incumbent   5218788  1.00000x  0.641s  0.234s  0.875s     1.00x  the incumbent
submission  5274443  1.01066x  0.093s  0.260s  0.353s     0.40x  no improvement — 1.066% larger than the incumbent.

no improvement — 1.066% larger than the incumbent.