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

“Erdos problem #728 was solved more or less autonomously by AI”

mathstodon.xyz

Post reply on HN
Print view View original

331–340 of 385 posts

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#331

Post by ancillary »

lwansbrough wrote: post #14

Can anyone with specific knowledge in a sophisticated/complex field such as physics or math tell me: do you regularly talk to AI models? Do feel like there's anything to learn? As a programmer, I can come to the AI with a problem and it can come up with a few different solutions, some I may have thought about, some not. Are you getting the same value in your work, in your field?

I did a theoretical computer science PhD a few years ago and write one or two papers a year in industry. I have not had much success getting models to come up with novel ideas or even prove theorems, but I have had some success asking them to prove smaller and narrower results and using them as an assistant to read papers (why are they proving this result, what is this notation they're using, expand this step of their proof, etc). Asking it to find any bugs in a draft before Arxiving also usually turns up some minor things to clarify.

Overall: useful, but not yet particularly "accelerating" for me.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#332

Post by dpe82 »

nottorp wrote: post #280
maxwells-daemon wrote: post #122

I work at Harmonic, the company behind Aristotle. To clear up a few misconceptions: - Aristotle uses modern AI techniques heavily, including language modeling. - Aristotle can be guided by an informal (English) proof. If the proof is correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here. - Once a pr…

So what did the "AI" actually do? Translate an informal description of the proof into this Lean?

TFA says ChatGPT wrote the informal description.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#333

Post by randomizedalgs »

lwansbrough wrote: post #14

Can anyone with specific knowledge in a sophisticated/complex field such as physics or math tell me: do you regularly talk to AI models? Do feel like there's anything to learn? As a programmer, I can come to the AI with a problem and it can come up with a few different solutions, some I may have thought about, some not. Are you getting the same value in your work, in your field?

I'm an active researcher in TCS. For me, AI has not been very helpful on technical things (or even technical writing), but has been super helpful for (1) literature reviews; (2) editing papers (e.g., changing a convention everywhere in the paper); and (3) generating Tikz figures/animations.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#334

Post by uoaei »

maxwells-daemon wrote: post #122

I work at Harmonic, the company behind Aristotle. To clear up a few misconceptions: - Aristotle uses modern AI techniques heavily, including language modeling. - Aristotle can be guided by an informal (English) proof. If the proof is correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here. - Once a pr…

You seem to be openly contradicting your company's PR and language. Your description very clearly describes the "AI" as a tool to translate relatively informal specifications into formal proof logic, but does not itself do the proving.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#335

Post by bee_rider »

sibrahim wrote: post #158
aidenn0 wrote: post #148

Earlier quoted context omitted.

How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.

That's what's covered by the "assuming you have formalized the statement correctly" parenthetical. Given a formal statement of what you want, Lean can validate that the steps in a (tedious) machine-readable purported proof are valid and imply the result from accepted axioms. This is not AI, but a tiny, well reviewed kernel that only accepts correct formal logic arguments. So, if you have a formal statement that you'v…

How hard is it to go back to English, from Lean? Just as hard as going from English to Lean?

If it is easier to convert backwards, maybe the AI can at least describe what the equations mean…

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#336

Post by schrodinger »

ccppurcell wrote: post #222
ndriscoll wrote: post #179

Earlier quoted context omitted.

The problem statement is apparently > Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn? Which seems like it's the type of thing you give as a homework problem to state formally in an intro class.

Are you an expert? Not gatekeeping here but I have no intuition for what is easy or hard to formalise. A lot of very simply stated graph theoretical results are apparently extremely hard to formalise.

Voters: please reconsider your ups and downs. I think the “Are you an expert” question triggered a lot of downvotes when it was in fact asked in good faith to judge the person’s perspective of easy and hard.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#337

Post by dehsge »

falcor84 wrote: post #274
catlifeonmars wrote: post #149

Earlier quoted context omitted.

“Much longer” is doing a lot of heavy lifting there.

Let me put it like this: I expect AI to replace much of human wage labor over the next 20 years and push many of us, and myself almost certainly included, into premature retirement. I'm personally concerned that in a few years, I'll find my software proficiency to be as useful as my chess proficiency today is useful to Stockfish. I am afraid of a massive social upheaval both for myself and my family, and for society…

There are other bounds here at play that are often not talked about.

Ai runs on computers. Consider the undecidability of Rices theorem. Where compiled code of non trivial statements may or may not be error free. Even an ai can’t guarantee its compiled code is error free. Not because it wouldn’t write sufficient code that solves a problem, but the code it writes is bounded by other externalities. Undecidability in general makes the dream of generative ai considerably more challenging than how it’s being ‘sold.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#338

Post by dang »

maxbond wrote: post #220
dang wrote: post #194

Earlier quoted context omitted.

I respect your awareness of that, which I'm sure is much broader than mine is. HN consumes my attention; I'm all depth and no breadth. What I'm interested in is how well HN does at fulfilling its own mandate in its own terms. On that scale, it's getting worse—in this respect, at least, which is a big one. We're going to do something about it, the same way we've always tried to stave off the decline of this place ( ht…

> On that scale, it's getting worse... I don't mean to express doubt (you would know better than I) but what makes you say that? Do you think it's a consequence of external factors like the current political climate or of internal factors like HN getting larger?

I think it's both external and internal, but the internal factors are more important because a compromised immune system is more vulnerable to outer pathogens.

I'm not sure it's about HN getting larger, though. It's a bit hard to tell, but at least some of the upswing in cynical and curmudgeonly comments is coming from established users.

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#339

Post by svat »

aidenn0 wrote: post #148
maxwells-daemon wrote: post #122

I work at Harmonic, the company behind Aristotle. To clear up a few misconceptions: - Aristotle uses modern AI techniques heavily, including language modeling. - Aristotle can be guided by an informal (English) proof. If the proof is correct, Aristotle has a good chance at translating it into Lean (which is a strong vote of confidence that your English proof is solid). I believe that's what happened here. - Once a pr…

How do you verify that the AI translation to Lean is a correct formalization of the problem? In other fields, generative AI is very good at making up plausible sounding lies, so I'm wondering how likely that is for this usage.

It may help to look at this example concretely:

The natural-language statement of the problem is (from https://www.erdosproblems.com/728):

> Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn?

The Lean-language statement of the problem (which can be done either by hand or by AI) is (from https://github.com/plby/lean-proofs/blob/f44d8c0e433ab285541...):

    ∀ᶠ ε : ℝ in [>] 0, ∀ C > (0 : ℝ), ∀ C' > C,
      ∃ a b n : ℕ,
        0  n + C * log n ∧
        a + b
Yes on the one hand, one needs to know enough about Lean to be sure that this formulation matches what we intend, and isn't stating something trivial. But on the other hand, this is not as hard as finding an error on some obscure line of a long proof.

(There's also an older formulation at https://github.com/google-deepmind/formal-conjectures/blob/f... but the new one is more in the spirit of what was intended: see the discussion starting at https://www.erdosproblems.com/forum/thread/728#post-2196 which gives a clear picture, as of course does Tao's thread in the OP that summarizes this discussion.)

Re: “Erdos problem #728 was solved more or less autonomously by AI”

#340

Post by baq »

chpatrick wrote: post #311
baq wrote: post #264

Earlier quoted context omitted.

Finding a path in a maze was AI once.

I think that definition is pretty obsolete for the last 20 years. To me "AI" is machine learning, statistical algorithms trained on data. That's not true for Lean.

So basically anything we don’t know how to write an algorithm for? I see where you’re coming from - but at the same time it’s actually an AI meme and smells of permanently moving goalposts.
Post reply on HN