It may well be that I'm the last actual user of lean 3 on this planet.
It's dead, Jim.

math/lean still works and it's more than good enough for my own fork of
a mathlib from the stone age. I doubt it is all that useful for others
and I can trivially compile all that on demand whenever I need it for
doing some research.

While it is surely possible to get the current lean4 building and
working on OpenBSD - a couple of years back I managed to bootstrap and
build it, but turning my hacks into something viable for ports was way
too painful. math/lean is useless for this endeavor. lean4 is now one
or two orders of magnitude larger than it was back then (not to mention
mathlib).

I simply do not have the time, need and motivation for doing that again
in the foreseeable future.

math/lean doesn't really get in the way, but unless someone speaks up
that they want to keep using it, I think I'd rather remove it after the
release.