Perhaps it could benefit from being prompted to work more formally and make more incremental proofs? e.g. if it thinks it has an obstruction, it should prove th

Perhaps it could benefit from being prompted to work more formally and make more incremental proofs? e.g. if it thinks it has an obstruction, it should prove that some example shows the obstruction, or prove that the property does in general cause a problem. Or if it has an idea for a lead, it could show that whatever property does imply the thing it wants. It could also dispatch to a subagent to report back with these kinds of incremental proofs (prove this really would be a problem, prove this would help, etc.).