Lean4 배워서 남주기

[jeinryu]

이번 학기에 공부한 Lean4를 이용해 기여할 수 있는 오픈소스를 소개합니다. 수학적 증명을 정형화하는 것에 관심 있으신 분들에게 좋은 기회가 될 것 같습니다. 수학적 추측들을 Lean4로 정형화하는 구글 딥마인드의 프로젝트 formal-conjectures입니다. AI에게 좋은 데이터셋이 될 것 같아 소개하고 싶습니다.

이외에도 수학적 증명을 정형화하는 라이브러리가 많이 있습니다. 페르마의 마지막 정리를 정형화하는 FLT, Prime Number Theorem을 정형화하는 Prime Number Theorem 등 취향에 맞게 둘러보시면 좋을 것 같습니다. 또, Lean 게임을 만들 수 있는 lean4game도 있습니다. 여러분들에 의해 NNG같이 훌륭한 게임이 더 나오면 좋겠습니다. PR을 받지는 않는 것 같지만 흥미로운 라이브러리들도 많습니다. 논리학을 정형화하는 FormalizedFormalLogic, 해석학을 정형화하는 analysis 등이 있습니다. 수학을 정형화하는 것에 관심 있으신 분들은 이런 오픈소스에 기여해보면 좋은 기회가 될 것 같습니다.

이외에도 저는 ArkLib이라는 라이브러리에 기여했는데요, 암호학과 ZK 기술의 formalization에 관심이 있다면 둘러보는 것을 추천드립니다.

---

I would like to introduce some open-source projects where you can contribute using the Lean4 skills learned this semester. I believe this will be a great opportunity for those interested in formalizing mathematical proofs.

First is Google DeepMind's project, formal-conjectures, which formalizes mathematical conjectures in Lean4. I wanted to introduce this as it seems likely to become a valuable dataset for AI.

There are many other libraries for formalizing mathematical proofs as well. You might want to explore projects like FLT, which formalizes Fermat's Last Theorem, or Prime Number Theorem, depending on your interests. There is also lean4game, where you can create Lean-based games. I hope to see more excellent games like NNG created by you all.

There are also many interesting libraries that, while they may not be accepting PRs, are still worth noting. Examples include FormalizedFormalLogic, which formalizes logic, and analysis, which formalizes mathematical analysis. For those interested in mathematical formalization, contributing to these open-source projects would be a valuable experience.

Additionally, I contributed to a library called ArkLib. I recommend checking it out if you are interested in the formalization of cryptography and ZK technologies.

[KihongHeo]

훌륭합니다. 여러분들이 사회에 더 많이 기여하는 모습을 보면 저도 더욱 기쁘겠습니다.