← Back to context Comment by Jaxan 2 hours ago Wouldn’t a lot already be in leans mathlib? 1 comment Jaxan Reply throw567643u8 1 hour ago AI is hopeless at using existing code, it likes to append only.
AI is hopeless at using existing code, it likes to append only.