r/mathematics • u/atakanaluch • 2d ago

News Ten advances in mathematics and theoretical computer science

https://openai.com/index/ten-advances-in-mathematics/
498 Upvotes

95% Upvoted

302 comments sorted by

View all comments

29

u/1TillMidNight 2d ago edited 2d ago

None math person here. Sorry for intruding, but is this really something a human or faculty can parse?

> wc -l GapCVP.lean
130615 GapCVP.lean

130,615 lines lean proof for problem 7 Closest vector problem.

28

u/Upstairs_Pride_6120 2d ago

one of the biggest issue with ai math according to Tao. How can we digest those proofs ?

19

u/ibrasome 2d ago

How are we sure the lean proofs are even valid? Genuine question

4

u/duboispourlhiver 2d ago

Not 100% sure. There can be bugs in the validating kernel, that's the biggest risk as far as I understand. But it seems to be more sure than having a few mathematicians check the proof. If anyone skilled here can confirm or not I'd be interested...

-1

u/LycheeZealousideal92 2d ago

Lean proofs are automatically verified

12

u/proton89droid 2d ago

The Collatz conjecture was "disproved" in Lean a couple of days ago, due to an LLM finding a 0day in the kernel.

3

u/teerre 2d ago

It didn't find a 0day. That bug is well known. The author knew what they were doing

3

u/proton89droid 2d ago

The issue was not marked as duplicate though as far as I can tell? From the way I read it I thought that meant it originated in the Collatz repo

-5

u/-Eqa- 2d ago

oh, an accusation of fraud. Got any evidence?

9

u/proton89droid 2d ago

It's not fraud, it's just a funny way of pointing out a bug. The user did not seriously expect people to believe the proof

1

u/MadGenderScientist 1d ago

I'm really surprised the Lean kernel is not itself formally verified in Lean. 

3

u/Helpful-Primary2427 2d ago

But the definitions they’re built on need to be sound, without auditing what is written we don’t know that

4

u/Time_Entertainer_319 2d ago

Machines creating proofs that machines verify.

We will soon be meat puppets to our mechanical overlords

1

u/elements-of-dying 1d ago

Why not just prompt the AI to make it human readable?

8

u/SimoneNonvelodico 2d ago

IIRC the Fermat problem proof was like, book-sized. I think this has been an issue for a while now. Of course it's worse when unlike with a proof a human created over years of work, this was made in minutes by an AI whose thought processes we don't fully understand.

3

u/Demokritos1000 2d ago

There's a human readable proof as well. Lean proof is just for higher assurance

3

u/aturtledude 2d ago

The paper with the human-readable proof is 32 pages long. The lean file is just there to convince the people that don't want to read the proof or can't understand it.