urkud

import Mathlib.Data.Real.NNReal

-- Solution of https://www.facebook.com/groups/mathpuz/posts/2449634078545753/
-- formalized in Lean 4
-- depends on https://github.com/leanprover-community/mathlib4

open NNReal Set

namespace hidden

urkud

Filter	Meaning
at_top	filter generated by [x, +∞)
at_bot	filter generated by (-∞, x]
𝓝 x	neighborhoods of x
𝓝[s] x	neighborhoods of x within s
𝓝[Ici x] x	right neighborhoods of x
𝓝[Ioi x] x	punctured right neighborhoods of x
𝓝[Iio x] x	punctured left neighborhoods of x
𝓝[{x}ᶜ] x	punctured neighborhoods of x

urkud

[[a, b, c, d]| let as = filter ((==2) . length . nub . show) [1..360], a <- as, let bs = filter ((==2) . length . nub . (show a ++) . show) as, b <- bs, c <- bs, d <- bs, a + b + c + d == 360]

urkud

Keybase proof

I hereby claim:

• I am urkud on github.
• I am urkud (https://keybase.io/urkud) on keybase.
• I have a public key ASCZ1-7hsoJLYycGPz6kEvWquYlbz1jIwtJBdaul1N1Wqwo

To claim this, I am signing this object: