AI in mathematics is forcing big questions • Hacker News Board

Re: AI in mathematics is forcing big questions

#71

Post by jdw64 » Sat, Jun 27, 2026, 6:10 AM UTC

mockerell wrote: post #69

jdw64 wrote: post #66

Someday, human mathematicians might end up doing proofs for proofs. When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it. In those cases, we usually write tests. But when tests get too big, we end up writing tests for the tests. Eventually, it feels like we're heading into an era of proofs for proofs. For me, this problem usually unfolds like this…

That’s an interesting way to think about it. While tests don’t satisfy mathematicians‘ standards for rigor one could instead look at interactive proofs from complexity theory. These are of interest if a problem doesn’t allow for short proofs, i.e. when the problem is not in NP [1]. In your scenario an adapted AI-assisted theorem prover would be the prover, and a mathematician the verifier. [1] https://en.wikipedia.or…

Thank you for explaining my point more logically and coherently. I'll read it over.

Re: AI in mathematics is forcing big questions

#72

Post by bodzioney » Sat, Jun 27, 2026, 6:13 AM UTC

jdw64 wrote: post #66

Someday, human mathematicians might end up doing proofs for proofs. When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it. In those cases, we usually write tests. But when tests get too big, we end up writing tests for the tests. Eventually, it feels like we're heading into an era of proofs for proofs. For me, this problem usually unfolds like this…

Interactive theorem provers are what verifies (or proves) the proof here. This means you don’t even have to look at the actual proof to check its correctness. You just have to make sure the theorem definition is what you wanted (not to say this is trivial) and that no nonsense axioms were defined etc. Now for verifying the theorem prover itself, this is kind of a chicken and the egg problem. We know the mathematical foundations are solid. But to check the implementation of said foundations would require… another theorem prover. In practice, most theorem provers try to make their kernel as small as possible so it can be reasoned about by humans. Coming back to the original topic, mathematics isn’t all proofs though. Someone has to come up with new theories and models. I guess this is what mathematicians would be doing in the future if AI becomes better at proving things than humans. But I could see it narrowing the field, just like it’s doing in others.

Re: AI in mathematics is forcing big questions

#73

Post by schmuhblaster » Sat, Jun 27, 2026, 6:16 AM UTC

fiforpg wrote: post #11

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…

Mathematics has always been an experimental science to some extent. While Newton, Euler and Gauss would spend a lot time calculating numerical approximations by hand, modern mathematicians have been doing the same using computers and software. And once an a clear picture emerge about what’s going, you can start to formalize that and attempt to prove and communicate your results in the standard definition, proposition, lemma, theorem scheme. (Btw there is even a journal called Experimental Mathematics devoted to this approach).

I don’t see that LLMs will fundamentally change this, but rather accelerate the speed of mathematical research.

Some computer generated proofs might of course be hard to understand, but at least their existence gives another data point work with.

Doing Mathematics is more than proving something, that’s just the end of a long road spent pondering at one’s desk about how things could work out.

Re: AI in mathematics is forcing big questions

#74

Post by anon-3988 » Sat, Jun 27, 2026, 6:24 AM UTC

jdw64 wrote: post #66

Someday, human mathematicians might end up doing proofs for proofs. When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it. In those cases, we usually write tests. But when tests get too big, we end up writing tests for the tests. Eventually, it feels like we're heading into an era of proofs for proofs. For me, this problem usually unfolds like this…

What _should_ happen is that we create abstraction. We create a proof for a concept or algorithms. Then we can move on. We need to develop artifacts that can carry proof. We cannot keep writing piles and piles of texts and Python code to build infrastructure. We would be rewriting the same thing 1000x.

Re: AI in mathematics is forcing big questions

#75

Post by ggm » Sat, Jun 27, 2026, 6:27 AM UTC

Argument started when 4 colour map proof was machine assisted. So 1976. (Which the fine article says: I remember my dad being in this argument at the time from the comp. sci side, albiet as a mathematicianby training)

Re: AI in mathematics is forcing big questions

#76

Post by Rekindle8090 » Sat, Jun 27, 2026, 6:33 AM UTC

jdw64 wrote: post #66

Someday, human mathematicians might end up doing proofs for proofs. When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it. In those cases, we usually write tests. But when tests get too big, we end up writing tests for the tests. Eventually, it feels like we're heading into an era of proofs for proofs. For me, this problem usually unfolds like this…

[dead]

Re: AI in mathematics is forcing big questions

#77

Post by FridgeSeal » Sat, Jun 27, 2026, 6:36 AM UTC

crystal_revenge wrote: post #58

zmgsabst wrote: post #54

Earlier quoted context omitted.

You didn’t answer why merge it into a library focused on humans developing mathematics though. It remains all of those things, sitting alone in its own repository of 200kLOC; what benefit comes from merging it into mathlib? > There is also not reason to assume that if we restrict ourselves to the subset of mathematical statements that are human intelligible that this is of any use. This is obviously silly: Things tha…

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

Re: AI in mathematics is forcing big questions

#78

Post by akoboldfrying » Sat, Jun 27, 2026, 6:45 AM UTC

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.

How does this involve computer checking of a formal proof?

Last time I checked, it was a disagreement over whether an informal proof is sound, which is exactly the problem with informal proofs.

ETA: There might be a misunderstanding about what "formal proof" means. Even a very detailed, precise English-language description of a proof is generally not a formal proof. The bar is essentially: "It could be checked by a machine that follows simple rules." If different interpretations of a "proof" are possible, the "proof" is by definition informal. Informal proofs are valuable because they are strong evidence that there's a corresponding formal proof "underneath" that would establish the theorem's truth, and because they are (usually) much easier to understand.

Re: AI in mathematics is forcing big questions

#79

Post by teiferer » Sat, Jun 27, 2026, 7:18 AM UTC

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…

> Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use:

Here is a other one: hello_world.c versus hello_world.exe (apologies for windows extensions, just for illustration).

One is made by a human for human consumption and extension (though legible by a machine). The source code.

One is made by a machine for a machine. Unreadable by a human. The "binary", though that's a terrible misnomer. (Sure you can disassemble but any nontrivial program is too much to cope with as a whole).

Source vs binary. Both are useful but only one is useful for human consumption.

Re: AI in mathematics is forcing big questions

#80

Post by sdenton4 » Sat, Jun 27, 2026, 7:18 AM UTC

zmgsabst wrote: post #70

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…

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…

How many people drive cars without knowing how an engine works? Or make a phone call without knowing how voice compression for a cellular network does it's thing? Or eats food without knowing how it came together from the supply chain?