Ironically though, what I imagine will happen, is that the researchers will pay OAI to use chatGPT to help themselves eval the proofs.
You have the frontier labs who are marketing that it’s over and they’re building intelligent machines and you’re saying the mathematicians should ignore it? Ok
Mathematicians, as autonomous entities with no formal connection to any AI lab, have zero obligation to do any work for those labs. OAI can't do anything if all the mathematicians band together and say "Sorry, we're not interested".
If they do chose to engage, they are doing so entirely voluntarily, and it would strongly indicate, if they are voluntarily doing it for free, that there is value (i.e. compensation, payment, barter, worthwhile, whatever) to be had by digging in.
That's right, and the difference is that this one is parasitic.
If reading each others work is symbiotic it makes sense OpenAI is parasitic: whose papers are they reading in return? No-one’s.
The problem people are having is they clearly are interested. They think the ideas are good. In fact, too good. If they thought otherwise, they would just say it's all slop, no one cares, business as usual. And you can tell that there's this phase change in their behavior because previously you could ask chatgpt about math and it would just give you word salad and everyone knew that. Now we can all see that it's not just word salad and people are scrambling to figure out what to make of that. Obviously an accurate answer oracle is still strictly useful even if it makes no attempt to tell you why (you can even use it only to help prove your boring technical lemmas when you have ideas!), so obviously this is an emotional reaction, not a rational one.
Shouldn't we pay for the best tools if it helps researchers to be more effective?
We need the companies to humanly review their papers. in the same way as at other companies we use humans to review the papers.
(If you're going to object that it's difficult to validate the statement of the problem, please first state your level of experience doing so. It's getting tiring seeing people raise this objection and claim that a statement is just as hard as a proof over and over who don't seem to actually know any math and have never tried to write anything in Lean)
Someone still has to read the formalization.
This _might_ have been true somewhat in the past (although it wasn't), but it's completely false today. Anyone with access to a sufficiently advanced model has the capabilities of analyzing these papers/proofs. It's no different than reading a codebase you might not be fully familiar with, and checking it for correctness (give an engineering analogy).
This hardcore gatekeeping of math (and by extension STEM) fields MUST stop.
Like I was reading some about adele rings last night, which is already going to be quite a concept for a layman to be able to even slightly describe. Then you can layer on that apparently they're locally compact, so we can talk about harmonic analysis on the additive group. Like, come on now, 99.99% of people have no hope of ever following along, and this is stuff from 75 years ago.
But they don’t. What they have is the ability to ask something else to do the analysis. It’s an important distinction. If the asker has the skills to evaluate the results, that’s one thing, but too many don’t and act as if whatever they got is unambiguous truth.
> This hardcore gatekeeping of math (and by extension STEM) fields MUST stop.
What must stop is the overuse of the word “gatekeeping”. Anyone is free to study these fields and work on problems. What people rightfully object to is uninformed research flooding everything with hard to verify junk.
Mathematicians do have some vested interest in keeping the profession from collapsing into an intellectual oligopoly, where one or two commercial players with early access to their own internal models continuously scoops everyone else and pollutes the field with externalities, and the profession itself collapses, only leaving AIs and hobbyists able to stand. At that point it'll be the AI firms who become rent-seekers. That's not really "gatekeeping" in any conventional sense of the term, it's protecting a healthy economy of ideas and the long-term development of mathematics.
Is someone stopping you from studying maths?
I also fail to see the issue you have with releasing abandoned source. In what world is that bad? That obviously is a gift and should be encouraged. e.g. id software's history of doing that has meant their work stays alive forever.