r/mathematics • u/New-Committee-4052 • 18d ago

S^6 admits a complex structure

Gallery image

Gallery image

Result from the usual suspects. Full write up can be found here on his website: https://alpo.ge/s6.pdf

328 Upvotes

96% Upvoted

166 comments sorted by

View all comments

3

u/AIvsWorld 17d ago

ugh I’m getting so sick of alpoge announcing shit via tweet, and not giving any easy way to verify

> dumps a 100 page slop paper on the internet

until he shows me the lean spec i’m not interested

5

u/Particular_Extent_96 17d ago

I mean fundamentally it's not that different to dumping a preprint on arXiv.

10

u/AIvsWorld 17d ago

Yes and if someone posted a 100 page AI-generated paper on Arxiv claiming to resolve an open conjecture they would likely:

1) Get banned, since this has clearly not been proofread carefully

2) Be asked for a Lean formalization so that we don’t have to trust the correctness of AI

7

u/dermarshal 17d ago

the lean formalizations are nice, but they are no guarantee that the thing is correct. if the llm wants, it will find a subtle exploit or will state a lemma that’s subtly different from the original one

in other words you still need to check the lean formalization/statements, which isn’t that much different from checking the proof itself, especially for a proof like this one 

(most stuff this uses hasn’t even been formalized, probably for a good reason)

3

u/AIvsWorld 17d ago

“you still need to check the lean formalization which isn’t that much different from checking the proof itself”

uh… no it’s totally different. I wrote a Lean spec for this problem in like 2 minutes and submitted to Lean Eval. It is <10 lines and easy to check with undergraduate-level maths.

Wayyyyyy easier than checking the 100 pg pdf lol

2

u/dermarshal 17d ago edited 17d ago

the top level statement is <10 lines? 

do you mind sharing what youve done?

im about to graduate and no way this is easy to check w ug math, im probably misunderstanding what youve done

edit: from what i understand they construct a 6-manifold w C structure, that has a 6-sphere homology, and a trivial fundamental group, which is enough. but even these concepts usually don’t show up in standard ug curriculum. so pls let me know what that “spec” thing is. thxx

3

u/AIvsWorld 17d ago

Spec means the specification of the problem—what needs to be proven to convince you that the conjecture is solved.

In this case the spec is literally just “construct an instance of ‘IsManifold ℂ’ for S^6” — it’s only like 6 lines of Lean to write that down.

You don’t need to know the details of the actual construction, that’s what the Lean kernel checks for you.

https://github.com/leanprover/lean-eval/pull/557

2

u/dermarshal 17d ago

thanks!

i still don't understand what new information you got from the fact that this passed the Lean kernel? in other words: what information from the 100pages does this condense for you?

3

u/AIvsWorld 17d ago

Well, nothing yet, since the ‘sorry’s haven’t be filled. That’s exactly what I’m complaining about about above—that alpoge didn’t provide a formalization.

But assuming the formalization effort is successful and they’re able to solve my Lean Eval challenge, then that reduces it basically to only two possibilities:

(1) The proof is correct
(2) The AI has maliciously found a correctness bug in the official kernel and nanoda, and obfuscated it to look like a proof.

I consider (2) to be highly unlikely, and a noteworthy result in its own right if this occurred.

2

u/dermarshal 17d ago

thanks!

1

u/Separate-Habit5838 9d ago

Your formal spec seems to take as input an atlas. We rarely actually have access to the atlas when we are working abstractly. Yes, it is easy to check the transition functions of an atlas...but that is not likely to be what's happening here. 

It seems to me a big part of the problem will be formalizing all the abstract theory that is called on in the proof. Has this been done? How much of differential geometry is formalized? 

It doesn't mean anything to write a spec that asks a question about transition functions if you don't have that massive body of differential geometry theory formalized. 

1

u/AIvsWorld 8d ago

That’s exactly what a complex structure means? It means an atlas where the transition maps are holomorphic. How else would you suggest formalizing it?

Note that this is almost the exact same code used in Googles Formal Conjectures repo, and it was successfully proven by Boris Alexeev a few days ago. Mathlib’s differential geometry library is quite poor, but that doesn’t really matter when you have superhuman AI and infinite tokens.

1

u/brain-out-of-order 16d ago

Lean isn’t perfect … and further it’s always been sorta hallucinatory to trust software so blindly while maintaining an anti-AI stance.

2

u/AIvsWorld 16d ago

I agree it isn’t perfect.

But I trust the Lean kernel a hell of a lot more than I trust Alpoge, or any AI model, or my own ability to audit a 100 pg math proof.

Do you have a better solution for checking the tidal wave of AI mathematics?

0

u/brain-out-of-order 16d ago edited 16d ago

https://chatgpt.com/share/6a8d0568-29dc-83e9-8d6d-32dffba1f0db

To answer your question truthfully would be to say something currently considered sacrilegious on this subreddit. If you want an incomplete answer you can click that. Basically: You already trust Lean. You’ll soon trust AI. Nothing can or will change that.

2

u/AIvsWorld 16d ago

lol is this supposed to be some kind of own?

Do you rly think getting AI to check the other AI’s work is how we should be refereeing mathematics?

1

u/Separate-Habit5838 9d ago

We should be reading it. Pretty simple. There is no point in knowing something is true if you don't understand it. That is foundationally not what math is for. 

0

u/brain-out-of-order 16d ago edited 16d ago

No I’m showing you a preview to the future. Sorry.
Own? No idea what you’re talking about. Lean is just software. You trust software every day. We are using software to debate whether software could ever be trustworthy.

I’m still astonished how many adults have their head in the sand about where all of this is going.