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

171–180 of 193 posts

Re: AI in mathematics is forcing big questions

#171

Post by cdetrio »

Diogenesian wrote: post #168
bckgrndrdtn wrote: post #153

Earlier quoted context omitted.

> These proof checkers all have bugs, every single one Please show me a proof of `False` in Lean.

That's not what I mean. I am talking about quirks and bugs that really are pretty subtle, and which really might turn up in e.g. a verified systems programming context: https://github.com/James-Hanson/junk-theorems-in-lean/blob/m... (there is a proof of 0=1 at the end - it is easy to understand where it comes from, but low-level compiler stuff like this is always a possibility.) LLM agents will a) discover dumb count…

I'd be very curious whether such junk lean code could be used to solve Kevin Buzzard's Jacobian challenge: https://gist.github.com/kbuzzard/778bc714030b3e974ab5f403878...

The idea behind the challenge to provide a few lines of human-written/checked scaffolding that defines an "API surface". The API surface is resistant to junk/slop filling out the sorry's. This is supposed to reduce the number of lines that humans have to read to only a handful, while the full valid AI-generated proof is tens of thousands of lines. The challenge was just solved a couple weeks, here's the discussion about it: https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...

Re: AI in mathematics is forcing big questions

#172

Post by cornholio »

zmgsabst wrote: post #145
cornholio wrote: post #109

Earlier quoted context omitted.

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…

This is true for any drug, any drug can presumably become a poison, can interact with some genetic or biological trait and trigger a side effect and so on. The complexity of the biological systems is so great that they defy clear deterministic understanding, but stochastic empiric knowledge and treatments still have immense value.

If you give me an inference chip that runs 200x faster, yes, it could be backdoored to take control of my dishwasher and kill me in my sleep - but I can't deny it runs 200x faster an account of nobody being able to explain why. The same for the mistery cancer drug that cured everyone who took it up to now, but could, without doubt, kill the next patient.

Re: AI in mathematics is forcing big questions

#173

Post by whoke »

crote wrote: post #139
_zoltan_ wrote: post #91

Earlier quoted context omitted.

there is a difference but it's overrated. if a theorem is proven, then, as OP said, the theorem is the interface, no matter where the proof is. just as we don't re-prove Fermat's little theorem every time I use it in a proof, because well, it's a theorem.

> just as we don't re-prove Fermat's little theorem every time I use it in a proof Exactly! There's a shared foundation, and everyone builds upon it. A mathematical paper is a whole bunch of Lego blocks being added to that foundation, and combining them in a hopefully-useful new interface. But if the entire paper is just one giant black box, you only get to use the final interface: you lose the ability to meaningfull…

I think the interesting part here is that the black box gives us a starting point. And it's not a true black box: if a model is generating Lean, we can examine the entire source, iteratively refine by refactoring into smaller self-contained units, and the compiler gives us the certainty that our decomposition is correct.

Re: AI in mathematics is forcing big questions

#174

Post by dag100 »

guyomes wrote: post #122

Beyond the technical aspects, this new technology also leads to fundamental social changes. In particular, until now, mathematics were one of the rare sciences were great scientists could emerge from any country with a good education system. With the raise of strong AI tools, only scientists in rich countries with access to those tools might be able to advance faster on the most difficult problems like the millennium…

> mathematics were one of the rare sciences were great scientists could emerge from any country with a good education system.

But would they be able to realize their potential without further (mostly monetary and institutional) support from their country? In that way, things now are not so different from before. However, the story will probably change in a few years' time.

Computational intelligence obviates the role of the human in making capital reproduce and multiply. Mathematics as its own field of study might become pointless other than as a hobby - an endeavour reserved for those entitled to the machine's output. What the machine develops in the place of mathematics may not be recognizable enough to even share the same label - that is, if it even uses mathematical principles rather than just finding correlations that are 'good enough' for its use.

Re: AI in mathematics is forcing big questions

#175

Post by znkr »

euroderf wrote: post #148
hiAndrewQuinn wrote: post #84

Earlier quoted context omitted.

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 ?

