3 ms·Wouldn’t a lot already be in leans mathlib?by Jaxan 21d agoWouldn’t a lot already be in leans mathlib?throw567643u8 21d agoAI is hopeless at using existing code, it likes to append only.