Formal-AVS: A Lean Benchmark for Anytime-Valid Confidence-Sequence Theorem Proving60 Lean 4 theorem targets on anytime-valid confidence sequences across four families (Howard-Ramdas, betting, Whitehouse vector, asymptotic CLT).
60 targets grouped into tiers T0-T3 (pre-evaluation) and categories T4-T5 (empirical)
7 drafters evaluated across single-shot, agentic, and unbounded modes
14 Aristotle sessions (unbounded refinement)
Headline Results… See the full description on the dataset page: https://huggingface.co/datasets/neurips-2026-avs-bench/formal-anytime-valid-stats.
