←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
248 points rishicomplex | 1 comments | 17 Nov 24 17:20 UTC | HN request time: 0.203s | source
Show context
throwaway713 ◴[17 Nov 24 22:24 UTC] No.42167915[source]▶
Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?
replies(11): >>42168138 #>>42168188 #>>42168552 #>>42169054 #>>42169223 #>>42169808 #>>42170065 #>>42170119 #>>42170460 #>>42171863 #>>42197083 #
margorczynski ◴[17 Nov 24 23:00 UTC] No.42168138[source]▶
I doubt it. Math has the property that you have a way to 100% verify that what you're doing is correct with little cost (as it is done with Lean). Most problems don't have anything close to that.
replies(2): >>42168205 #>>42169130 #
AlotOfReading ◴[18 Nov 24 02:16 UTC] No.42169130[source]▶
Math doesn't have a property that you can verify everything you're doing is correct with little cost. Humans simply tend to prefer theorems and proofs that are simpler.
replies(1): >>42172952 #
thrance ◴[18 Nov 24 15:06 UTC] No.42172952[source]▶
You can, in principle, formalize any correct mathematical proof and verify its validity procedurally with a "simple" algorithm, that actually exists (See Coq, Lean...). Coming up with the proof is much harder, and deciding what to attempt to prove even harder, though.
replies(1): >>42173253 #
1. AlotOfReading ◴[18 Nov 24 15:30 UTC] No.42173253[source]▶
You can verify it with a simple algorithm, but that verification won't always be cheap. If it was, curry-howard would be incredibly uninteresting. It only seems cheap because we usually have little interest in exploring the expensive theorems. Sometimes we do though and get things like the 4 color theorem whose proof verification amounts to combinatorial search.