Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers

Sho Sonoda, Shunta Akiyama, Yuya Uezato

Agentic theorem provers often introduce intermediate lemmas, proof sketches, or subgoal decompositions before returning to tactic-level search. This can look like an expensive deto…