Hacker News Reader

Comment by kens | Hacker News Reader

It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis. A mathematician (Mochizuki) claimed to have proven it in 2012 using a new theory called "Inter-universal Teichmüller theory" that almost nobody understands. Some mathematicians think the proof is correct while the majority don't. So the conjecture is in this annoying limbo where its status is a social construct rather than a decided fact.

https://en.wikipedia.org/wiki/Abc_conjecture

View on HN

> It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis.

People did attempt this:

https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...

Here are Kirti Joshi's comments about the LANA project report: https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...

I'm sure over the next 6 months both OpenAI and Anthropic are going to continue pouring many many millions of dollars into any famous open mathematical problem like that. There is a limited pool of problems which have held prestige for enough time to make general news headlines when solved and you don't really get nearly as much limelight for proving it the second time or adding in proof for additional cases/forms.

That's true of the entirety of mathematics. Its validity is a social construct. That is not to relativize it entirely, but much of what was considered good and sound mathematics in the ancient Agean for example would now fall way short of what mathematicians consider valid proofs.

Mathematics is a human endeavor funded on communicating and sharing mental constructs. Some are useful but most of it is not about producing useful things, quite the opposite in fact.

Gödel showed you need to agree on definitions to even do any valid mathematical construct.

Truth is also ill defined. That's what I don't get about generating math with LLMs. Who cares if you make hundreds of pages and lean code and it gets a thumbs up for logical validity? Mathematics is so much more then concatenating valid logical statements.

There's a large difference between "wrong for the given definitions" and "right in that context, but wrong for other definitions" though.

I think I am make a much more basic point than what you're talking about but then again I am not sure what you're tying to say here...

The problem with the acceptance of the given proof of the abc conjecture is rooted in beliefs the proof had at least one erroneous step in its logic which leaves gaps not able to be filled back in without significant new work in the proof. It's not rooted in a difference of starting axioms, what Gödel wrote about, or what kind of truth there can be (though the foreignness has certainly never sped its review up). Your comment may have separate points to make about those things in general but it does not make the problem with the proposed proof the same as the issues which apply to all of mathematics.

Yeah I'm not talking about that one proof, I'm talking about the whole of mathematics. It's not manufacturing theorems, it's an ongoing conversation. It's poetry in the etymological sense, poesis, it's creative. Why would anyone think that manufacturing mathematics is a good idea?

“Good, he did not have enough imagination to become a mathematician.

[Upon hearing that one of his students had dropped out to study poetry]” ― David Hilbert

"We've pointed LLM 7.0 into verifying the Inter-universal Teichmüller theory, spent 100M$ in tokens and generated a 20k line Lean and a 100k line js repo, the result is that the theory is... proven! Hopefully that solves the issue (rather than recreating it with even more complexity)

Reply on news.ycombinator.com