Lean 3 formalization of 1998 Bulgarian Mathematical Olympiad Problem 8

[@hotdogontology]

Do you mind sharing what your setup for LEAN is on your computer? Whatever you have done is running smooth and quick.

[@dwrensha]

I'm using emacs with lean-mode github.com/leanprover/lean-mode
One important step is running `leanproject get-mathlib-cache` (leanprover-community.github.io/leanproject.html#getting-mathlib-oleans ) before opening the file. That way, you don't need to recompile mathlib from source.

[@hotdogontology]

@@dwrensha Thank you.