AI in mathematics is forcing big questions • Hacker News Board

Re: AI in mathematics is forcing big questions

#131

Post by skydhash » Sat, Jun 27, 2026, 12:47 PM UTC

bananaflag wrote: post #115

teiferer wrote: post #83

Earlier quoted context omitted.

> proofs for proofs. What does that even mean? Sorry, this is just a nonsensical term. The issue is not that the proofs could be wrong. It's that humans don't understand them even if they are verifibly correct. In contrast, with software you don't know if it's correct. That's what you have a test for. Even if you understand it, there could be a bug. And tests could have bugs too, so you can have tests for tests. But…

Thank you for spelling this in detail! One thing I might add is that not all programs can be proved to be correct for the simple reason that not all purposes of a program can be mathematically specified. For example, for (even "closed world" domain programs like) a chess engine, the one thing that matters (in the absence of a complete solution of a game like there exists in checkers) is "can beat world champions", wh…

It cannot be mathematically specified because there’s no way to formalize the statements.

Also code is a mathematical object, but running code (the process) is not because it’s just electricity in metals and semiconductors. We modify the voltage somewhere and that leads to a transformation (light in displays, sound in speakers,..) somewhere else. We do have models for all of this but they are approximations, not the real representation.

Re: AI in mathematics is forcing big questions

#132

Post by bckgrndrdtn » Sat, Jun 27, 2026, 1:03 PM UTC

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?

There's a lot to be said about that: https://lean-lang.org/doc/reference/latest/ValidatingProofs/

But let's assume Lean is perfect: - you have to trust your file system - you have to trust your OS - are you sure your monitor displays "proof is valid" correctly - maybe there's a bug in your CPU hardware? - or background radiation flipped a bit in your RAM - do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".

Re: AI in mathematics is forcing big questions

#133

Post by bckgrndrdtn » Sat, Jun 27, 2026, 1:04 PM UTC

skipkey wrote: post #28

therobots927 wrote: post #23

It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify th…

I would imagine that in the future AI will be doing proofs in Lean or whatever the successor to it, which gives you a pretty good confidence it’s correct.

The future is now. See the article under discussion for some examples.

Re: AI in mathematics is forcing big questions

#134

Post by crote » Sat, Jun 27, 2026, 1:06 PM UTC

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…

> 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 you completely ignore it and end up burning a massive amount of electricity on what is essentially a bunch of LLMs jerking each other off, or you blindly follow it and end up with a Machine God who can justify a genocide with a "This is the correct thing to do. Trust me bro, I have irrefutable proof - you won't understand it". There's just no sensible way to do post-human math in an inherently human world.

Re: AI in mathematics is forcing big questions

#135

Post by bckgrndrdtn » Sat, Jun 27, 2026, 1:08 PM UTC

hackermailman wrote: post #17

paulpauper wrote: post #8

It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very e…

AI can't yet come up with any new ideas to make the inductive leap to solve a math problem. New ideas are what get the accolades and using an old idea just means the original author missed something. We are still at the author missed something stage that AI is doing today. It can definitely be a good research assistant though

All well and good, but we should also admit that under this criterion 95% of published math papers don't contain new ideas but are just filling in stuff that previous authors missed.

Re: AI in mathematics is forcing big questions

#136

Post by throw310822 » Sat, Jun 27, 2026, 1:08 PM UTC

therobots927 wrote: post #23

It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify th…

> even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it.

I hope mathematicians have the self-respect of not establishing rules such as "if a proof is longer than X, break it up in smaller ones, otherwise it'll be outright rejected".

Re: AI in mathematics is forcing big questions

#137

Post by Verdex » Sat, Jun 27, 2026, 1:16 PM UTC

stringfood wrote: post #56

rirze wrote: post #41

I think we’re going to find out the hard way that the proofs left to solve are very much not elegant.

couldn't God have created a more orderly universe for us? this is ridiculous

The way I look at it, the absurd complexity that rule systems can get into is a check and punishment for the arrogant and the tyrannical. 'Look I designed these rules myself just follow them and everything will be fine.' Ah but what about this edge case. 'Hm, I guess we can add a few more rules.' Bam, next thing you know it's a Byzantine bureaucratic nightmare any your empire refuses to grow anymore.

Meanwhile, if you put honorable people in charge and trust them to do the right thing, they can figure things out ad hoc.

Unfortunately, mathematics suffers as a bystander. But the good news is that the muggles will always want to keep the eggheads around because they would rather die than think about the negative consequences of having their dreams come true exactly like they wanted.

Re: AI in mathematics is forcing big questions

#138

Post by bckgrndrdtn » Sat, Jun 27, 2026, 1:16 PM UTC

crystal_revenge wrote: post #51

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…

> Who in their right mind would merge a 200,000-line unaudited vibe-coded blob Anyone who understands type theory and how theorem provers work? It's sort of akin to saying "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!", you know because the compilation would have failed otherwise(this…

You would think that the people maintaining Mathlib are a subset of {understands type theory and how theorem provers work}...

Yet they don't merge this stuff, for many different reasons, including that those 200K lines are free as in puppies.

You can have all the type theory of the world, but the library still needs maintenance.

Change a simp-lemma in a file close to the root. Oooh noes, now there's 987 errors in the 200K loc that we merged last week. And there's nobody there who understands how to fix them.

Just use AI to fix. Or maybe just don't merge the code and let it sit in a downstream library?

And wait until there's evidence that the code is stable, high-quality, with well-designed APIs. And then decide that it might be worthy including in a more foundational library.

Re: AI in mathematics is forcing big questions

#139

Post by crote » Sat, Jun 27, 2026, 1:18 PM UTC

_zoltan_ wrote: post #91

mittensc wrote: post #90

Earlier quoted context omitted.

There's a difference in math between giving just the answer to a problem and doing it properly/elegantly. So yeah, generated machine-valid proof can be denied if it's incomprehensible, same as human machine-valid proof can be denied for same reasons.

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 meaningfully repurpose the individual Lego blocks to build a different interface. You end up having to reinvent the same Lego blocks over and over again, just with a slightly different color each time.

Don't want to re-prove each and every Lego brick? Then you shouldn't accept giant black box proofs.

Re: AI in mathematics is forcing big questions

#140

Post by bckgrndrdtn » Sat, Jun 27, 2026, 1:20 PM UTC

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