# Community Proof Statistics

<!-- generated by tools/leaderboard/generate.py — do not edit by hand -->

Verified output comes from active `library/index` records plus archived index records only after their active copy has been retired; append-only terminal-run telemetry comes from `proof-runs/`. Rates cover only logged runs and never guess historical failures from Git history. Timing is contributor-reported local proof plus verification time.

**546 verified proofs · 255 attributed · 291 historical/unknown · 527 logged terminal runs.**

## Efficiency Baseline

| Metric | Value |
|--------|------:|
| Successful terminal runs | 208 |
| Failed terminal runs | 319 |
| Decomposed after failure | 18 |
| Failed without decomposition | 301 |
| Run success rate | 39.5% |
| Provider attempts | 579 |
| Failed attempts | 371 |
| Attempt yield | 35.9% |
| Recorded run time | 98h 15m |
| Median / p90 run time | 5m 9s / 31m 55s |
| Verified successes per recorded hour | 2.12 |
| Proofs with run telemetry | 208 (38.1%) |

## Work Queue

**774 goals · 138 archived · 3 blocked · 216 open · 408 proved · 9 translated.**

## Efficiency by Difficulty

| Difficulty | Runs | Successes | Run success | Failed attempts | Median time |
|-----------:|-----:|----------:|------------:|----------------:|------------:|
| 1 | 85 | 29 | 34.1% | 74 | 5m 24s |
| 2 | 237 | 99 | 41.8% | 158 | 4m 41s |
| 3 | 177 | 72 | 40.7% | 119 | 6m 8s |
| 4 | 26 | 8 | 30.8% | 18 | 5m 53s |
| 5 | 2 | 0 | 0.0% | 2 | 31m 25s |

## Unresolved Effort

| Goal | Status | Difficulty | Runs | Failed attempts | Recorded time |
|------|--------|-----------:|-----:|----------------:|--------------:|
| `sq-add-sq-eq-three-mul-sq-s4` | `open` | 1 | 3 | 7 | 1h 26m |
| `nat-sq-lt-two-pow-s2` | `open` | 1 | 4 | 6 | 52m 47s |
| `consecutive-cubes-diff-odd` | `archived` | 2 | 3 | 5 | 21m 11s |
| `nesbitt-inequality-s1` | `open` | 1 | 2 | 4 | 47m 0s |
| `dvd-210-pow-fifteen-sub-pow-three` | `open` | 2 | 2 | 4 | 7m 0s |
| `cube-sum-ge-mul-sq` | `archived` | 2 | 2 | 4 | 5m 47s |
| `prod-one-sub-inv-sq-telescope` | `open` | 4 | 3 | 3 | 1h 9m |
| `six-dvd-pow-three-add-five-mul` | `open` | 2 | 3 | 3 | 46m 45s |
| `fourth-power-mod-five` | `archived` | 3 | 1 | 3 | 20m 27s |
| `cube-eq-triangular-sq-diff` | `archived` | 2 | 1 | 3 | 14m 49s |

## Contributor Leaderboard

Rank uses credited verified proofs. Explicit `solver≜...` provenance wins; older proof records without solver provenance use git add-author attribution as inferred historical credit.

