Terence Tao has been experimenting with formal theorem proving using Lean and writing about his experience. Here’s something Tao said on Mathstodon that I thought was interesting. It is remarkable how much “decoupling” is achieved by the Lean+Blueprint combo. Contributors can work locally on proving a lemma, without necessarily fully understanding the global proof structure. […] The post Decoupling formal theorem proving effort first appeared on John D. Cook.