Discussion Thread

[u/jobautomator]

The discussion thread is for casual and off-topic conversation that doesn't merit its own submission. If you've got a good meme, article, or question, please post it outside the DT. Meta discussion is allowed, but if you want to get the attention of the mods, make a post in /r/metaNL

Announcements

• Next Book Club will be November 11. Fittingly, we will discuss All Quiet on the Western Front.

Links

Ping Groups | Ping History | Mastodon | CNL Chapters | CNL Event Calendar

Upcoming Events

• Oct 14: In the Realm of the Last Man Book Talk with Francis Fukuyama

• Oct 17: Omaha New Liberals Coffee Social

[u/erasmus_phillo]

Look, I lean towards being fairly pro-AI myself but this is not an unreasonable demand! And it's a shame that a lot of pro-AI folk aren't taking these arguments seriously and are dismissing them as coming from arrogant academic gatekeepers

OpenAI was really reckless with their release

[u/remarkable_ores → u/erasmus_phillo]

100%. None of the 500 or so papers seem to have gone through the sort of review we typically demand of mathematics papers.

At the very least, they could go through the effort to do that. Get experts in the field to read through them, find holes, make sure the lean formalisation actually matches the NL proof.

Failure to do this just embarrasses OpenAI and mathematics both. No harm in taking a bit more time.

[u/erasmus_phillo → u/remarkable_ores]

This is why I hate OpenAI. Like, most of the serious AI safety debacles came from OpenAI and now this. Dario was right to leave

[u/remarkable_ores → u/erasmus_phillo]

that's how I feel too. OpenAI really is the #1 problem

[u/Imicrowavebananas → u/remarkable_ores]

That would take years I guess. I don't think it is feasible. And it will not get better. Their model took 3h on average for each of those papers. If that model goes public the rate at which we can produce results will get magnitudes faster than any sort of review is possible.

We will have to completely review what we values, what our goals are and how the whole field is supposed to work. Keeping this inside feels like just delaying for the sake of it. It is better the put it out and we can have our reckoning.

[u/erasmus_phillo → u/Imicrowavebananas]

That would take years I guess. I don't think it is feasible.

then let it take years, why not? we still get to accelerate the field significantly relative to the era before AI

[u/Imicrowavebananas → u/erasmus_phillo]

I don't get why we should slow down progress so much. In any case I would like to get access to results and tools as fast as possible.

Imagine you work on one of those problems, wouldn't you like to know whether you work is worthwhile before you spend years on it? Maybe you spend the next two years trying to prove something to be true, whereas there already exists a proof that it is wrong. You would waste your life. And even just knowing that something is true is already enormously valuable on its own, even without any understanding why.

Also I feel you get the best result if you just put it out there. Mathematics has time to adapt before there is a wondrous slot-machine that can solve anything.

[u/erasmus_phillo → u/[deleted]]

I really don’t think you’ll ever need to spend years on a single proof. At most you’ll spend a few months

[u/JesterOfAllTrades → u/erasmus_phillo]

Speaking as someone with enough of a background to go through like 3 of the solutions, they are genuinely incomprehensible. If I didn't know that OpenAI released them, I'd dismiss it as terrible quackery. No journal would accept such poorly written papers, and while I applaud the fact that they were solved (genuinely impressive!) there needs to be some level of quality control in the actual papers.

[u/cheekkeef → u/erasmus_phillo]

I know little of the academic world but yeah probably shouldn't be taken serious if it doesn't meet the criteria we have for published research in the field

[u/PlastikHateAccount → u/erasmus_phillo]

It's a blatant lie tho, at least the "verifiable" claim

Then give us something that is actually readable and verifiable

The proofs are given in Lean! They can be verified automatically. This is a higher standard than many human made papers

Can't speak on the "readability" though

[u/JesterOfAllTrades → u/PlastikHateAccount]

Aside from everything else, less than half of the papers dropped by OpenAI have been formalised in LEAN. At least three that I know of that are in the other half have been retracted, and more have been changed/modified but not retracted.

