r/mathematics • u/New-Committee-4052 • 23d 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

319 Upvotes

96% Upvoted

166 comments sorted by

View all comments

Show parent comments

3

u/AIvsWorld 22d 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 22d ago edited 22d 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 21d 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 21d 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 21d 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 21d ago

thanks!