Get the inside story on Terry Tao’s journey into Lean and AI for math. This is an abridged chapter from @kevinhartnett.bsky.social’s THE PROOF IN THE CODE, available in bookstores tomorrow!
Thomas Lin
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…
