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

61–70 of 193 posts

Re: AI in mathematics is forcing big questions

#61

Post by jstanley »

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…

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

Re: AI in mathematics is forcing big questions

#62

Post by whattheheckheck »

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…

And theyre ignorant. You want to be ignorant? They had a term for that in ancient Greece.

Reasoning by analogy...

Re: AI in mathematics is forcing big questions

#63

Post by whattheheckheck »

akoboldfrying wrote: post #29
jackyinger wrote: post #14

Earlier quoted context omitted.

To bluntly put it in a nutshell, and state the obvious: If you don’t understand the problem you can’t be sure that the computer does.

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…

Complexity theorists are in a good spot

Re: AI in mathematics is forcing big questions

#64

Post by greenavocado »

zmgsabst wrote: post #54
crystal_revenge wrote: post #51

Earlier quoted context omitted.

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

My brother in Christ, you didn't need x86 opcodes to be intelligible to use this web site.

Re: AI in mathematics is forcing big questions

#65

Post by whattheheckheck »

kimjune01 wrote: post #36
jackyinger wrote: post #14

Earlier quoted context omitted.

To bluntly put it in a nutshell, and state the obvious: If you don’t understand the problem you can’t be sure that the computer does.

lean compiles or it doesnt

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

Re: AI in mathematics is forcing big questions

#66

Post by jdw64 »

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:

1.I can't trust SDKs or Stack Overflow code.

2.So I write tests.

3.But I can't trust the tests either.

4.So I use test coverage, mutation testing, property testing, and fuzzing.

5.If that's still not enough, I add formal verification.

6.And then the problem becomes: can I trust the verifier?

That's how it ends up. Wouldn't human work shift toward verifying the verification systems themselves?

Re: AI in mathematics is forcing big questions

#67

Post by galaxyLogic »

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.

Re: AI in mathematics is forcing big questions

#68

Post by dripdry45 »

greenavocado wrote: post #64
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…

My brother in Christ, you didn't need x86 opcodes to be intelligible to use this web site.

No, but SOMEONE did.

Re: AI in mathematics is forcing big questions

#69

Post by mockerell »

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.org/wiki/Interactive_proof_system

Re: AI in mathematics is forcing big questions

#70

Post by zmgsabst »

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…

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 mathematics without understanding, you cause disasters: stock market crashes from mispricing options, Amazon’s 2018 hiring freeze from misallocating $1B, etc.

Note: neither of your examples (sleep, gravity) are things that people intentionally use. They just happen to people.

I think it’s very telling you couldn’t think of an example.

Post reply on HN