chabulhwi

I'm also a Korean, and I've been getting on without KakaoTalk for two years. But I've never met any other Korean personally who doesn't use it.

Yes.

Theorem Proving in Lean 4: https://leanprover.github.io/theorem_proving_in_lean4/

I only had a basic knowledge of first-order logic and set theory before reading TPiL4. It wasn't easy, but now I can prove theorems in Lean. By the way, I still can't write a program in any language.

Lean is an interactive theorem prover. It can verify proofs written in Lean by humans. Mathlib is a monolithic library of classical mathematics written in Lean. Mathematicians contributing to Mathlib love it because it has all the interconnected subdisciplines they need in one place, and most of them aren't huge fans of constructive mathematics or univalent mathematics.

Lean is also a strict pure functional programming language with dependent types. You can write correct and maintainable programs in Lean. You can also write proofs showing that a program terminates or it computes the desired answer, etc. Some computer scientists and programmers praise Lean's extensible syntax and editor support.

See also: https://leanprover.zulipchat.com/#narrow/stream/113488-gener...