alt Hacker NewsOne hesitation I have with this idea is that proofs themselves can be modeled as mathematical objects. So if you have a machine which can construct examples then we just view the proof as an example, and it should be good at constructing them.
Maybe this is naive.
LLMs are certainly good at generating proofs/solutions ("examples") to problems that humans know how to solve, since they were trained on these, and they will have learned how to generalize a bit from this. However, this isn't going to be a huge amount of help in tackling problems that have stumped humans unless they get lucky and it's more a matter of relentless perseverance (the obvious computer strength) using known techniques - plucking the low hanging fruit that humans have missed.