Remix.run Logo
gus_massa 14 hours ago

With very difficult human generated proof, it's common that it take like 10 or 20 to make it understandable for mortals. The idea is to split the proof, create new notation, add intermedite steps that are nice, find a simpler path. It's like refactoring.

Sometimes the original proof is compleyely replaced, bit by bit, until there is an easy to understand version.

gus_massa 8 hours ago | parent | next [-]

Too late to edit:

"10 or 20" -> "10 or 20 years"

gaigalas 8 hours ago | parent [-]

Wow!

If curl developers are overwhelmed by AI PRs, imagine how mathematicians will feel verifying a huge backlog of automated proofs.

Or isn't there such a thing? Can someone make a very complicated automated proof that ultimately reveals itself to be useless?

gus_massa 5 hours ago | parent [-]

For math it's easy, everyone just ignore it. There is no Daniel to blame. There are a few post about P=/!=NP or the Riemann conjeture or rewriting physics each week that are posted to HN. I'm just ignoring them. Other mathematicians are just ignoring them. But you will not find anyone to blame.

There are a few "solutions" of conjetures that may be correct, like https://en.wikipedia.org/wiki/Abc_conjecture I'm not sure about the current state. There may be a few mathematicians trying to read some parts, or perhaps no. Perhaps in a few years the easy parts will be refactored and isolated, and published as special cases. And after a while, it may be verified or someone will find a gap and perhaps fix it. Just wait a few decades.

> Can someone make a very complicated automated proof that ultimately reveals itself to be useless?

It depends, on what you consider insightful. Take a look at "Determination of the fifth Busy Beaver value" https://news.ycombinator.com/item?id=45273999 in particular the first comment. Is that an heroic result that opens a lot of paths or a useless combination of tricks that no one will ever understand? (In my opinion a proof is a proof [standing applause emoji].)

tug2024 12 hours ago | parent | prev [-]

[dead]