Comment by kevinventullo
12 hours ago
AlphaProof works natively in Lean. Literally the one part it couldn’t do was translate the natural language statements into the formalized language; that was done manually by humans.
I’m saying that the view of formalized languages as a crutch is backwards; they are in fact a challenging constraint.
The most extreme version of my position is that there is no such thing as a rigorous natural language proof, and that humans will view the relative informality of 20th and early 21st century mathematics much like we currently view the informality of pre-18th century mathematics.
I did not say formal languages are a crutch. I said they served as a crutch for the Alphaproof system, because they literally did.
It was there so the generator wouldn't go off the rails hallucinating and candidates could be verified. And the solving still took days. Take that away and the generator doesn't get anywhere near silver with all the time in the world.
That is the definition of a crutch. The generator was smart enough to produce promising candidates with enough brute force trial and error, but that's it. Without Lean, it wouldn't have worked.