Comment by robinhouston

2 hours ago

I don't think that's actually the real problem. Along with the progress in answering mathematical questions, recent progress on AI-powered autoformalisation has been astonishing. All the recent AI discoveries have been accompanied by Lean proofs.

And, yes: that doesn't absolutely guarantee correctness. The Lean kernel has had soundness bugs, and may have some still. But it's pretty strong evidence of correctness nevertheless.

The concern among mathematicians is not mainly that they doubt the correctness of any of these discoveries, but that human understanding may be devalued.

4 comments

robinhouston

Reply
vld_chk  1 hour ago

I am not that worried, but rather just observing. Humanity is about to enter the phase when we will be using things based on ideas no human ever properly understands. This thought … disturbing, somehow?

It is perfectly valid counterpoint to say that we already do it. We everyday use myriad of things, tools, and software we have 0 clue how it operates. But for us as humans it was reassuring that we know that at least there are a few other alive humans who know it, who create it and who can explain it.

With AI soon that comforting zone will be gone.

  • famouswaffles  38 minutes ago

    >Humanity is about to enter the phase when we will be using things based on ideas no human ever properly understands. This thought … disturbing, somehow?

    This is just normal though. We were building sophisticated bronze and steel tools long before any complex understanding of metallurgy or chemistry. Medicine is still the wild west.

    • bananaflag  24 minutes ago

      I first wanted to say fire, even though it's a cliche, but then I thought that in antiquity we used like everything without anything that would qualify today as understanding. Also now we have a lot of stuff that we "know" it works based on complicated numerical simulation.

      I think the most "understanding" we ever had was in the 40s-50s designing nuclear bombs with slide rules. It was the culture that produced the idea of psychohistory.

      > Medicine is still the wild west.

      Reminder that we have no idea how anesthesia works.