I've only thought of this because superficially they look the same, and seem to be making similar claims. When you prove a statement P=>Q ◻, then is it the same as writing ◻P=>Q in modal logic?
As Mauro indicates the original intention of Halmos was not ◻ to mean "necessarily". But if you agree that our logic holds in all possible worlds - a necessary assumption when discussing possible worlds at all - then any mathematical(!) proof A => B holds necessarily in any possible world, hence ◻(A=>B).