waynecochran

I would really like to see an AI invent a new set of (consistent) axioms from which a whole slew of new problems and solutions arise. Something akin to Euclidean geometry, but for a whole new landscape of theorems.

LEAN and other tools verify from what do know -- at least stepwise. Anything that deviates from these things should stick out. I suppose some million line LEAN program may have embedded within it something that is novel and not readily apparent, but I imagine truly novel approaches should stick out like a sore thumb.

Could AI create a novel set of axioms (a new math) from which things like RH become a by product? I think that would be hard to miss.

What is the current thought on AI creating new emergent forms of mathematics? Even the most stunning results like the proof of the quasi-RH are a clever combination of known mathematics. Humans have created (discovered?) stunning new ideas (e.g. complex numbers) that have opened wide new horizons -- do we think AI will be capable of creting / discovering novel new things like this?

Great. Glad it worked for you.

FORTRAN 77 was the language for the first programming language course I took. I absolutely hated computers and programming after that course. Later I took CS courses and used Pascal -- one day the concept of abstraction hit me as we were developing data structs in the 2nd semester and the light went on. That is when I first started to love programming. FORTRAN was thereafter referred to as the F language. Sorry to be a bummer, but I still recoil when I hear about that language.

I had to quit using desktop Safari because it essentially quit working. The problem had something to do with icloud. Apple assumes everyone is using icloud I imagine and does not handle corner cases for folks with full icloud disks or improper setups. I have an paid icloud subscription now, but I haven't looked back.

<unbearable web page to read>

Yes, of course. It makes complete sense to have the implementation of a C++ compiler to be written in a highly portable and much simpler language like C.

Yes, it is hard, psychologically, to grant trust to some silly perverse little thing I want crush like a surreal cartoonish cockroach.

Excellent description. I feel like I understand how a fridge works now -- when I took physics as a freshman in 1985 I was just surviving and I remember just getting it enough to pass the test on the thermo section but never really grasping it. You basically have a year to understand what it took man centuries to figure out.

My premise was that the proof was opaque -- i.e., no insight was to be gained from it.

I am not sure this is either end. An obscure proof to RH or P < NP does not seem to solve anything -- seems to leave us right where we are -- that was my point. We would know a fact for which we could do nothing with nor gain any new insight.

Would it matter if AI had a proof for RH or P < NP, but the proof was 1000 pages long that Leaf could verify but otherwise impenetrable by a human mind? We generally assume these are true already -- I am not sure a long convoluted proof puts us in a much different place.

Again with the gatekeeping. An AI generating a convoluted proof for some conjecture is not gatekeeping. It just does not care if you understand. It only cares enough that it can be verified -- usually using some other opaque proof tool like Lean.

Folks keep using the word "gate keeping" -- I never used that term nor implied intentional gate keeping. It's simply not caring if those outside the club understand -- there is no one guarding the door its just folks don't care if anyone finds it.