Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

First Proof

arxiv.org

Post reply on HN
Print view View original

91–100 of 126 posts

Re: First Proof

#91

Post by robinzfc »

LegionMammal978 wrote: post #57
Western0 wrote: post #40

No, this is not a proof because not using Mizar ;-) https://mizar.uwb.edu.pl/

Would something be a proof in that sense even if it did use Mizar? As far as I can tell, Mizar has no complete reference for its language semantics, except for the single closed-source implementation. In general, information about the system itself (outside of the library) seems very scarce, or at least scarcely advertised.

Mizar source was "available upon request" for maybe 30-40 years. It got completely open-sourced under GPL some 3 years ago (maybe earlier, not sure), see [1], also [2] and [3] about an alternative implementation in Rust. Mizar is indeed "scarcely advertised", but all the information is publicly available, who wants to know knows. As for Mizar semantics, see for example [4].

[1] https://github.com/MizarProject/system [2] https://github.com/digama0/mizar-rs [3] https://arxiv.org/pdf/2304.08391v2 [4] https://link.springer.com/article/10.1007/s10817-018-9479-z

Re: First Proof

#92

Post by data_maan »

bwfan123 wrote: post #66
data_maan wrote: post #47

Earlier quoted context omitted.

On the website https://1stproof.org/#about they claim: "This project represents our preliminary efforts to develop an objective and realistic methodology for assessing the capabilities of AI systems to autonomously solve research-level math questions." Sounds to me to be a benchmark in all but a name. And they failed pretty terribly at achieving what they set out to do.

> And they failed pretty terribly at achieving what they set out to do. Why the angst ? If the ai can autonomously solve these problems, isnt that a huge step forward for the field.

It's not angst. It's intense frustration that they 1) are not doing the science correctly, and 2) that others (e.g. FrontierMath) already did everything they claim to be doing, so we won't learn anything new here, but somehow 1stproof get all the credit.

Re: First Proof

#93

Post by bawolff »

data_maan wrote: post #92
bwfan123 wrote: post #66

Earlier quoted context omitted.

> And they failed pretty terribly at achieving what they set out to do. Why the angst ? If the ai can autonomously solve these problems, isnt that a huge step forward for the field.

It's not angst. It's intense frustration that they 1) are not doing the science correctly, and 2) that others (e.g. FrontierMath) already did everything they claim to be doing, so we won't learn anything new here, but somehow 1stproof get all the credit.

Are they really trying to do science, or are they just trying to determine pragmatically whether or not current AI is useful for a research mathematician in their day to day job?

Re: First Proof

#94

Post by okintheory »

Syzygies wrote: post #23

I'm a mathematician relying heavily on AI as an association engine of massive scope, to organize and expand my thoughts. One doesn't get best results by "testing" AI. A surfboard is also an amazing tool, but there's more to operating one than telling it which way to go. Many people want self-driving cars so they can drink in the back seat watching movies. They'll find their jobs replaced by AI, with a poor quality of…

I think you're misunderstanding the point this paper is trying to make. They're interested in trying to distinguish whether AI is capable of solving new math problems or only capable of identifying existing solutions in the literature. Distinguishing these two is difficult, because self-contained math problems that are easy enough for LLMs to address (e.g. minor Erdos-problems) may have been solved already as subcomponents of other work, without this widely known. So when an AI makes progress on such an Erdos problem, we don't know if it had a new idea, or correctly identified an existing but obscure answer. This issue has been dogging the claims of AI solving Erdos problems.

Instead, here you get questions that extremely famous mathematicians (Hairer, Spielman) are telling you (a) are solvable in <5 pages (b) do not have known solutions in the literature. This means that solutions from AI to these problems would perhaps give a clearer signal on what AI is doing, when it works on research math.

Re: First Proof

#95

Post by yorwba »

data_maan wrote: post #90
pickleRick243 wrote: post #62

Earlier quoted context omitted.

I don't think it's that serious...it's an interesting experiment that assumes people will take it in good faith. The idea is also of course to attach the transcript log and how you prompted the LLM so that anyone can attempt to reproduce if they wish.

