I'm using MacOS 10.12.6. lamport.org does resolve to 205.233.73.65 for me. I don't use a proxy server in the browser, but at work our requests do go through ForcePoint. TLA Toolbox seems to start up OK for me at home, but comes up with the login when I try to run it from work. (Screenshot attached.)
Using Wireshark, I see an HTTP GET to 205.233.73.65 for /tlatoolbox/toolboxUpdate/p2.index, which gets an HTTP 307 Authentication Required response. When I make the same request from a browser I get an HTTP 302 redirect to http://tla.msr-inria.inria.fr/tlatoolbox/toolboxUpdate/p2.index, which works. Strange... seems like ForcePoint is messing it up somehow, but not sure why it works OK from the browser, unless ForcePoint is varying its behavior based on the User-Agent header or something like that.
