Zulip Chat Archive

Stream: new members

Topic: Bulhwi Cha: Introduction

Bulhwi Cha (Aug 11 2022 at 16:18):

Hello, everyone. My name is Bulhwi Cha, and I'm an undergraduate in aerospace engineering at Korea Aerospace University. I've been slowly learning "Theorem Proving in Lean 4" with my friends @shimsw20 and @Minju Kim since the beginning of this year.

I hope to start an EdTech company one day that creates video games and other media for learning STEM subjects. I'm sure proof assistants like Lean and Metamath Zero will play crucial roles in developing serious games for mathematics education.

But I still have a lot to learn. After I finish "Theorem Proving in Lean 4," I'd like to read "Functional Programming in Lean" and "Metaprogramming in Lean 4." Perhaps I could start a small project such as lean-snakebird by then.

I think the future for Lean and formal mathematics is bright!

Last updated: Dec 20 2023 at 11:08 UTC