Hey, guys. It is a second try of my blogging. You know me from my prev. channel and if you don’t know me, it is not a problem, just read my posts. You are here to learn something, not for deanonyming me. Let’s start 😀

Hey. in these days, I started to learn "Lean 4" in parallel while I am learning Haskell. Here my first simple proof you can see:

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  rw [← mul_assoc a b c]
  rw [← mul_assoc b a c]
  rw [mul_comm a b]

In these example, I proved a * (b * c) = b * (a * c) with multiplication association and commutative properties.

1. I rewrite expression on the left with association: a * (b * c) -> a * b *c
2. I rewrite expression on the right with association: b * (a * c) -> b * a * c
3. I rewrite expression on the left with commutative for a and b: a * b * c -> b * a * c
4. Expressions on the left and right now equal with reflexivity: b * a * c = b * a * c

Link

In this problem, you have to implement your sqrt function without using any std library.

What did I do? Using a property of sorted order of natural numbers, I did binary search between 0 and half of given number. And checked square of mid number is equal to given number. If result is not found, returned the last number which square of this number is less than given number

Yesterday, we have participated in Cyberkent 3.0 and have got 20 place.

It is nicer than previous year