From: Theo Buehler <tb@theobuehler.org>
Subject: Re: math/lean: update to 4.35.0 + deps; math/mathlib: new port (version 4.35.0)
To: ports@openbsd.org
Date: Thu, 15 Oct 2026 12:44:23 +0200

> Anyway, regarding the size: it is large but without it modern lean is
> somehow useless. Almost everything inside mathlib.

I know what you mean.

You have my approval for the update. Not mathlib. I gave my reasons for
suggesting to remove lean a while back.