[krnsll]

If you think of this as a search, retrieval and “application” problem on the space of convex optimization proof techniques, it’s not a particularly striking result to a mathematician. Partly because: the space of results/techniques and crucially applications of those results and proof techniques is very rich (it’s an active field with many follow up papers).

On the other hand, I have a collection of unpublished results in less active fields that I’ve tested every frontier model on (publicly accessible and otherwise) and each time the models have failed to solve them. Some of these are simply reformulations of results in the literature that the models are unable to find/connect which is what leads me to formulate this as a search problem with the space not being densely populated enough in this case (in terms of activity in these subfields).