Perhaps a CLD2 / CLD3 based language detector can be added to support the autodetect feature that's common in other translation services. - https://github.com/CLD2Owners/cld2 - https://github.com/google/cld3 Maybe we can go with CLD3 Here's a lean 4 proof that 3 > 2 ```lean example : 3 > 2 := Nat.lt.base 2 ```