Not much. It's too inaccurate for my research and is a bad writer. Day to day I write Lean, and I use moogle.ai to find theorems. It's... fine as a first pass.

Not much. It's too inaccurate for my research and is a bad writer. Day to day I write Lean, and I use moogle.ai to find theorems. It's... fine as a first pass. The website constantly gets confused about similar-looking theorems, it can't pattern match, and it can't really introspect typeclasses (which can be hiding the theorems I want). However it usually can usually help me go from a vague description of what I want to some relevant doc pages, so credit where it's due for that.