Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AI in mathematics is forcing big questions

spectrum.ieee.org

Post reply on HN
Print view View original

141–150 of 193 posts

Re: AI in mathematics is forcing big questions

#141

Post by goalieca »

hiAndrewQuinn wrote: post #84
skybrian wrote: post #35

Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use: > A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs a…

Imo, the proved theorem is the API. And that's really all it has to be. If there are other lemmas, etc buried inside that 200k blob that can be factored out and proved and used themselves, so much the better. But denying a machine-valid proof just because it's incomprehensible with what a human being considers a reasonable effort made to unpack it just seems odd to me. I see no reason not to accept the vibe coded blo…

> Imo, the proved theorem is the API. And that's really all it has to be.

The novel approaches to solving challenging proofs is very useful.

Re: AI in mathematics is forcing big questions

#142

Post by Verdex »

therobots927 wrote: post #26
cpard wrote: post #20

Human mathematicians could become “priests to oracles.” Priests were interpreting the oracles (at least at a place like Delphi) according to the context of the people asking the questions aka participating in politics of that ancient times. Subjectivity was a feature and I’m not sure that fits to mathematics though. I wonder if mathematics as a science field moves more into engineering or if a different branch will e…

Human mathematicians could become “priests to oracles.” This is a decidedly anti-enlightenment statement.

Okay ..

However given the history of mathematics that's not really out of order. There's a lot of mysticism intertwined with early mathematics and it's only relatively recently that mathematics has taken the beads out of her hair, put on a business suit, and gotten to work.

I mean even Galileo's, the patron saint of skepticism, job was observing the stars so that he could write horoscopes.

And we see the attitude repeated even today. I work in a technical field and whenever I mention that I think type theory is kind of cool the response more often then not is for them to give me the ol' "Thank goodness for people like you, I'm just not a math person."

Re: AI in mathematics is forcing big questions

#143

Post by simonh »

FridgeSeal wrote: post #77
crystal_revenge wrote: post #58

Earlier quoted context omitted.

> Things that aren’t human intelligible aren’t human usable This is objectively false, people use things every single day they don't understand. We still have plenty of things about the world we don't understand but still find useful. You are saying anything we know to be the case, but cannot understand why cannot be used? Can we just stop sleeping because we haven't reasoned why sleep is necessary even though we kno…

If you’re fine with a future like Warhammer 40k where we all have to be Tech Priests making prayers and performing opaque rituals to get things out of the machine god because we no longer understand things, that’s fine, but that’s not a future the rest of us want.

It’s not a matter of what we want or don’t want, or are fine with. The universe doesn’t owe us explanations. Of course I’d prefer to understand everything, or as much as possible, but we don’t always get what we want.

Re: AI in mathematics is forcing big questions

#144

Post by bckgrndrdtn »

galaxyLogic wrote: post #67
skybrian wrote: post #35

Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use: > A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs a…

> Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. So why don;t they use AI to write Lean programs? That should make the AI-proofs more readily human undersrndable.

It's a mixed bag. Some people don't use AI, for the usual reasons that people don't use AI. Others have used AI to write Lean programs. For example the 200K loc example mentioned in OP. But generally speaking, the quality isn't good enough yet. And when you've looked at 13 AI-generated examples and found them lacking on various axes compared to Mathlib, then you'll take a break before being motivated to look at example 14.

Re: AI in mathematics is forcing big questions

#145

Post by zmgsabst »

cornholio wrote: post #109
zmgsabst wrote: post #70

Earlier quoted context omitted.

No — people don’t successfully use things they don’t understand every day. They approximately use them with varying degrees of success, but also mistakes, broken inferences, etc. My exact point is that your view reduces our ability to do mathematics to that broken, flawed usage and thereby undermines its utility for logical precision: mathematics is only useful because we cleanly understand it. When you try to use ma…

It's easy to find counterexamples: the entire science of pharmacology is based on macroscopic effects that often lack a fundamental understanding of the underlying mechanisms of action. Psychopharmacology is the extreme example. Often, the fact that a drug worked made scientists investigate and discover the mechanism behind it, but for many drugs used every day by billions it's still a mystery, or it's understood onl…

Psychopharmacology is a great example of “doesn’t reliably work” as their products have serious and even disastrous side effects at times — including SSRIs triggering violent acts and suicides.

Again, my exact point is that mathematics loses its utility when you reduce it to that inaccurate usage. You no longer can have any faith in the conclusions — just like sometimes psychiatrists kill their patients with an SSRI prescription because they don’t understand the drugs.

