Results

Result 1. The AUC of obscurity and attention features for predicting AI resolution is

0.571

(95% CI

[0.511, 0.632]

) over 7 test origins, 4458 rows and 152 events. The threshold

0.6

is not reached, so H1 is not supported. Source. forecaster/out/backtest_results.json

Result 2. Bridge distance adds no predictive signal:

\Delta\mathrm{AUC} = -0.004

(DeLong

p = 0.54

, permutation

p = 0.61

). H2 is not supported. Source. forecaster/out/backtest_results.json

Result 3. Gradient boosting on all features reaches

\mathrm{AUC} = 0.49

and

\mathrm{Brier} = 0.034

against a base-rate Brier of

0.0341

. Source. forecaster/out/backtest_results.json

Result 4. 593 open Erdős problems carry an AI-resolution probability, with

7.8

resolutions expected in 3 months (model hgb_all). SHA-256 2c9a9d86ec22b205717723ce04ad9d8d6e013372f0f79b897e6813b3f1245981. Source. forecaster/out/forecast.csv, forecaster/out/forecast.sha256

Result 5. The formal-conjectures Erdős directory holds 909 Lean files with 2918 theorems: 2114 marked proved and 804 marked open by the repository. Lean verification under Rule 2 has not run (AXLE verify_proof false, axiom audit false, lake build false). Source. ~/euled-experiments/forecaster/data/formal-conjectures/FormalConjectures/ErdosProblems/

Result 6 (pending, 2026-10-24). G1, compute-matched comparison of arms A, B and C at 0.8 GPU-hours each. Verified solves: A 0, B 0, C 0. The power analysis requires 80 solves. Source. results.json: compute_matched

Result 7 (pending, 2026-10-24). G2, open-set solves on the 68 FME conjectures and formal-conjectures, ordered by coverage per cost. Source. results.json: fme

Result 8 (pending, 2026-10-24). Shortener cascade on AlphaProof Nexus proofs and new proofs, median reduction in steps, characters and kernel time. Source. results.json: shortener

Result 9 (pending, 2026-10-24). Reinvention audit: AlphaProof Nexus problems re-solved without the original proof. Source. results.json: reinvention

Result 10 (pending, 2026-10-24). PutnamBench (6 solved) and miniF2F (0 solved) under the pinned Lean toolchain. Source. results.json: putnambench, minif2f

Result 11 (pending, 2026-10-24). Exponential test: constant ratio against logistic growth by AICc over successive rounds (0 rounds run). Source. results.json: exponential_test

Result 12. GPU job euled-g0 on 2x T4 used

0.09

GPU-hours and ended with status failed:no-internet. Completed GPU-hours:

0

. Source. gpu_ledger.csv

Results

Downloads