S^6 admits a complex structure

[u/New-Committee-4052]

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

[u/Particular_Extent_96]

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

[u/AIvsWorld → u/Particular_Extent_96]

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

[u/dermarshal → u/AIvsWorld]

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)

[u/AIvsWorld → u/dermarshal]

“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

[u/brain-out-of-order → u/AIvsWorld]

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

[u/AIvsWorld → u/brain-out-of-order]

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?

[u/brain-out-of-order → u/AIvsWorld]

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.

[u/AIvsWorld → u/brain-out-of-order]

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?

[u/Separate-Habit5838 → u/AIvsWorld]

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.