Automorphisms of ℂ

Stream: Is there code for X?

[Alena Gusakov]

This might be a stretch, but is there a proof of the existence of wild automorphisms of the complex numbers assuming the axiom of choice? Or any work being done with that intention?

[Mario Carneiro]

Well we do have the existence of bases on arbitrary vector spaces

[Mario Carneiro]

I forget how much more is needed to turn that into a field hom

[Alena Gusakov]

That's fair, I don't think I really understand the full proof yet anyway. I just thought it was a cool result and was wondering whether it would make for a good project, way out in the future, once I've gained a lot more experience with Lean and do actually understand the proof lol

[Johan Commelin]

We need a bit of stuff on transcendental field extensions, but I don't think that much is missing.

[Johan Commelin]

Once you have the concept of a transcendence basis, you are basically done.