Decoupling formal theorem proving effort
( go to the article → https://www.johndcook.com/blog/2023/11/19/decoupling-formal-theorem-proving-effort/ )
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.
Nov. 19, 2023, 11:39 p.m.