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

151–160 of 193 posts

Re: AI in mathematics is forcing big questions

#151

Post by abdullahkhalids »

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.

Terence Tao talks about this [1]

> In particular, the process of converting a medium-sized Lean document (containing a few thousand lines of code, with some proofs AI-generated) into a nicely golfed and structured Mathlib submission has been an interesting experience. AI agents can be used to perform local golfs that can shave the size of the code somewhat, but global refactoring decisions, such as noticing that a certain argument appears multiple times across the document and can be abstracted into a standalone lemma that can may have additional utility beyond the file, is still largely beyond the reach of current AI tools. (I find that I can explain such a refactor to an AI agent, who can then execute it, but they struggle to spontaneously discover such refactors on their own.)

[1] https://mathstodon.xyz/@tao/116789373239346609

Re: AI in mathematics is forcing big questions

#152

Post by jonahx »

tacomonstrous wrote: post #48
jonahx wrote: post #30

Earlier quoted context omitted.

> It would be great if someone could explain to me how AI improves this situation. It's main utility is in the search step, not the verification step. The search is the bulk of the work and creativity. Separately, as the sibling commenter pointed out, it will likely get better at the verification step as well, with integrations of tools like Lean. > One hallucination in 300 steps of logic is enough to destroy the ent…

>The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired. In fact, it was Wiles himself who realized there was an error.

Yes, at the prodding of the reviewer (from wikipedia):

> After the announcement, Nick Katz was appointed as one of the referees to review Wiles's manuscript. In the course of his review, he asked Wiles a series of clarifying questions that led Wiles to recognise that the proof contained a gap.

It seems likely Katz played a crucial role here.

Wiles is just a prominent example. In practice, other humans often play this "verification role" for mathematicians, whether via a formal review process or informal discussion.

Re: AI in mathematics is forcing big questions

#153

Post by bckgrndrdtn »

Diogenesian wrote: post #118
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…

These proof checkers all have bugs, every single one, and since AI is still 100% incapable of understanding simple mathematics we should assume agents are likely to cheat by exploiting a kernel bug. So a human really does have to be able to read and understand the proof. There's no difference between blindly trusting Lean and blindly trusting Grigori Perelman: yes you can be reasonably confident the proof is correct.…

> These proof checkers all have bugs, every single one

Please show me a proof of `False` in Lean.

Re: AI in mathematics is forcing big questions

#154

Post by indiv0 »

crote wrote: post #134
indiv0 wrote: post #113

Earlier quoted context omitted.

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…

> what if an intuitive understanding of the true “boundaries” of mathematics (if such things exist) is beyond the capabilities of a human mind? By extension: why should we assume that a human would still understand the problems - or the answers? If all of it is complete gibberish to a human and can never be applied in any way, shape, or form, then what's the point? The way I view it there are two options here: either…

That’s a fair point. I wouldn’t want to take machine god’s proclamations on faith either. I’d prefer it if the knowledge was always within our grasp. There is also a possible middle ground where we don’t understand the questions or the answers but we still benefit from the effects of the application of that knowledge. “Sufficiently advanced technology is indistinguishable from magic” and all that. Hopefully we can still judge the results based on the effects. Rejecting a call to genocide should be easy enough, but on the other hand the Native Americans couldn’t foresee what the smallpox blankets would do to them. Working from a position where you are the weaker side of a knowledge gap is a scary thought. It’s a rational fear and I think a lot of people will end up on that side of the divide if AI continues to advance.

Re: AI in mathematics is forcing big questions

#155

Post by pfdietz »

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…

Perhaps in the future we'll see golfing of formalized proofs as a valid and valuable form of mathematics, not just proving a theorem for the first time.

Of course there's no reason AI couldn't do that too.

Re: AI in mathematics is forcing big questions

#156

Post by pfdietz »

bsder wrote: post #40
akoboldfrying wrote: post #29

Earlier quoted context omitted.

Well, if you can formalise the problem statement (this is the hard part) sufficiently well that the computer can produce a proof, you can be very sure the proof is sound. A fundamental property of any formal proof is that it can be checked by a fairly stupid machine, automatically, because every step is a simple mechanical operation that names one of a handful of axioms and refers to a handful of earlier steps, the t…

> 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.

Re: AI in mathematics is forcing big questions

#157

Post by pfdietz »

whattheheckheck wrote: post #65
kimjune01 wrote: post #36

Earlier quoted context omitted.

lean compiles or it doesnt

You can also pass pytest with assert 1 = 1...

There are also ways to cheat like that in Lean, but they are all easily identifiable. So when people talk about formalization, they mean formalization without such cheats.

Re: AI in mathematics is forcing big questions

#158

Post by bwfan123 »

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…

Loved Bessis's book and his writings because of his human-centric view which is missed by the ai maximalists. I just cant wait for the upcoming AI bust to skim the froth in the debate.

Re: AI in mathematics is forcing big questions

#159

Post by pfdietz »

AaronAPU wrote: post #116
jstanley wrote: post #61

Earlier quoted context omitted.

This is what Lean is for: https://lean-lang.org/ If you have the LLM generate Lean code, and it compiles, then the proof is correct and you don't need to bother checking its working. (You still need to check that it is proving the theorem you asked it to prove).

I’m playing devil’s advocate here, so go easy on me. But how completely do we know lean is perfectly true in all cases?

If there's concern, I understand Lean can dump out a proof object, and this object can be checked for validity by a separate, smaller program. One could even write that smaller program multiple times.

It would be interesting to see how Lean is being tested. Pummeling it with inputs from AI proof search engines sounds like a good way to expose hidden bugs, just as pummeling a compiler with randomly generated programs is a good way to expose previously unknown compiler bugs.

Post reply on HN