Reproduce

1. Forecaster backtest

The forecaster is the only finished experiment. One command reproduces its backtest.

git clone https://github.com/Questboy23/ai-math-forecast && cd ai-math-forecast && python code/run_backtest.py

The GPU prover runs G0 to G4 have not run, so they have no reproduction command.

2. GPU ledger

Every GPU job is logged in gpu_ledger.csv. Target 6.0 GPU-hours, hard cap 7.5, no new job after 6.5.

JobTagHardwareStarted (UTC)GPU-hoursTokensStatus
euled-g0kaggle2xT42026-10-24T06:18:26Z0.0900failed:no-internet

Completed GPU-hours: 0.00. Remaining under the 7.5 cap: 7.50.

3. Model versions

ModelSourceUseTraining cutoff
Goedel-Prover-V2-8BNumina/Goedel-Prover-V2-8B, mainG0 calibration, G2 open-set, G3 neural shortener2025-06 (model card)
Pythagoras-Prover-4BNumina/Pythagoras-Prover-4B, v1Backup prover2025-04 (model card)
GPT-OSS-120BOpenAI via fcc proxyFrontier calls, daily cap2024-10 (knowledge cutoff)

4. Pinned Lean toolchains

Each source builds in its own lake project with its own lean-toolchain.

SourceLean toolchainMathlib commitLake project
formal-conjectures (ErdosProblems)leanprover/lean4:v4.33.1pending~/euled-experiments/forecaster/data/formal-conjectures
FME (Epoch AI LeanOpenProblems)pendingpending~/euled-experiments/fme
AlphaProof Nexuspendingpending~/euled-experiments/alphaproof-nexus
PutnamBenchpendingpending~/euled-experiments/putnambench
miniF2Fpendingpending~/euled-experiments/minif2f

5. Repositories

  1. Questboy23/ai-math-forecast (forecast, Brier-scored)
  2. epoch-research/LeanOpenProblems (FME, 68 conjectures)
  3. google-deepmind/alphaproof-nexus-results
  4. trishullab/PutnamBench

6. Data files

The site is static files generated by build.py. No server computes anything.

  1. results.json: Full results per schema
  2. graph.json: 2948 nodes and 4074 edges
  3. search-index.json: Search index for the Solve panel
  4. forecast.json: Forecast data
  5. forecast.csv: Per-problem forecast
  6. gpu_ledger.csv: GPU job log
  7. background/progress.json: Background run numbers, pending until Lean-verified

7. External cost anchors

AnchorValueUnitSourceAccessed
AlphaProof Nexus cost per problem$300USDDeepMind publications (AlphaProof Nexus blog post)2026-10-24
FME cost per problem$300USDEpoch AI FrontierMath Erdős scaffold2026-10-24
GPU rate for dollar conversion2.50USD per H100-hourCloud provider pricing (Lambda Labs, RunPod)2026-10-24