logoalt Hacker News

jrflotoday at 7:21 PM3 repliesview on HN

I don't think it really attacks human understanding though. You can still read and understand an AI written proof. If another person comes up with a solution to a problem, you can read their methods and understand it. It doesn't matter if a human came up with that or not. It's really only attacking the "generating new ideas" part.


Replies

9question1today at 7:37 PM

That's precisely the problem though. You cannot still read and understand an AI written proof at the current skill level of the AI being applied, because they're orders of magnitude longer than human written proofs even when they don't need to be, and spend most of that length on the parts that aren't important. This has been really thoroughly documented by expert mathematicians who are engaging with AI in public like Terence Tao and showing in detail how much work it takes working alongside AI to figure out how to understand AI generated proofs. With human generated proofs that process is forced to happen before publishing the proof because the new style of AI generated proofs validated only by formal verification is supplanting the old human peer review process that forced the burden of understanding onto the publisher and not the reader.

show 2 replies
ksopedtoday at 7:40 PM

Not "a" human's understanding; Humanity's understanding. Understanding the research problem, and the solution especially, is a lot more involved than simply "read their methods". That's the whole point being made.

It matters if a human came up with it because of everything mentioned in the article... A mathematician's solution is necessarily built on other's ideas that have been disseminated, internalized, pressure tested etc. Methodologies differ too. AI can abuse its compute resources and generate a true/false or counterexample statements, without laying the foundation that a decade of globalized research would have.

well_ackshuallytoday at 7:48 PM

>You can still read and understand an AI written proof.

No you can't lol, they're multi million lines of Lean, which is already an obscure language to understand. It's an assault on your senses.

show 1 reply