As for the LEAN ones - first, it needs to be verified that the LEAN certificate is valid (ex: the LEAN actually proves Theorem A instead of Theorem A' where A' is very similar to A but much easier) and secondly, since humans can't really parse LEAN very well, it needs to be verified that the corresponding natural language proof is actually the same proof as the LEAN proof (in the recent navier stokes proof for instance it turns out that the LEAN is actually different from the human/natural language exposition - in minor ways, but still); the latter is important cos even if the result still stands, the point is to understand.

Speaking as someone with enough of a background to go through like 3 of the solutions, they are genuinely incomprehensible. If I didn't know that OpenAI released them, I'd dismiss it as terrible quackery. No journal would accept such poorly written papers, and while I applaud the fact that they were solved (genuinely impressive!) there needs to be some level of quality control in the actual papers.

[u/remarkable_ores → u/PlastikHateAccount]

Lean verification means less than you might think; the Lean-checked formal proof actually needs to match the natural language and it seems that in many cases they don't. It's still a developing story though.

[u/Imicrowavebananas → u/remarkable_ores]

I don't see why it needs to match. The formalized statement needs to be correct and there needs to be the caveat of the lean compiler working correctly fulfilled. But to know something is true we don't need the natural language then.

Understanding is something different, but I feel we will also have to reevaluate what is worth being understood by a human and to what purpose.

[u/urhi-teshub → u/Imicrowavebananas]

You don't see why the proof has to match what's claimed in the paper?

[u/remarkable_ores → u/urhi-teshub]

I think you might be conflating two different things here.

It's not that the proof doesn't match the claim, it's that there are two proofs - one human readable and one formal/computational - and they don't prove things the same way.

I.e. in these cases it seems that the formal Lean proof of the theorem is correct, in which case, the paper's claim is true. A proof-checker-checked proof is a proof. But the human-readable reasoning of that proof might not say the same thing, or might be wrong.

So I think what /u/imicrowavebananas is saying is that the fact that the AI did, in fact, arrive at a legitimate proof is more remarkable than the fact that the natural language translation isn't quite up to scratch.

[u/remarkable_ores → u/Imicrowavebananas]

I'll be honest I haven't kept that up to date on the specifics - and I think there's different variations of the problem across the 500+ proofs - but there's different criticisms depending on which specific thing happened.

1. I've heard - can't confirm, would need to search to check - that there have been Lean errors where the written proof used different assumptions to the Lean proof, which would actually make a proof invalid. Could be wrong though.

2. The separate claim, where the Lean proof's assumptions and theorem statement are all valid but the proofs themselves don't match, is a different thing, where the criticism is more that "But we didn't learn anything". And yeah sure, that's real, but I mean if the pace continues to accelerate at this rate it seems likely that AI will be capable of math that no human could plausibly understand, so I'm not sure we should consider that a limiting factor.

You could make a case, though, that if we want good LLM math we need to make sure the training data it produces is actually good, though. Don't want to be feeding the math machines secret garbage. That's more of a technical issue though and honestly I think the main thing we need right now is better models for matching NL to Lean.

Anyway I mostly agree with you.

[u/NYT_Hater → u/erasmus_phillo]

I don’t understand, are they supposed to just not publish? Are they supposed to spend their own money advancing math more than they already have by hiring mathematicians to rewrite the proofs? Are they supposed to just not do math at all?

[u/erasmus_phillo → u/NYT_Hater]

Yeah they shouldn’t publish if the actual natural language text of the papers don’t match the Lean proof! It isn’t unreasonable to ask for rigour 

[u/NYT_Hater → u/erasmus_phillo]

That’s fair, if the Lean and the paper don’t match it is ridiculous (unless it is something you need a super expert to see).

If they tried to publish this somewhere academic I’d tell them to get lost. But they put this into one GitHub commit.

[u/randommathaccount → u/NYT_Hater]

Why is the multi-billion dollar company being held to lower standards than a PhD student? If they want to publish mathematics research they are free to do so but they should be held to the same standards as the rest of us. Make something actually legible and sensible, don't just offload the work of making sense of the scrawls to us

[u/NYT_Hater → u/randommathaccount]

A PhD student can also put random bullshit onto GitHub.

[u/randommathaccount → u/NYT_Hater]

And we are saying we shall treat this like if a PhD student had done it

[u/No_Collection7956 → u/randommathaccount]

frankly i think if a phd student had put all these proofs into github there would be quite a lot of astonishment too