The Importance Oracle

Formal verification solves the correctness problem while leaving the importance problem open. A proof assistant can certify that a derivation follows from axioms, but it does not certify that the theorem was worth proving.

This matters because self-play needs a reward. For games, the terminal reward is available. For many theorem-proving tasks, correctness can be checked. For mathematical research, the missing object is a judge for whether a statement matters. There is no cheap oracle that scores a proposed lemma by whether it opens a field, compresses a proof, connects two literatures, or changes what problems become askable.

RLHF leaves the obstruction in place. If each judgment of importance requires expert mathematical taste, then the label is expensive and sparse. The candidate space is enormous, and most formally true statements are useless. The bottleneck moves from “can the system prove this?” to “which statements should enter the search space?”.

This is the sense in which proof search can scale while research taste remains hard to automate. AI can expand the set of closed questions without automatically expanding the set of good questions. The mathematician still has to decide which questions should enter the search process.

Blog Use

Use this to refine claims about AlphaProof-style progress. Fast verification enables powerful search, but research also needs question selection.

Source Trail

  • Jeremy Avigad, “Mathematicians in the age of AI”, arXiv:2603.03684.
  • Petra Schwer, “The meaning of doing mathematics”, arXiv:2509.15998.
  • ../ai_views.md, “The importance oracle problem” and “AI scales in the verifiable register”.
  • See reference_inventory.md for full source status.