If you want to do this rigorously, you should run it as a competition like the guys at the AI-MO Prize are doing on Kaggle. That way you get all the necessary data. I still think this is bro science.

If this were a competition, some people would try hard to win it. But the goal here is exploration, not exploitation. Once the answers are revealed, it's unlikely a winner will be identified, but a bunch of mathematicians who tried prompting AI with the questions might learn something from the exercise.

Re: First Proof

#96

Post by Davidzheng »

okintheory wrote: post #94
Syzygies wrote: post #23

I'm a mathematician relying heavily on AI as an association engine of massive scope, to organize and expand my thoughts. One doesn't get best results by "testing" AI. A surfboard is also an amazing tool, but there's more to operating one than telling it which way to go. Many people want self-driving cars so they can drink in the back seat watching movies. They'll find their jobs replaced by AI, with a poor quality of…

I think you're misunderstanding the point this paper is trying to make. They're interested in trying to distinguish whether AI is capable of solving new math problems or only capable of identifying existing solutions in the literature. Distinguishing these two is difficult, because self-contained math problems that are easy enough for LLMs to address (e.g. minor Erdos-problems) may have been solved already as subcomp…

I find it unbelievable that this question can't be settled themselves without posting this simply by asking the AI enough novel questions. I myself have little doubt that at least they can solve some novel questions (of course similarity of proofs is a spectrum so it's hard to draw the line at how original they are)

Re: First Proof

#97

Post by Davidzheng »

pegasus wrote: post #56
nemo1618 wrote: post #33

Earlier quoted context omitted.

Centaurs are a transient phenomenon. In chess, the era of centaur supremacy lasted only about a decade before computers alone eclipsed human+computer. The same will be true in every other discipline. You can surf the wave, but sooner or later, the wave will come crashing down.

They are transient only in those rare domains that can be fully formalized/specified. Like chess. Anything that depends on the messy world of human - world interactions will require humans in the loop for translation and verification purposes.

Sure, but in pure mathematics there are a lot of well specific problems which no one can solve.

Re: First Proof

#98

Post by okintheory »

Davidzheng wrote: post #96
okintheory wrote: post #94

Earlier quoted context omitted.

I think you're misunderstanding the point this paper is trying to make. They're interested in trying to distinguish whether AI is capable of solving new math problems or only capable of identifying existing solutions in the literature. Distinguishing these two is difficult, because self-contained math problems that are easy enough for LLMs to address (e.g. minor Erdos-problems) may have been solved already as subcomp…

I find it unbelievable that this question can't be settled themselves without posting this simply by asking the AI enough novel questions. I myself have little doubt that at least they can solve some novel questions (of course similarity of proofs is a spectrum so it's hard to draw the line at how original they are)

I settle this question for myself every month: I try asking ChatGPT and Gemini for help, but in my domains it fails miserably at anything that looks new. But, YMMV, that's just the experience of one professional mathematician.

Re: First Proof

#99

Post by seg_lol »

okintheory wrote: post #98
Davidzheng wrote: post #96

Earlier quoted context omitted.

I find it unbelievable that this question can't be settled themselves without posting this simply by asking the AI enough novel questions. I myself have little doubt that at least they can solve some novel questions (of course similarity of proofs is a spectrum so it's hard to draw the line at how original they are)

I settle this question for myself every month: I try asking ChatGPT and Gemini for help, but in my domains it fails miserably at anything that looks new. But, YMMV, that's just the experience of one professional mathematician.

New doesn't have to mean "the hardest thing yet", but as humans mastering our subdomain, they are often the same.

Re: First Proof

#100

Post by ozgung »

This is exciting as a reality check of our expectations from the current level of AI. I expect AIs to solve at least 2-3 of them in a week. I expect one “easy” problem that multiple models solve. And I expect at least one solution to be “interesting” and different than the human solutions. I also expect human researchers to solve more than AIs in a week (globally, by total) but I don’t know what happens if they publish their results during the week. We’ll see results soon.
Post reply on HN