Levent Alpöge, the guy who worked with Anthropic's Fable to disprove the Jacobian Conjecture, now claims to have cracked a much bigger problem. The claimed proof is 108 pages - and unlike the Jacobian Conjecture counterexample, it's very hard to check.
Many people have claimed to solve this problem: finding a way to make the 6-sphere into a complex manifold, or showing it's impossible. So far all have gone down in flames. For example, in his later years the famous mathematician Atiyah claimed to prove it's impossible 0 but later, as he became more erratic, people realized it was a first symptom of his mental decline.
This new claimed way to give the 6-sphere a complex structure relies on a heavy-duty result in algebraic topology, but most of the hard work is in the realm of complex geometry. I suspect it would be quite hard to formalize in Lean without using lots of existing results as "axioms" - but I'm no expert on formalization, nor on the math used here.
Another interesting feature is that this result claims to contradict - and disprove some of - a paper published in 2020. It goes into a lot of detail about the conflict, which is good.
I'm really curious how mathematicians will react to this. Will they dive in and figure out what's going on? Will some get sick of Alpöge cracking, or claiming to crack, hard problems with the help of Fable?
And here is a claimed complex structure on S^6: https://alpo.ge/s6.pdf
This is a notorious problem that has attracted many claimed solutions that did not stand up to scrutiny, so some caution is warranted, but IMHO there are also grounds for optimism.
(Context: https://mathoverflow.net/questions/1973/is-there-a-complex-structure-on-the-6-sphere)