感覺使用lean4很像用計算機編程

有無最簡單的實例？

回復 @啊啊是誰都對：有的，git clone https://github.com/leanprover-community/mathematics_in_lean.git下載mathematics_in_lean，在這個項目的目錄下lake exe cache get就可以下載相應的依賴文件，然後在vscode里打開項目文件夾，在MIL子文件夾下就可以看到例子了