Formalizing Belyi's Theorem / Dessins

Stream: maths

[Ayberk Zeytin]

Hi everyone! :wave:

I am new and this is my first post here. So apologies if I am breaking rules.

I've been considering formalization of Belyi’s Theorem and the theory of Dessins d'Enfants. Before I dive in, I wanted to check with the community to see if this is a realistic undertaking given the current state of Mathlib.
Questions I have in mind:

• Is the "easy" algebraic direction (1) currently feasible with the state of function fields/projective curves in Mathlib?
• Is anyone currently working on formalizing Dessins d'Enfants (combinatorial maps) or Belyi's theorem? I’d hate to duplicate work!
• Would a formalization of just the combinatorial side (maps on surfaces) and the definition of a Belyi map be considered a useful contribution on its own?
  Any insights or warnings about "rabbit holes" in this area would be appreciated!