LLMs have gotten good at creating Lean proofs so the are much more common but not universal. And they depend on https://github.com/leanprover-community/mathlib4