We put asterisks next to proofs that use the axiom of choice. If a machine comes up with proof that’s not verifiable by humans, you can very well be sure that there will be asterisks.

Re: AI in mathematics is forcing big questions

#176

Post by murderfs »

bckgrndrdtn wrote: post #140
hiAndrewQuinn wrote: post #84

Earlier quoted context omitted.

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 are conflating: (i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib. Valid Lean proofs need maintenance. Mathlib is a living blob of code. People care about how fast the proofs typecheck. Many other properties of code play a role. Not everything that is true is worthy of immediately including in the Encyclopaedia Brittanica.

So add it as an axiom with a comment pointing to the proof. If you don't trust the proof because you don't personally understand it, why are you using a proof assistant in the first place?

Re: AI in mathematics is forcing big questions

#177

Post by bsder »

pfdietz wrote: post #156
bsder wrote: post #40

Earlier quoted context omitted.

> checking an existing fully fleshed out proof is simple The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.

His partisans are trying to formalize his proof. I expect they're not going to be able to do it, because the proof is flawed. This is one of the great things about formalization: it would have avoided this entire debacle.

> This is one of the great things about formalization: it would have avoided this entire debacle.

It's also a MASSIVE amount of SUPER TEDIOUS work. And it's the kind of work that folks who think up advanced math proofs tend to loathe. It's along the lines of programming by toggling in the code from front panel switches.

So what current mathematics does is judge a proof by whether or not the application of the proof somehow coincides with the result from some other adjacent branch of mathematical knowledge. So, a "novel" proof is expected to either help prove something in a slightly different branch of mathematics or simplify some already existing proof.

And that is, as I understand it, the crux of the matter with the Mochizuki proof of the "abc Conjecture." Solving the "abc Conjecture" should provide tools for solving other similar problems just like Wiles' proof of Fermat's Last Theorem provided an entire class of tools for dealing with modularity and elliptic curves. And yet Mochizuki seems to unable to do or demonstrate any of that.

So, Mochizuki's work is like someone dropping a gigantic and impenetrable proof of exactly and only Fermat's Last Theorem that doesn't apply to anything else. Sure, it would be an interesting (and true!) thing, but without the ability to use it further, it's a curiosity rather than a pillar.

Re: AI in mathematics is forcing big questions

#178

Post by pfdietz »

bsder wrote: post #177
pfdietz wrote: post #156

Earlier quoted context omitted.

His partisans are trying to formalize his proof. I expect they're not going to be able to do it, because the proof is flawed. This is one of the great things about formalization: it would have avoided this entire debacle.

> This is one of the great things about formalization: it would have avoided this entire debacle. It's also a MASSIVE amount of SUPER TEDIOUS work. And it's the kind of work that folks who think up advanced math proofs tend to loathe. It's along the lines of programming by toggling in the code from front panel switches. So what current mathematics does is judge a proof by whether or not the application of the proof s…

> It's also a MASSIVE amount of SUPER TEDIOUS work.

It was, but now autoformalization is a thing. If he had delivered his proof and a formalization -- no matter how much it looked like autogenerated slop -- he would have been taken much more seriously.

Despite reluctance to do formalization, I expect it will gradually become required to get math published, since journals will be flooded with AI generated slop. It will be necessary to filter the slop, and requirement of formalization in the supplementary material would be a good way to do that. It would still be necessary to check that the formalization of the statement of the theorem is correct, but that's a much smaller ask.

Re: AI in mathematics is forcing big questions

#179

Post by Twey »

indiv0 wrote: post #113
crote wrote: post #99

Earlier quoted context omitted.

> I think the point is to prove the statement. I couldn't disagree more. A lot of mathematical "problems" are almost entirely pointless. Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map - it is the math that is developed during the solving process that is valuable! An answer to a question like "what is the exact area of a unit ci…

My instinct is to agree with you. I believe that the drive to a deeper understanding of the problems is what helps us unlock new areas of study, and find opportunities to transfer techniques or bridge otherwise unconnected domains. But let’s consider a hypothetical: what if an intuitive understanding of the true “boundaries” of mathematics (if such things exist) is beyond the capabilities of a human mind? If there tr…

Mathematics, and its empirical cousin science, are not about picking out individual things that are true in the universe. There is an infinite set of statements of things that are true about the universe, almost all of which are, necessarily, too complex (in a Kolmogorov sense) to be captured by a human mind, and each of which is so specific as to be largely useless. Once you have a statement, though, they're usually trivial to prove by observation.

Mathematics and science are both about building structure on large classes of facts about the (logical or physical, respectively) universe that allow us to generalize our knowledge and make predictions about facts we cannot yet observe. This also lets us make claims about things that are, individually, too complex for the human mind to grasp, by abstracting away the complex details into a simpler structure and then making the claim about anything that satisfies that structure.

To put it another way, mathematics is about finding beauty — specifically those things that exhibit structure that humans can grasp. Modern mathematics, for the most part, makes no claims about what lies outside that space: if it turns out that the universe consists only of things that humans can describe through mathematics that would be neat, but in the much more likely case that it doesn't mathematics continues as it is today.

It's an interesting and maybe even useful trivium if (according to some set of axioms, such as those implemented by your favourite proof assistant) a fact is true, but it's not (human) mathematics, and if there's no useful way for humans to generalize from it there's no point in including it in a library of mathematics. It wouldn't be that surprising (but would be very interesting!) if there were an entire parallel class (or, more likely, family of classes, one for each AI architecture) of AI mathematics comprising structures that AIs can usefully generalize from. Such a thing has no reason to bear any resemblance to human mathematics, which is based on mapping structures to innate human linguistic and spatial intuitions, and may not yield any insights to human mathematicians.

Re: AI in mathematics is forcing big questions

#180

Post by YeGoblynQueenne »

I swear, with AI it's got to the point that I read articles in the tech press that sound like blog posts by homeopathy enthusiasts, the way they play fast and loose with facts and fudge technical details. Take the following:

>> In February, for example, the AI company Math, Inc. used its aspirationally named reasoning agent Gauss to formalize a proof that had earned the mathematician Maryna Viazovska, of EPFL, in Switzerland, a Fields Medal in 2022. Gauss first helped human mathematicians complete the formalization of Viazovska’s solution to the 8-dimensional sphere-packing problem in a matter of days, and then autonomously formalized the more complicated 24-dimensional case in just two weeks.

Gauss "autonomously" formalized? There are no autonomous AI systems! Even the most performant agentic harnesses require extensive human guidance and cannot complete substantial problems without some user interaction. Indeed, if I read the Math, Inc. pages linked in the article I find that Gauss is a typical agentic harness that relies on human scaffolding and interaction and its vaunted autonomy is currently only speculative:

>> Gauss offers a glimpse of how formalization will scale into the future. Currently, it relies on natural language scaffolding supplied by human mathematicians, and requires high-level expert guidance and development on that scaffolding. We anticipate future iterations of Gauss to be more capable and autonomous.

Or take this bit from the Math, Inc. pages again:

>> In two weeks, Gauss then autoformalized the 24-dimensional case using only the original paper as input, performing autonomous literature searches when needed. This brought the total sphere packing formalization from 70k to ~200k lines.

https://www.math.inc/sphere-packing

Gauss took only the original paper as input? Really? No initial prompts? No scaffolding? Just the paper and off it went? But then, the future feared by the young mathematicians at the 12th Heidelberg Laureate Forum, has already come to pass:

>> Speakers described a future in which superhuman AI mathematicians transcend human knowledge and capabilities: forming conjectures, searching solution spaces, proving conjectures, and finally verifying the proofs and generalizing the results, all without human involvement.

Hold the press for that is already happening: Gauss, the autonomous agent for autoformilization, is already capable of running completely autonomously with "only a paper as input"!

This is not serious. It's some kind of over-exaggerated mumbo-jumbo that fails to impart any useful information and makes it impossible to tell what advances have really been made and where things still can go. But perhaps that's exactly the point? Unbelievable.

Post reply on HN