Lean 4 語言體驗心得與軟體的未來

​🚀 《Lean 4 語言體驗心得與軟體的未來》活動來了！ 🚀

Lean 4 是一個用來證明數學的語言，不要跟 Lean 以太坊專案搞混了。

​我會先分享自己上手 Lean 4 的經歷：實際用起來是什麼感覺，從 Lean Game Server 到從頭證明 Arrow's Impossibility Theorem。

​然後我們來看：AI 現在可以快速找出程式裡的 bug，也能以同樣的速度寫出新的程式碼。那在這個新世界裡，要怎麼打造安全的軟體？人們現在用 Lean 4 在做的事，或許能讓我們看見未來在以太坊、密碼學、乃至整個軟體開發會長什麼樣子。

"本場演講將以英文進行，無需任何數學證明經驗。"
-
活動時間：05 月 20 日（三）19:00 - 20:30（18:30 入場）
活動地點：imToken，台北市中正區羅斯福路二段 9 號 9 樓
活動講者：CC – 過去，他在以太坊生態系統中開發零知識應用程式。
-
🎓 參加活動，你可以收穫什麼？
✔️ 了解 Lean 4 實際上手的學習路徑與使用體驗
✔️ 了解講者如何從 Lean Game Server 走到證明 Arrow's Impossibility Theorem
✔️ 思考 AI 時代下，Ethereum、密碼學與軟體工程可能走向的未來