←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
250 points rishicomplex | 3 comments | 17 Nov 24 17:20 UTC | HN request time: 0s | source
Show context
sega_sai ◴[17 Nov 24 22:32 UTC] No.42167962[source]▶
I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
replies(9): >>42168164 #>>42168732 #>>42168855 #>>42169086 #>>42169255 #>>42169394 #>>42169686 #>>42171742 #>>42176215 #
gosub100 ◴[18 Nov 24 19:52 UTC] No.42176215[source]▶
Ok so Claude says that the Riemann hypothesis is proven and gives you 1200 pages of math symbols backing it up. Now what?

You probably say "now a human can verify it" but what if the humans are wrong? What is the source of truth?

replies(1): >>42181708 #
1. Turneyboy ◴[19 Nov 24 09:55 UTC] No.42181708[source]▶
The nice thing about formal verification is exactly that. You have a separate tool that's very much like a compiler that can check those 1200 pages and tell you that it's true.

The source of truth here is the code we wrote for the formal verification system.

replies(1): >>42182929 #
2. gosub100 ◴[19 Nov 24 12:59 UTC] No.42182929[source]▶
Could formal verification prove the nexus between the Taniyama-Shimura conjecture and Fermat's last theorem? I don't claim to know what the former is, but I am skeptical that a system that can only validate what we already know would have any luck with sudden leaps between disparate corners of the field. Or worse, what if we had this verification 30 years ago, Wiles gets excited thinking he proved a 300 year old mystery, only to be told by the algorithm, "sorry son, this code doesn't verify. Try again next time!"
replies(1): >>42244827 #
3. falcor84 ◴[26 Nov 24 11:40 UTC] No.42244827[source]▶
> "sorry son, this code doesn't verify. Try again next time!"

But that's not how it works; rather it tells you about the specific issue with a particular step in the proof, which you then debug, as you would with code that isn't compiling (or not passing some static analysis test).