← Back to context Comment by Jaxan 3 hours ago Wouldn’t a lot already be in leans mathlib? 1 comment Jaxan Reply throw567643u8 2 hours 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.