3 ms·
He didn't really fully explain why he chose Lean over Coq or Agda though.
by thdhhghgbhy 1y ago
He didn't really fully explain why he chose Lean over Coq or Agda though.
- _delirium 1y agoFor this book specifically, I think the reason is just that Lean is the theorem prover he already knows and uses in his own work [1]. Now as to why he picked Lean a few years ago as his go-to theorem prover, I do think that would be an interesting backstory. As far as I know he hasn't written anything explicit about it. [1] E.g., https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...
- UltraSane 1y agoI would assume he chose Lean because it is what Kevin Buzzard has popularized and has been used to prove some very complex theories.