A slightly longer Lean 4 proof tour | What's new
In my previous post, I walked through the task of formally deducing one lemma from another in Lean 4. The deduction was deliberately chosen to be short and only showcased a small number of Lean tac…
A slightly longer Lean 4 proof tour | What's new What's new Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao Home About Career advice On writing Books Mastodon+ Applets Subscribe to feed A slightly longer Lean 4 proof tour 5 December, 2023 in expository , math.CA | Tags: Lean4 | by Terence Tao In my previous post , I walked through the task of formally deducing one lemma from another in Lean 4 . The deduction was deliberately chosen to be short and only showcased a small number of Lean tactics. Here I would like
related reading
- Lean Programming Languagelean-lang.org
- Lean Game Serveradam.math.hhu.de
- What's new | Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Taoterrytao.wordpress.com
- There’s more to mathematics than rigour and proofs | What's newterrytao.wordpress.com
- Using spaced repetition systems to see through a piece of mathematicscognitivemedium.com
- Xena | Mathematicians learning Lean by doing.xenaproject.wordpress.com
- Formalizing Fermat's Last Theoremanthropic.com
- FLT: Anthropic has beaten me to itxenaproject.wordpress.com
- A shallow dive into formal verificationvitalik.eth.limo
- blueprint.pdfimperialcollegelondon.github.io
- A Lean Syntax Primer — overreactedoverreacted.io
- 3. Logic - Mathematics in Lean v4.19.0 documentationleanprover-community.github.io