Radó's theorem on Riemann surfaces

rado_riemannSurface — a formalization challenge from the lean-eval benchmark.

Formal statement

theorem rado_riemannSurface {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] :
    SecondCountableTopology X := by
  sorry

Source

John Hamal Hubbard, Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1, §1.3.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: rado_riemannSurface
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Junyan Xu.