Comment by matusp

The agents here very likely used search. On top of that, they have boundless patience and can quickly process top K hits to find what they need. This is exactly the skill that is super useful for finding various niche sub-proofs that can help you build the final proof. A human mathematician is not going to digest 1000 papers from a different sub-field to find the needle they want, not knowing if it is actually there. AI can do it in few hours.