4 ms·Lean Co-pilot for LLM-human collaboration to write formal mathematical proofs4 points by techwizrd 3y ago