如何系統(tǒng)地學(xué)習(xí)Lean語言？
作者： 發(fā)布日期：2025-06-29 08:45:11
我就默認(rèn)你學(xué)的是Lean4了。
可以試著玩玩下面兩款交互式證明游戲： The Natural Number Game 這款是自然數(shù)游戲，作者是Kevin Buzzard（就是那個大力推廣Lean4的數(shù)學(xué)家，現(xiàn)在正在領(lǐng)導(dǎo)形式化費(fèi)馬大定理的項(xiàng)目），讓你使用Lean4從皮亞諾公理構(gòu)造自然數(shù)算術(shù)和幾個基礎(chǔ)的運(yùn)算律。
The Set Theory Game 這一款是集合論游戲，讓你熟悉如何用Lean4進(jìn)行涉及集合論的證明。
上面兩款小游戲可以帶你快速熟悉Lean4策略模式的用法，不過對數(shù)學(xué)…。
