Post #4256563

@mevenlennonbertrand@lipn.info Perhaps: """ Using LLMs and the Lean Proof Assistant for maths makes it hard to tell if you've discovered new maths or a bug in Lean. """