Bulhwi Cha: Introduction

Stream: new members

[Bulhwi Cha]

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!