Cost
What does a verified theorem cost?
Model cost is the provider-reported charge for every call, including calls replayed from the response cache (so each configuration is priced as if run alone). Lean time is the fast REPL checks plus the independent certification of every candidate proof.
Budget by configuration
| Configuration | Verified | Model calls | Tokens | Cost | Cost / verified | Tokens / verified | Lean check s | Certify s | Timeouts |
|---|---|---|---|---|---|---|---|---|---|
| Template (no LLM) | 26% | 0 | 0 | $0.00000 | $0.00000 | 0 | 259 | 8,778 | 0.0% |
| Direct (paraphrased prompt) | 3% | 174 | 82,020 | $0.020 | $0.00403 | 16,404 | 6 | 988 | 0.0% |
| Repair (paraphrased prompt) | 7% | 670 | 703,436 | $0.129 | $0.011 | 58,620 | 15 | 160 | 0.0% |
| Hybrid retrieval | 2% | 174 | 198,715 | $0.036 | $0.012 | 66,238 | 29 | 382 | 0.0% |
| Repair | 6% | 675 | 861,900 | $0.165 | $0.015 | 78,355 | 14 | 138 | 0.0% |
| BM25 retrieval + repair | 7% | 671 | 1,262,354 | $0.199 | $0.015 | 97,104 | 56 | 214 | 0.0% |
| Full − skeleton | 7% | 838 | 1,571,091 | $0.251 | $0.019 | 120,853 | 27 | 185 | 0.0% |
| Dense retrieval + repair | 5% | 680 | 1,163,873 | $0.187 | $0.021 | 129,319 | 24 | 126 | 0.0% |
| Hybrid retrieval + repair | 5% | 680 | 1,187,433 | $0.187 | $0.023 | 148,429 | 272 | 1,176 | 0.1% |
| Full (plan + retrieval + repair) | 7% | 841 | 1,952,639 | $0.333 | $0.026 | 150,203 | 49 | 744 | 0.0% |
| Full − memory | 6% | 842 | 1,705,014 | $0.303 | $0.028 | 155,001 | 12 | 162 | 0.0% |
| Full − retrieval | 5% | 844 | 1,405,154 | $0.266 | $0.030 | 156,128 | 23 | 1,022 | 0.0% |
| Direct | 1% | 174 | 104,753 | $0.030 | $0.030 | 104,753 | 5 | 12 | 0.0% |
| Full − compiler feedback | 6% | 844 | 1,820,390 | $0.311 | $0.031 | 182,039 | 16 | 2,517 | 0.0% |
| Direct ×4 | 1% | 691 | 411,650 | $0.119 | $0.059 | 205,825 | 75 | 535 | 0.0% |