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.
