[program_whiz]

Isn't the question at hand whether its bad for mathematics if "prove the circle has area 3" devolves into 500 lines of inscrutable lean code, vs just having `pi r^2 == 3`? Sure they both "proved" it true/false, but knowing an answer isn't as useful as knowing why its an answer. Knowing an answer does have some value, its just not as valuable. If I can't work it out myself, I just trust the oracle.

Now if you ask "does the area of unit circle equal 4?", I don't really know, but we can go back to the oracle and ask again (we haven't learned the general pattern).

Also, I'm not sure that assuming this 'area of circle' question was cutting edge math, that the oracle wouldn't say 'yes, to a certain level of tolerance'. Can't count how many times I've seen agent decide a test needs to be loosened or deleted because its an "edge case" or "blocking". If you don't understand the proof you might get back 'yes' for some versions of 'is the area of unit circle 3' (depending on complexity of that ask).

[skydhash]

It’s like the Hilbert’s problem and the birth of computers. Turing’s paper is like 66 pages, but the most valuable output is the Turing machine which can be explained in a few paragraphs.