News for hackers. Stuff that matters.

A comment on Lean proof of Fermat's Last Theorem [pdf]. Parent comment

Re:Lean proof of Fermat's Last Theorem [pdf] by joachimma on Thursday August 21, 2025 @02:31AM (#44969690)
Terrence Tao is apparently in the process of converting the exercises from his "Analysis I" book into Lean.

https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t...

[ Parent | on HN ]
Re:Lean proof of Fermat's Last Theorem [pdf] by majikaja on Thursday August 21, 2025 @05:35AM (#44970785)
This is cool

I guess intros based on the structure of mathlib could work for people who haven't published their own textbooks.

[ Parent | on HN ]