Question about Elementary Geometry formalization

Stream: mathlib4

[Louis Liu]

Hi guys! I am new to the community and have a question regarding the current stage of formalization in Elementary Geometry:

I wonder why some important theorems in Elementary Geometry (eg. Ceva's theorem and Menelaus's theorem) haven't been formalized so far? Is it because we currently intend to give priority to formalizing the theorems which are more mathematically general or we've met some severe barriers to overcome first in order to progress at the stage? If it is the latter case, could anyone specify what those barriers are? Thanks!!!

[Kevin Buzzard]

Nobody is really giving priority to anything, the growth of the library is organic and just goes where people are interested.

[Yaël Dillies]

Ceva is proved in !3#10632

[Yaël Dillies]

Elementary geometry is in fact pretty hard to formalise. It you're interested, I suggest you ask Joseph Myers.

[Louis Liu]

Thank you for the info!! @Kevin Buzzard @Yaël Dillies