The Trojan Horse in AI-Written Mathematics

Kevin Hartnett, author of The Proof in the Code, on the catch in AI autoformalisation. An LLM can now turn a maths paper into Lean code in a fraction of the time a team of humans would take, and the Mathlib community is finding that's a little bit of a Trojan horse: a flood of Lean that isn't written with the precision and economy Mathlib's canonical definitions need. It's the same problem everyone else has with the volume of AI-generated everything. From our documentary "Mathematics Just Changed Forever" with Kevin Hartnett, Kevin Buzzard, Jeremy Avigad, Leo de Moura and Paul Lessard. Watch t