Hacker News Reader

Comment by gste | Hacker News Reader

> Using AI to find and highlight new principles, methods, or insights, rather than merely new proofs.

I would have assumed that, by producing new proofs, the AI has either validated existing principles, or discovered new ones? Isn't that worth studying?

Are mathematicians complaining that reviewing AI's proofs is not as fun as writing your own? Try being a programmer... welcome to our world!

If AI lacks imagination and is not discovering new principles, then it's doing us a favour: it's crossing out the problems that don't need new principles. So the problems/conjectures that are still left are the more interesting ones.

View on HN

I have done both scientific research and software development, they are not the same world. For a start, when you write a program you have a specific goal. When you ask a scientific question, you often don't.

Absolutely not. New proofs aren't the same thing as new proof techniques, AI is not generating new techniques (yet), and while the existence of more mechanical proofs is interesting those same problems if left to human mathematicians would have been much more likely to actually generate new techniques. Much like how tech has a "juniors" problem we're pushing on the future (no reason to hire juniors, so where are tomorrow's staff engineers going to come from), OpenAI's approach generated a "questions" problem where math and AI could happily coexist if we designed that correctly, but instead nobody's going to be generating or working on the right questions anymore.

> AI is not generating new techniques

Source? I assume that many of the approaches embedded in this proof dump will eventually be distilled and generalized into new techniques. That's how proof techniques tend to come about anyway (before AI): human mathematicians do something novel and unexpected to solve a particular problem, then efforts are made to understand how the "trick" works.

The point is that so far the AI is not doing a good job at explaining the "trick", so we (humans) have to do it. And the way these results are published at the moment (that is, dumping a load of proofs with badly written explanations) is not cooperative to enable this distillation (for example, presenting results at conferences and engaging with mathematicians). I recall Tao working through the disproof of the Jacobian conjecture, stating some steps as "miracles" for lack of better terms. If a human solves a problem in an unexpected way, at least there is some reason why they chose this path, which can help in understanding. This is not available to the same extent with AI generated proofs.

> The point is that so far the AI is not doing a good job at explaining the "trick", so we (humans) have to do it.

Sure, but that's a real technical limitation with current AIs, not something that AI firms should be blamed for. And if anything, this creates a viable career path for the mathematicians who were "scooped" wrt. the original solution: they can at least puzzle out what exactly the AI managed to do. Many practitioners are actually quite excited by this possibility; Tao's stance is by no means universally shared.

I'm about to start a PhD in mathematics. The idea of puzzling out what an AI did to prove something sounds quite boring and unappealing. But yes, maybe it's a viable career path.

I'm just not happy with the presentation of OpenAIs result. Maybe they could have gotten into contact with the people of the research areas of the problems that they solved and worked with them to create a better exposition. Sure, it's a slow process and requires lots of staff. But I believe that they can afford it.

> The idea of puzzling out what an AI did to prove something sounds quite boring and unappealing.

The way I see it, it's no different from a lot of grad student work where you have to figure out what a human-written proof is doing.

> Maybe they could have gotten into contact with the people of the research areas of the problems that they solved and worked with them to create a better exposition.

That's what Anthropic is doing, and the issue is that people will complain that they weren't the chosen "person to work with". OpenAI's approach is more like a race where everyone's at the same starting point: they get the AI's raw proof to work on and have to figure out how it works.

You raise good points. I don't have answers for them. We will see how this plays out in the next few months.

Reply on news.ycombinator.com