Cet article fascinant m’a renvoyé à l’époque du projet Polymath et des blogs de Gowers et Tao, en retraçant la généalogie qui les lie à Lean et aux preuves par l’IA. J’en recommande la lecture ! (via @monniauxd.bsky.social)
Antoine Blanchard
Software like Lean, which allows mathematical proofs to be written and checked as computer code, could usher in a new, more collaborative era of problem solving. One of its most prominent supporters is mathematician Terence Tao.
www.quantamagazine.org/how-terry-ta...
www.quantamagazine.org
With automated proof-checkers, a problem can be broken up into small chunks, solved bit-by-bit, then reassembled with confidence that every piece is correct. For some, this heralds a new area in…
