The unproven inputs
What the formal proofs rest on. Formalize one, and every problem that assumes it becomes unconditional.
Click any assumed theorem to see its blast radius: the problems whose only formal support falls with it if the assumption is retracted.
Named results a proof takes as given, as an axiom or as a hypothesis it never discharges. These are the frontier’s real dependencies: each is a known theorem not yet in Mathlib, and formalizing it clears the problems that cite it.
A proof here carries a problem-specific hypothesis it did not prove. Unlike the assumed theorems above, these are internal to one problem, so they are a fidelity concern for that proof rather than a shared input to formalize.
Not a kernel proof: the argument trusts a native-compiled computation
(native_decide), which extends the trusted base beyond Lean’s kernel.