| Rank | Contributor | Proof credit | Explicit | Inferred | Runs | Run success | Difficulty points | Score |
|-----:|-------------|-------------:|---------:|---------:|-----:|------------:|------------------:|------:|
| 1 | [@chat-bit-01](https://github.com/chat-bit-01) | 230 | 0 | 230 | 0 | — | 515 | 57250 |
| 2 | [@ohdearquant](https://github.com/ohdearquant) | 121 | 121 | 0 | 121 | 100.0% | 287 | 31725 |
| 3 | [@cgbarlow](https://github.com/cgbarlow) | 118 | 71 | 47 | 310 | 18.7% | 212 | 24150 |
| 4 | [@perttu](https://github.com/perttu) | 37 | 33 | 4 | 35 | 71.4% | 83 | 9225 |
| 5 | [@ruvnet](https://github.com/ruvnet) | 21 | 21 | 0 | 0 | — | 55 | 6025 |
| 6 | [@binto](https://github.com/binto) | 9 | 0 | 9 | 0 | — | 19 | 2125 |
| 7 | [@adam91holt](https://github.com/adam91holt) | 7 | 7 | 0 | 58 | 5.2% | 13 | 1475 |
| 8 | [@OceanLi](https://github.com/OceanLi) | 1 | 0 | 1 | 0 | — | 3 | 325 |
| 9 | [@perttu-mp](https://github.com/perttu-mp) | 1 | 1 | 0 | 3 | 33.3% | 1 | 125 |
| 10 | [@yarcles](https://github.com/yarcles) | 1 | 1 | 0 | 0 | — | 1 | 125 |

## Attribution Notes

**255 explicit solver credits · 291 inferred git credits · 0 uncredited proof records.**

Git add-author attribution covers 546 of 546 proof index files. It is used only where explicit `solver≜` provenance is missing.

## Providers and Models

| Provider / model | Verified proofs | Runs | Run success | Failed attempts | Solvers | Median time | Successes / recorded hour |
|------------------|----------------:|-----:|------------:|----------------:|--------:|------------:|-------------------------:|
| `claude / opus` | 56 | 53 | 90.6% | 19 | 5 | 4m 30s | 6.48 |
| `claude / template-zmod-crt` | 41 | 41 | 100.0% | 0 | 1 | 0s | — |
| `claude / template-sum-induction` | 36 | 36 | 100.0% | 0 | 1 | 0s | — |
| `codex / unknown` | 24 | 80 | 22.5% | 90 | 3 | 7m 38s | 1.45 |
| `openai / leanstral-2603` | 21 | 217 | 7.4% | 205 | 1 | 6m 30s | 0.30 |
| `openrouter / unknown` | 21 | 0 | — | 0 | 1 | — | — |
| `claude / template-decide` | 19 | 19 | 100.0% | 0 | 1 | 0s | — |
| `claude / template-zmod-decide` | 13 | 13 | 100.0% | 0 | 1 | 0s | — |
| `claude / template-sum-closedform` | 8 | 8 | 100.0% | 0 | 1 | 0s | — |
| `gemini / gemini-3.1-pro-preview` | 7 | 7 | 71.4% | 6 | 1 | 6m 32s | 5.32 |
| `manual / gpt-5.5` | 4 | 0 | — | 0 | 1 | — | — |
| `claude / template-nlinarith` | 2 | 2 | 100.0% | 0 | 1 | 0s | — |
| `claude / sonnet` | 1 | 1 | 100.0% | 0 | 1 | 42s | 85.71 |
| `claude / template-telescope` | 1 | 1 | 100.0% | 0 | 1 | 0s | — |
| `claude / unknown` | 1 | 0 | — | 0 | 1 | — | — |
| `openai / jackcloudman/Leanstral-2603-GGUF` | 0 | 47 | 0.0% | 47 | 1 | 31m 57s | 0.00 |
| `codex / gpt-5.3-codex-spark` | 0 | 1 | 0.0% | 3 | 1 | 1m 34s | 0.00 |
| `openai / leanstral-2603-sovereign` | 0 | 1 | 0.0% | 1 | 1 | 1m 22s | 0.00 |

## Recent Terminal Runs

| Ended (UTC) | Goal | Solver | Provider / model | Outcome | Attempts | Failed attempts | Time |
|-------------|------|--------|------------------|---------|---------:|----------------:|-----:|
| `2026-06-17T16:29:26Z` | `fib-two-mul-sq-diff-int` | [@adam91holt](https://github.com/adam91holt) | `codex / unknown` | `proved` | 3 | 2 | 9m 13s |
| `2026-06-17T00:21:09Z` | `sum-stella-octangula-closed-form` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:21:02Z` | `sum-range-succ-mul-two-pow-eq-closed` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:50Z` | `sum-range-recip-two-pow` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:47Z` | `sum-range-odd-mul-three-pow` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:45Z` | `sum-range-k-sq-mul-four-pow-closed` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:43Z` | `sum-range-k-sq-mul-five-pow-closed` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:38Z` | `sum-range-id-mul-three-pow-closed` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:36Z` | `sum-range-id-mul-neg-two-pow-closed` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:31Z` | `sum-range-four-cube-diff-eq` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:26Z` | `sum-range-cube-diff-eq-cube` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:21Z` | `sum-quadruple-product-closed-form` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:19Z` | `sum-pentatope-triple-product` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:16Z` | `sum-pentagonal-pyramidal-closed-form` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:12Z` | `sum-odd-squares-eq` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:09Z` | `sum-octahedral-numbers-closed-form` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:07Z` | `sum-octagonal-numbers-closed-form` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:20:02Z` | `sum-oblong-eq` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:19:58Z` | `sum-k-mul-succ-sq-closed-form` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |
| `2026-06-17T00:19:55Z` | `sum-k-mul-succ-mul-two-k-succ` | [@ohdearquant](https://github.com/ohdearquant) | `claude / template-sum-induction` | `proved` | 1 | 0 | 0s |

## Interpretation

- Leaderboard rank is based on verified proofs, then difficulty points; failures are credited as effort but do not improve rank.
- Run and attempt rates are descriptive, not causal model comparisons. Stratify by difficulty and wait for useful sample sizes.
- Infrastructure failures are excluded because they provide no evidence about mathematical or model performance.
- Historical proofs and failed attempts before this telemetry existed remain unknown rather than reconstructed.