> Would the high priestess of human reason pass her divining rod over such chips or life-saving drugs and reject it as the work of the AI devil?

My point is you can’t know if you’re turning it over for life saving drugs or poison, if you don’t understand what you’re getting.

Re: AI in mathematics is forcing big questions

#146

Post by zmgsabst »

simonh wrote: post #143
FridgeSeal wrote: post #77

Earlier quoted context omitted.

If you’re fine with a future like Warhammer 40k where we all have to be Tech Priests making prayers and performing opaque rituals to get things out of the machine god because we no longer understand things, that’s fine, but that’s not a future the rest of us want.

It’s not a matter of what we want or don’t want, or are fine with. The universe doesn’t owe us explanations. Of course I’d prefer to understand everything, or as much as possible, but we don’t always get what we want.

You didn’t respond to his point:

In the 40k universe, modern humanity is below not just their peak of technological prowess, but even their peak of pre-AI prowess. Because they landed in a valley of superstition involving machines they do not understand — and have no way to rebuild towards their peak, without yet further losses by moving away from the magical machines.

That has nothing to do with the universe at large — and everything to do with human society and choices. Which we do have control over.

Re: AI in mathematics is forcing big questions

#148

Post by euroderf »

hiAndrewQuinn wrote: post #84
skybrian wrote: post #35

Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use: > A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs a…

Imo, the proved theorem is the API. And that's really all it has to be. If there are other lemmas, etc buried inside that 200k blob that can be factored out and proved and used themselves, so much the better. But denying a machine-valid proof just because it's incomprehensible with what a human being considers a reasonable effort made to unpack it just seems odd to me. I see no reason not to accept the vibe coded blo…

You might get the Riemann hypothesis robo-proven and unintelligibly dense. Would mathematic professionals trust it, or would they always be putting asterisks next to proofs downstream of it ?

Re: AI in mathematics is forcing big questions

#149

Post by lioeters »

bananaflag wrote: post #105
6thbit wrote: post #104

I always struggled with my lack of intuition vs that of my peers that had had a more comprehensive ‘math upbringing’. Is direct experience and struggle really the only driver for developing intuition?

I am a mathematician, and I was never the kind to like to struggle by working on problems, but I developed a lot of intuition by 1) thinking deeply about definitions and proofs and why are they this way and not another 2) reading a lot of blogs and expository papers by great mathematicians, even (the more philosophically minded) mathoverflow q&a's (so I absorbed their way of thinking unconsciously). For example, I te…

> John Baez's This Week's Finds posts

As an aspiring amateur of recreational mathematics, it gives me joy to find this recommendation and start reading the series. It reminds me of Martin Gardner's "Mathematical Games" column, and its successor, Douglas Hofstadter's "Metamagical Themas".

For a while now I've been chewing on Baez's paper, "Physics, Topology, Logic and Computation: A Rosetta Stone". I'm intrigued by it. At first baffled, then continued studying related topics, coming back to re-read and appreciate what it's saying. I'm exploring what it means from the computation angle, in the context of Haskell Curry, combinators, lambda calculus, cellular automata, rewriting systems. And more far-fetched thoughts, like Stephen Wolfram, Max Tegmark, or how it may relate to biology such as Michael Levin's research.

On the role of AI in mathematics, it brings up more questions about the use of computers in experimental/exploratory mathematics. Part of the concensus emerging, it seems, is the formalization of programs as proofs, in particular the Lean language ecosystem. It's like the field of software engineering is rediscovering its roots.

The deeper I go the more I want to participate, write and talk about the fun things I'm discovering. Maybe one day write a paper of my own, if I can manage to do it in a respectable rigorous manner. For that I know I still have a lot of basics to learn, cultural etiquette too, and probably lean on something like Lean to be able to demonstrate that the ideas are sound.

Re: AI in mathematics is forcing big questions

#150

Post by lioeters »

PunchyHamster wrote: post #147

Is the big quesition same as in other domains, "how to stop AI bros from flooding us from slop that is made only to prove AI can do it too?"

News at 5: Team of corporate mathematicians working for OpenAI rewrites the foundation of mathematics in a billion lines of vibe-coded theorems and proofs that are so complex it's impossible for humans to review or understand. Next generation of children don't need to learn math anymore, they just get a subscription to OpenMath™.
Post reply on HN