Numina-Prover: Open-Source Vibe Proving for Informal Mathematics via Parallel Subagents

Frontier language models now reach research-level mathematics, and the strongest systems coordinate several models. But almost all such mathematics is informal—natural language and LaTeX—and there, unlike a competition answer or a kernel-checked formal proof, no external checker can certify a result: the proof is the argument, so a fluent proof can hide a gap only an expert catches, and existing inference-time loops fall back on letting one model grade its own work. We present $\textbf{Numina-Prover}$, an open-source, model-agnostic, training-free system that constructs this correctness signal architecturally rather than importing it from a formal backend. First, a pure orchestrator writes no mathematics: it decomposes a problem into independently verifiable subproblems and dispatches generation, verification and revision to parallel subagents backed by different model families, so no proof is graded by the agent authoring the proof, while a steering channel lets a mathematician redirect a live run. Acceptance is gated by an adversarial verifier that only reports flaws, never repairs them, and must return clean across several independent runs—one flagged issue is a rejection. On seven research-level problems graded by senior expert mathematicians, Numina-Prover scores 78\% against 61\% for the strongest frontier model prompted directly and 70\% for a single-agent verification loop, with the largest gains on the hardest. It also helped settle a conjecture open for roughly a decade that frontier models alone could not solve at the time; the resulting proof has since been confirmed by an expert.