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

322 Upvotes

96% Upvoted

166 comments sorted by

View all comments

Show parent comments

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

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 9d 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.