Diamond problems and universes

Stream: Machine Learning for Theorem Proving

[Bas Spitters]

When auto-formalizing, I notice the LLM often has problems with diamond inheritance problems and with universes.
This is not a surprise, this is hard for humans too, but it may be another reason to think deeper about these issues.

The new universe system in Rocq, may be interesting for Lean too. I believe this is the latest state update:
https://sozeau.gitlabpages.inria.fr/www/research/publications/Bounded_Cumulative_Universe_Polymorphism_with_Algebraic_Universes-AIMXIX-241125.pdf