Comment by causalmodels
10 hours ago
Maybe I'll end up doing the write ups pseudonymously. I have taken care to make sure the results can meaningfully contribute to field but I don't want to plant flags or really receive credit of any kind. I just think they are interesting.
I like my current life and don't want to get dragged into the current fracas surrounding the use of AI in math.
If you have taken care, then share it with the community. People will be thankful and happy.
The problem is with people that may do it without contributing to the community.
If this was limited to just three results, I would agree with you. But those three are just the ones I've managed to verify myself. The list of unverified results is quite a bit larger.
The field I've been investigating is not large. Even if I were to take the time and care to beat the interesting results into something meaningful, I'm afraid the pace at which I'm able to produce these results would not be well received.
This all comes down to what we think mathematics is. There are two options here:
Mathematics is just the formal system: in that case we will never be able to beat the AI as humans. The goal is then to cover as much of the formal landscape with AI generated proofs to proof as much statements as possible. Success metrics are lines of lean and numbers of proven statements.
Or
The formal system is just a limited representation of what mathematics is: in that case probably some parts of the formal mathematical landscape are more important than others. Not all statements are born equal. And 90% of AI generated proofs will be just noise. Our job as mathematitians is to steer the AI to high mathematical value regions and turn formal proofs into mathematical proofs and insights.
From my point of view we have know since Godel that we are living in the reality of point 2.
Each of the two points implies a very different way of doing mathematics. So pick the one that you think is true and act accordingly.